non-normal modal logic

The syntax of non-normal modal logic systems resembles that of normal modal logics, which is founded upon propositional logic. An atomic statement is represented with propositional variables (e.g., $p,\; q,\; r$); logical connectives include negation ($\backslash neg$), conjunction ($\backslash land$), disjunction ($\backslash lor$) and implication ($\backslash to$). The modalities are most commonly represented with the box ($\backslash Box$) and the diamond ($\backslash Diamond$).

A formal grammar for this syntax can minimally be defined using only the negation, disjunction and box symbols. In such a language,

$\backslash varphi,\; \backslash psi\; :=\; p\backslash \; |\backslash \; \backslash neg\backslash varphi\backslash \; |\backslash \; \backslash Box\backslash varphi\backslash \; |\backslash \; \backslash varphi\; \backslash lor\; \backslash psi$ where $p$ is any propositional name. The conjunction $\backslash varphi\; \backslash land\; \backslash psi$ may then be defined as equivalent to $\backslash neg\; (\backslash neg\backslash varphi\; \backslash lor\; \backslash neg\backslash psi)$. For any modal formula $\backslash varphi$, the formula $\backslash Diamond\backslash varphi$ is defined by $\backslash neg\backslash Box\backslash neg\backslash varphi$. Alternatively, if the language is first defined with the diamond, then the box can be analogously defined by $\backslash Box\backslash varphi\; \backslash equiv\; \backslash neg\backslash Diamond\backslash neg\backslash varphi$.{{cite journal |last=Carnap |first=Rudolf |author-link=Rudolf Carnap |title=Modalities and Quantification |journal=The Journal of Symbolic Logic |volume=11 |issue=2 |date=June 1946 |pages=33–64 |doi=10.2307/2268610 |publisher=Association for Symbolic Logic |jstor=2268610 |url=https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/modalities-and-quantification/9BCD64F045217C2B13A02277F0FFBB9E |access-date=27 December 2023|url-access=subscription }}

For any propositional name $p$, the formulae $p$ and $\backslash neg\; p$ are considered propositional literals whilst $\backslash Box\; p$ and $\backslash neg\backslash Box\; p$ are considered modal literals.

Logic E, the minimal variant of non-normal modal logics, includes the RE congruence rule in its Hilbert calculus or the E rule in its sequent calculus.

The Hilbert calculus for logic E is built upon the one for classical propositional logic with the congruence rule (RE): $\backslash frac\{A\; \backslash leftrightarrow\; B\}\{\backslash Box\; A\; \backslash leftrightarrow\; \backslash Box\; B\}$. Alternatively, the rule can be defined by $\backslash frac\{A\; \backslash leftrightarrow\; B\}\{\backslash Diamond\; A\; \backslash leftrightarrow\; \backslash Diamond\; B\}$. Logics containing this rule are called congruential.

The sequent calculus for logic E, another proof system that operates on sequents, consists of the inference rules for propositional logic and the E rule of inference: $\backslash frac\{A\; \backslash vdash\; B\; \backslash qquad\; B\; \backslash vdash\; A\}\{\backslash Gamma,\; \backslash Box\; A\; \backslash vdash\; \backslash Box\; B,\; \backslash Delta\}$.

The sequent $\backslash Gamma\; \backslash vdash\; \backslash Delta$ means $\backslash Gamma$ entails $\backslash Delta$, with $\backslash Gamma$ being the antecedent (a conjunction of formulae as premises) and $\backslash Delta$ being the precedent (a disjunction of formulae as the conclusion).

The resolution calculus for non-normal modal logics introduces the concept of global and local modalities. The formula $\backslash mathsf\{G\}(\backslash varphi)$ denotes the global modality of the modal formula $\backslash varphi$, which means that $\backslash varphi$ holds true in all worlds in a neighbourhood model. For logic E, the resolution calculus consists of LRES, GRES, G2L, LERES and GERES rules.{{cite conference |last1=Pattinson |first1=Dirk |last2=Olivetti |first2=Nicola |last3=Nalon |first3=Cláudia |title=Resolution Calculi for Non-normal Modal Logics |conference=TABLEAUX 2023 |series=Lecture Notes in Computer Science |volume=14278 |pages=322–341 |date=2023 |doi=10.1007/978-3-031-43513-3_18 |doi-access=free }}

The LRES rule resembles the resolution rule for classical propositional logic, where any propositional literals $p$ and $\backslash neg\; p$ are eliminated: $\backslash frac\{D\; \backslash lor\; l\; \backslash qquad\; D\text{'}\; \backslash lor\; \backslash neg\; l\}\{D\; \backslash lor\; D\text{'}\}$.

The LERES rule states that if two propositional names $p$ and $p\text{'}$ are equivalent, then $\backslash Box\; p$ and $\backslash neg\backslash Box\; p\text{'}$ can be eliminated. The G2L rule states that any globally true formula is also locally true. The GRES and GERES inference rules, whilst variants of LRES and LERES, apply to formulae featuring the global modality.

Given any modal formula, the proving process with this resolution calculus is done by recursively renaming a complex modal formula as a propositional name and using the global modality to assert their equivalence.

{{See also|Neighbourhood semantics}}

Whilst Kripke semantics is often applied as the semantics of normal modal logics, the semantics of non-normal modal logics are commonly defined with neighbourhood models. A standard neighbourhood model $\backslash mathcal\{M\}$ is defined with the triple $\backslash langle\; \backslash mathcal\{W\},\; \backslash mathcal\{N\},\; \backslash mathcal\{V\}\; \backslash rangle$ where:{{cite book |last=Pacuit |first=Eric |title=Neighborhood Semantics for Modal Logic |series=Short Textbooks in Logic |publisher=Springer |date=November 2017 |isbn=978-3-319-67149-9 |url-access=subscription |url=https://link.springer.com/book/10.1007/978-3-319-67149-9 |doi=10.1007/978-3-319-67149-9 |access-date=24 December 2023}}{{cite thesis |last=Dalmonte |first=Tiziano |title=Non-Normal Modal Logics: Neighbourhood Semantics and their Calculi |publisher=Aix-Marseille Université |year=2020 |url=https://www.theses.fr/2020AIXM0314.pdf |access-date=24 December 2023}}

• $\backslash mathcal\{W\}$ is a non-empty set of worlds.
• $\backslash mathcal\{N\}:\; \backslash mathcal\{W\}\; \backslash to\; \backslash mathcal\{PP\}(\backslash mathcal\{W\})$ is the neighbourhood function that maps any world to a set of worlds. The function $\backslash mathcal\{P\}$ denotes a power set.
• $\backslash mathcal\{V\}:\; Atm\; \backslash to\; \backslash mathcal\{P\}(\backslash mathcal\{W\})$ is the valuation function which, given any propositional name $p$, outputs a set of worlds where $p$ is true.

The semantics can be further generalised as bi-neighbourhood semantics.{{cite conference |last1=Dalmonte |first1=Tiziano |last2=Olivetti |first2=Nicola |last3=Negri |first3=Sara |author-link3=Sara Negri |title=Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi |book-title=Advances in Modal Logic 2018 |date=August 2018 |location=Berne, Switzerland |isbn=978-1-84890-255-8 |url=https://hal.archives-ouvertes.fr/hal-02076639}}

The classical cube of non-normal modal logic considers axioms M, C and N that can be added to logic E defined as follows.

A logic system containing axiom M is monotonic. With axioms M and C, the logic system is regular. Including all three axioms, the logic system is normal.

With these axioms, additional rules are included in their proof systems accordingly.

{{Reflist}}

Category:Modal logic

Category:Semantics