Non-normal modal logic

A non-normal modal logic is a variant of modal logic that deviates from the basic principles of normal modal logics. Normal modal logics adhere to the K axiom ($\Box (p\to q)\to \Box p\to \Box q$) and the necessitation principle which states that "a tautology must be necessarily true" ($A\to \Box A$). On the other hand, non-normal modal logics do not always have such requirements. The minimal variant of non-normal modal logics is logic E. Axioms M, C and N can be added to the logic system. With all three axioms added to logic E, a logic system equivalent to normal modal logic K is formed.

Syntax and Proofs

The syntax of non-normal modal logic systems resembles that of normal modal logics. The modalities are most commonly represented with the box ($\Box$) and the diamond ($\Diamond$). For any modal formula $\varphi$, the formula $\Diamond \varphi$ is defined by $\neg \Box \neg \varphi$. Alternatively, if the language is first defined with the diamond, then the box can be analogously defined by $\Box \varphi \equiv \neg \Diamond \neg \varphi$.

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.

Hilbert Calculus

The Hilbert calculus for logic E is built upon the one for classical propositional logic with the congruence rule (RE): ${\frac {A\leftrightarrow B}{\Box A\leftrightarrow \Box B}}$.

Logics containing this rule are called congruential.

Sequent Calculus

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: ${\frac {A\vdash B\qquad B\vdash A}{\Gamma ,A\vdash B,\Delta }}$.

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

Resolution Calculus

The resolution calculus for non-normal modal logics introduces the concept of global and local modalities. The formula ${\mathsf {G}}(\varphi )$ denotes global modality of the modal formula $\varphi$, which means that $\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.

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

The LERES rule states that if two propositional names $p$ and $p'$ are equivalent, then $\Box p$ and $\neg \Box p'$ can be eliminated. The G2L rule states that any globally true formula is also locally true.

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.