Note for Modal Logic

Mainly from Frank Pfenning 15-816 Modal Logic. This note is surely incomplete and contain errors. Please let me know if you find any mistakes.

Proposition

• Verification: we can construct it, introduction
• May be used: how to use it, elimination
• Propositional logic: Proposition is true or false, with connnectives AND, OR, NOR, etc
• Predicate logic: Use quantifier variables over the objects. For example, ∀x, if x is human, then x is mortal, $\forall x$ is a quantifier, $x$ is variable, ... is human and ... is mortal are predicates.
• Second-order logic: Use quantifier variables over the properties/relations, $\forall P, (\forall x, P(x) \implies P(Socrates))$

$\Box$ Necessity

Comp: A $\supset$ B $\equiv$ if A then B Valid/Necessity: A is valid if A true that does not require any assumptions, aka “true in all models”.

\[\Box A\ \cdot \vdash A\ true \to A\ valid\]

$\cdot \vdash A\ true$ determine the validity of $A$, but we want to reasoning question like If A ⊆ B valid and A valid, is B valid?, so we try to use $\Box A$ to represent a proposition like A is valid in all models.

\[\frac{\cdot \vdash A\ true}{\Gamma \vdash \Box A\ true} \quad (\Box-I_2)\]

Difference

• $\Box A$: A proposition that A is true in all possible models, may or may not be true in current model depending on your system.
• $A\ true$: A is true in the current model.
• $\Box A\ true$: A is true in all models.

Elimination is not trivial, because it requires $\Gamma$ to be empty. So we introduce $A\ valid$ as a new form of assumption.

\(B_1\ valid \in \Delta;\) \(A_1\ true \in \Gamma\)

\[\frac{\Delta; \Gamma \vdash \Box A\ true \quad (\Delta, u :: A\ valid);\Gamma \vdash C\ true}{\Delta; \Gamma \vdash C\ true} \quad (\Box-E^u)\] \[\frac{\Delta; \cdot \vdash A\ true}{\Delta; \Gamma \vdash \Box A\ true} \quad (\Box-I)\]

To use the hypotheses $A\ valid$, we need to introduce a new rule $u$.

\[\frac{u::A\ valid \in\Delta}{\Delta; \Gamma \vdash A\ true} \quad (u)\]

Since proof and program are the same, the previous rules can be used to prove theorems.

\[\frac{u::A\in\Delta}{\Delta; \Gamma \vdash u : A} \quad (u)\] \[\frac{\Delta; \cdot \vdash M:A}{\Delta; \Gamma \vdash \textbf{box} M : \Box A} \quad (\Box-I)\] \[\frac{\Delta; \Gamma \vdash \textbf{box} M : \Box A \quad (\Delta, u::A);\Gamma \vdash N:C}{\Delta; \Gamma \vdash \textbf{let box}\ u = M\ \textbf{in}\ N:C} \quad (\Box-E)\]

Axioms

\[\begin{align*} \lambda x: \Box A. \textbf{let box}\ u = x\ \textbf{in}\ u : \Box A \supset A\\ \lambda x: \Box A. \textbf{let box}\ u = x\ \textbf{in}\ \textbf{box\ box}\ u : \Box A \supset \Box \Box A\\ \lambda x: \Box(A \supset B). \lambda y: \Box A. \textbf{let box}\ u = x\ \textbf{in}\ \textbf{let box}\ v = y\ \textbf{in}\ \textbf{box box}(u\ v) :\\ \Box(A \supset B) \supset \Box A \supset \Box B \end{align*}\]

Staged Computation

One of the possible interpretations of $\Box A$ is that it represents `source code’ of type $A$. Consider the function $\exp(n, b)$ that computes $b^n$. Following two functions will take another integer $b$ as base number, and return $b^n$:

\[\begin{align*} \exp(0) &= \lambda b.1 \\ \exp(s(n)) &= \lambda b. b * \exp \, n \, b \\ \\ \exp'(0) &= \lambda b.1 \\ \exp'(s(n)) &= \mathbf{let} \; f = \exp' \, n \; \mathbf{in} \; \lambda b. b * f \, b \end{align*}\]

If we call them with $s(s(0))$, first one give back an a closure:

\[\exp\bigl(s(s(0))\bigr) \longrightarrow^{*} \lambda b_2 . b_2 * \exp\bigl(s(0)\bigr) b_2\]

The second one evaluates all the way to 0 first, and then returns a function that does not depends on the exponent anymore, it will read the base number as $b_2$ and compute the result directly:

\[\begin{align*} \mathrm{exp}'\bigl(s(s(0))\bigr) &\quad \longrightarrow^{*} \quad \lambda b_2 . b_2 * \bigl(\lambda b_1 . b_1 * (\lambda b_0 . 1) b_1 \bigr) b_2 \\ &\quad \Longrightarrow^{*}_R \quad \lambda b_2 . b_2 * (b_2 * 1) \end{align*}\]

We would like to use necessity to design a type system that can fail the type check for first one because it does not carry out the computation require $n$, and allow the second one. The small-step semantic connects necessity to staged computation is in lecture note 04. $A\ true$ is a value that is already evaluated to true, $A\ valid$ is a source code of type $A$. $\Box M$ means that $M$ is a wrapped expression, instead of executing $M$ directly, we treat it like a value that can be stored and passed around. $\mathbf{let box}\ u = M\ \textbf{in}\ N$ means that we are going to evaluate $M$ first, and then use the result $u$ to compute $N$. So in the previous example, the type of $\exp$ is \(\exp : \mathbb{N} \to \Box(\mathbb{N} \to \mathbb{N})\) Here, implication $\supset$ is identified with function construction $\to$. First version of $\exp$ is not a valid term in this type system, because inside the body it refer to first argument which is $n$. Second version of $\exp’$ can be rewritten as: \(\exp'(s(n)) = \mathbf{let\ box} \; f = \exp' \, n \; \mathbf{in} \; \lambda b. b * f \, b \\\)

During the compilation, we need to unpack the box and generate the code (like marco in C/C++), so we need to refer to $\Box-E$:

\[\begin{align*} eval &= \lambda x\!:\! \Box\ A. \mathbf{let\ box} \; u = x \; \mathbf{in} \; u\\ &: \Box A \to A \end{align*}\]

The following is useful for metaprogramming:

\[\begin{align*} \text{quote} & = \lambda x\!:\! \Box A.\ \textbf{let } \textbf{box } u = x\ \textbf{in box box}\ u\\ \text{quote} & : \Box A \rightarrow \Box \Box A\\\\ \text{apply} & = \lambda x\!:\! \Box (A \rightarrow B).\ \lambda y\!:\! \Box A.\ \textbf{let box } u = x\ \textbf{in}\\ & \qquad\quad \textbf{let box } w = y\ \textbf{in box (} u\ w \textbf{)}\\ \text{apply} & : \Box (A \rightarrow B) \rightarrow \Box A \rightarrow \Box B \\ \end{align*}\]

Quote will unpack a boxed expression and return a double-boxed expression, apply will unpack two boxed expressions and apply the first one to the second one, wrapping the result back to a boxed expression. Further applications like regex matching, parser generator, intepreter, matrix multiplication, these error-prone, long and tedious tasks can be done in a staged way.

$\Diamond$ Possibility

In classical modal logic, possibility is defined as the negation of neg necessity. \(\Diamond A := \neg \Box \neg A\)

From the perspetives of multi-worlds interpretation of modal logic, any proposition $A$ is possible:

\[\frac{\Delta;\Gamma \vdash A\ true}{\Delta;\Gamma ;\vdash A\ possible} \quad (\text{poss})\] \[\frac{\Delta;\Gamma \vdash A\ possible}{\Delta;\Gamma \vdash \Diamond A\ true} \quad (\Diamond-I)\] \[\frac{\Delta;\Gamma \vdash \Diamond A\ true \quad (\Delta, u::A\ true);\Gamma \vdash C\ possible}{\Delta;\Gamma \vdash C\ possible} \quad (\Diamond-E)\]

Axioms

• $A \supset \Diamond A$: Truth is stronger than possibility.
• $\Diamond \Diamond A \supset \Diamond A$: If we iterate possibility, we obtain an equivalent proposition.
• $\Box (A \supset B) \supset \Diamond A \supset \Diamond B$: We need to add $\Box$ before $(A \supset B)$, otherwise it only means $(A \supset B)$ is true in the world at $(A \supset B)$, it may not true in the possible world where $A\ true$. $\Box$ make sure that $A \supset B$ is true in all the worlds including the possible world where $A\ true$, and then $B\ true$.

Verification, Uses, Monads and Computational Effects

One of the possible interpretations of $\Diamond$ is that it represents a computation that may contains effects. $A \cdot!\uparrow!\cdot$: if there is a Verification of $A\ poss$.

\[\frac{\Delta;\Gamma \vdash A \cdot\!\uparrow\!\cdot}{\Delta;\Gamma \vdash \Diamond A\uparrow} \quad (\Diamond-I)\] \[\frac{\Delta;\Gamma \vdash \Diamond A\downarrow \quad \Delta; u::A\ true \vdash C \cdot\!\uparrow\!\cdot}{\Delta;\Gamma \vdash C\ \cdot\!\uparrow\!\cdot} \quad (\Diamond-E)\]

$E \div A\ poss$(abbreviation as $E \div A$): E is a proof of $A\ poss$. We also give proof terms for $\Diamond$.

\[\frac{\Delta;\Gamma \vdash M:A\ true}{\Delta;\Gamma \vdash M \div A\ poss} \quad (\text{poss})\]

This means any proof term $M$ is also a proof expression. We can construct a proof expression of $\Diamond A$.

\[\frac{\Delta;\Gamma \vdash M \div A\ poss}{\Delta;\Gamma \vdash \textbf{dia} M : \Diamond A\ true} \quad (\Diamond-I)\]

We can also destruct a proof expression of $\Diamond A$, and obtain a proof of $A\ true$, and use it to construct a new proof expression of $C\ poss$.

\[\frac{\Delta;\Gamma \vdash \textbf{dia} M : \Diamond A\ true \quad \Delta; u::A\ true \vdash E:C\ poss}{\Delta;\Gamma \vdash let\ \textbf{dia} u = M\ \textbf{in}\ E \div C\ poss} \quad (\Diamond-E)\]

Notice previous $\Diamond-I$ we use $\textbf{dia}$ to pack a possible expression with type $A$ as type $\Diamond A$, and in $\Diamond-E$ we use $\textbf{dia}$ to destruct an expression with type $\Diamond A$, and then use it to construct a new possible expression $C\ poss$ with type $C$. Think of expression $E \div A\ poss$ as effectful computation that possibly returning a value of type $A$. $\Diamond A$ is a pure term that evaluating a value dia$E$ where $E$ is a possible effectful computation that returns a value of type $A$, this is monadic:

• $A \supset \Diamond A$ wrap a value to a computation.
• $\Diamond \Diamond A \supset \Diamond A$ take a computation possibly returns a dia value which is an another computation that possibly returns a value, wrap it to dia and return it.
• $\Box (A \supset B) \supset \Diamond A \supset \Diamond B$ is the bind operation, it takes a computation that possibly returns a value of type $A$, and a pure function that takes a value of type $A$ then returns a value of type $B$, and returns a computation that possibly returns a value of type $B$.

Classical Modal Logic

I \models A$: If formula $A$ (expression such as $P \rightarrow Q$) holds in interpretation $I$ (give $P, Q$ real meaning). This is more a semantic definition. Classical modal logic still accepts the classical axiom law of excluded middle (LEM). It also accepts bunch modes of truth such as true, necessarily true, possibly true, possible false, false. $\Box_i \phi$: man $i$ knows that formula $\phi$ holds true, $\Box_i$ is a modality. To use the system to reason something, we first need to allow all classical propositional logic $(P)$. We know all tautologies and all basic rules, and they are true, so we have generalization rule:

\[\frac{\phi}{\Box \phi} \quad ((G))\]

If we know $\phi$, and we know $\phi$ implies $\psi$, then we know $\psi$, this is modus ponens, an instance of the Kripke axiom:

\((MP)\quad (\Box \phi \land \Box (\phi \to \psi)) \to \Box \psi\) it can also be written as: \((K)\quad \Box (\phi \to \psi) \to (\Box \phi \to \Box \psi)\)

We also add two axioms into the system, which make sense in the context of knowledge:

\[\begin{align*} (T)\quad & \Box \phi \to \phi \\ (4)\quad & \Box \phi \to \Box \Box \phi \end{align*}\]

First axiom $T$ means if we know $\phi$, then $\phi$ is true, this means we are not allowed to know falsehood. Second axiom $4$ means if we know $\phi$, then we know that we know $\phi$, this means that if we know something, we will not forget it in the future. S4: the system with all the above axioms: $(P), (G), (K), (T), (4)$.

classical propositional logic

Propositional modal formulas: Given $\Sigma$ a set of propositional variables, we can construct a smallest set of propositional modal formulas by propositional logic and modal logic as follows:

• If $A \in \Sigma$, then $A \in Fml_{PML}(\Sigma)$.
• If $\phi, \psi \in Fml_{PML}(\Sigma)$, then $\neg \phi, \phi \land \psi, \phi \lor \psi, \phi \to \psi \in Fml_{PML}(\Sigma)$.
• If $\phi \in Fml_{PML}(\Sigma)$, then $\Box \phi, $\Diamond \phi \in Fml_{PML}(\Sigma)$.

Provability: let S be a system of modal logic, i.e. a set of proof rules and axioms, for a formula $\phi$ and a set of formulas $\Phi$, we say $\phi$ is provable in S from $\Phi$, written as $\Phi \vdash_S \phi$, if and only if there is a proof of $\phi$ only use S and $\Phi$.

Gödel Translation

Intuitionistic logic’s central constructions are about justification and preservation of justification. For the formula of law of excluded middle (LEM), since we (usually) do not have a justification of either $A$ or $\neg A$, we cannot use LEM in intuitionistic logic. The “justification” here maps to the “knowledge” in modal logic. Therefore, we can use the Gödel translation to translate intuitionistic logic to modal logic by prefixing all formulas with $\Box$, which means `provable’. Since we have the provability interpretation of $\Box$, we look at the previous axioms again:

• $(K)$: If $\phi \to \psi$ is provable, and if $\phi$ is provable, then $\psi$ is provable.
• $(T)$: If $\phi$ is provable, then $\phi$ is true.
• $(4)$: If $\phi$ is provable, then it is provable that $\phi$ is provable.
• $(G)$: If we have proven $\phi$, then $\phi$ is provable.
• We say that $\phi$ is provable instead of true, because of the Gödel’s incompleteness theorems, which states that there are true statements that cannot be proven in a system.

Kripke Semantics

• Kripke frame: is a pair $(W, \rho)$, where $W$ is a non-empty set of worlds and $\rho$ is a binary relation $W \times W$ which means the accessibility relation between worlds.
• Kripke structure: a triple $(W, \rho, v)$, where $(W, \rho)$ is a Kripke frame and $v$ is a mapping function that given a world $w \in W$ and a propositional variable $p \in \Sigma$, return a truth value $v(w, p) \in {true, false}$.
• interpretation: Given a Kripke structure $K = (W, \rho, v)$, the interpretation $\models$ in a world $s$ is defined as follows:
  1. $K, s \models A$ if and only if $v(s, A) = true$.
  2. $\land, \lor, \neg$ pretty much the same as the other semantic logic.
  3. $K, s \models \Box A$ if and only if $\forall$ accessible worlds $t$ from $s$ such that $s \rho t$, $K, t \models A$.
  4. $K, s \models \Diamond A$ if and only if $\exists$ an accessible world $t$ from $s$ such that $s \rho t$ and $K, t \models A$.

Soundness and Correspondence

Soundness

A modal logic system S consists of a set of axioms and rules of inference is externally sound if and only if for every formula $\phi$ and all sets of formulas $\Phi$, \(\Phi \vdash_S \phi \implies \Phi \models \phi\) In order to prove the soundness of a modal logic system S, we need to show that every axiom and rule of inference is sound, which means they are valid for all instances. Most of the axioms can be proved by induction simply, but we cannot prove the soundness of $(T)$ with respect to Kripke semantics, this issue exists in the other modal axioms as well, like how axiomatic and semantic systems are related.

Correspondence

Correspondence theory try to find the relationship between properties of Kripke frames and formulas in modal logic that are valid in all Kripke structures with those properties.

Lemma (Kripke Frame reflexive) A Kripke frame $(W, \rho)$ is reflexive if and only if

\[\forall K = (W, \rho, v), \forall s \in W, K, s \models \Box A \to A\]

This lemma says that the class of all reflexive Kripke frames is characterized by the formula $\Box A \to A$. Why reflexivity is important? Consider the case where we have a world $s$ where there is no accessible world from $s$ and $A$ is not true in $s$. $\Box A$ is vacuously true. Charaterization means that given a class of Kripke frames and a formula, the formula is valid in Kripke structure consists of those frames and all mappings.

Lemma (Kripke Frame transitive) > $\Box q \to\ \Box \Box q$ characterized by the class of all transitive Kripke frames.

Theorem > S4 are sound for the class of all reflexive and transitive Kripke frames.

Intuitionistic Kripke Semantics

We give an intuitionistic perspective on the typically classical Kripke structures. We revise the basic judgement from $A\ true$ to $A\ @\ w$, where $w$ is a world in the Kripke structure, to indicate that `there is a proof/knowledge of $A$ at world $w$’. The elimination rules in propositional connectives are used to move between worlds. The judgement $w\ \leq\ w’$ means that $w’$ is accessible from $w$.

Necessity in modal connectives To show $\Box A$ is true at world $w$, we need to show that $A$ is true at all worlds $w’$ that are accessible from $w$. We model this by assuming/introducing a new world parameter $\alpha$ and verifying that $A$ is true at $\alpha$, knowing only that $\alpha$ is accessible from $w$.

\[\frac{ \frac{}{\text{judgement not proposition}} (w \leq \alpha) \quad \frac{\cdots some\ reasoning \cdots}{A\ @\ \alpha} } {\Box A\ @\ w} \quad (\Box-I^\alpha)\]

The elimination rule for necessity is similar, if $\Box A$ is true at $w$, then we can conclude that $A$ is true at any world $\alpha$ that is accessible from $w$.

Possibility in modal connectives To show $\Diamond A$ is true at world $w$, we need to show that there exists a world $w’$ that is accessible from $w$ such that $A$ is true at $\alpha$.

\[\frac{w\ \leq\ w' \quad A\ @\ w'}{\Diamond A\ @\ w} \quad (\Diamond-I)\]

Now, in elimination rule, we need to assume that $A$ is true at some reachable world $w’$. We parametric in $\alpha$ and assume $w\ \leq\ \alpha$ and $A\ @\ \alpha$, and introduce another world $w’’ \neq w$ that is accessible:

\[\frac{ \frac{w\ \leq\ \alpha \quad A\ @\ \alpha \quad \cdots some\ reasoning \cdots}{C\ @\ w''} (x) \quad \Diamond A\ @\ w } {C\ @\ w} \quad (\Diamond-E^{\alpha, x})\]

To prove our familiar axioms, we need to add more rules to the system. For example, to prove $\Box(A \supset B) \supset \Box A \supset \Box B$, we expect the reflexivity that $\Box A \to A$, to prove $\Diamond\Diamond A \to \Diamond A$, we expect the transitivity. We can use following rules to construct intuitionistic modal logic systems like IK, IT(refl), I4(trans), IS4(refl&trans), I5(sym), IS5(refl&trans&sym).

\[\frac{x : A\ @\ w \in \Gamma}{\Gamma \vdash x : A\ @\ w} \quad (\text{Hyp})\] \[\frac{\Gamma, w \leq \alpha \vdash M : A\ @\ \alpha}{\Gamma \vdash \Lambda w \leq \alpha. M : \Box A\ @\ w} \quad (\Box I)\] \[\frac{\Gamma \vdash M : \Box A\ @\ w \quad \Gamma \vdash w \leq w'}{\Gamma \vdash M[w \leq w'] : A\ @\ w'} \quad (\Box E)\] \[\frac{\Gamma \vdash w \leq w' \quad \Gamma \vdash M : A\ @\ w'}{\Gamma \vdash \langle w \leq w' \rangle M : \Diamond A\ @\ w} \quad (\Diamond I)\] \[\frac{\Gamma \vdash M : \Diamond A\ @\ w \quad \Gamma, w \leq \alpha, x : A\ @\ \alpha \vdash N : C\ @\ w''}{\Gamma \vdash \text{let } \langle w \leq \alpha \rangle x = M \text{ in } N : C\ @\ w''} \quad (\Diamond E)\]

Distributed Programming

The connectivity between worlds in intuitionistic Kripke semantics can be interpreted as the communication channels between hosts. A value $V!:!\Box A$ is a mobile computation that can be sent to another reachable host, $V!:!\Diamond A$ is the address of a remote value of type $A$ at some reachable host. The reference to a remote value, a promise, may be mobile, but the remote value itself is not. The interpretation here can be a structural operational semantics. If we have a term $M$ of type $A$, we either evaluate it locally to obtain a value $v!:!A$, or just return $v!:!A$, otherwise, the computations cont F are represented as a stack of frames that each of them represents a computation steps described by $F$ when a value is returned to it. Variables are bounds by !bind x$V$. As we can see in the rules, all this part of computations are local. For $\Box A$, the source code $M$ is either

• Flows from w’ to w(in the reverse direction of relation)
• Is already located a $w$ which is the result of compilation an static distribution of the program

$\Diamond A$ is more complex, since it is a reference to a remote value that we don’t know where it is and not accessible from current world $w$.

\[\begin{align*} &\text{eval}\big(\text{let}\langle w \leq \alpha \rangle x = M \text{ in } N \big) w'' \quad \to \quad \text{eval}\, M\, w \bullet \text{cont}\big(\text{let}\langle w \leq \alpha \rangle x = \_ \, \text{in } N \big) w'' \\ &\text{eval} \langle w \leq w' \rangle M' \rangle w \quad \to \quad \text{eval}\, M' \, w' \bullet \text{cont} \langle w \leq w' \rangle \\ &\text{ret}\, V' \, w' \bullet \text{cont} \langle w \leq w' \rangle \_ ) \quad \to \quad \exists x .!\text{bind}\, x \, V' \, w' \bullet \text{ret} \langle w \leq w' \rangle x) w \\ &\text{ret} \big(\langle w \leq w' \rangle x \big) w \bullet \text{cont} \big( \text{let} \langle w \leq \alpha \rangle x = \_ \text{in } N \big) w'' \quad \to \quad \text{eval} \big([w'/\alpha] N \big) w'' \end{align*}\]

First rule is the evaluation of a remote value $M$ at world $w$, and send it to the continuation $N$ at world $w’’$. Second rule evaluate a remote value $M’$ at world $w’$, and we keep the continuation. Third rule create a binding to a remote value $V’$ at world $w’$, then return the reference to this remote value. Fourth one is how we use the reference to a remote value $x$. after the return statement, we substitute the local variable $x$ with the remote reference $\langle w \leq w’ \rangle x$ in the continuation $N$, and since now we know where it comes from, we substitute $\alpha$ with $w’$ in $N$ and evaluate it at $w’’$. The issue in fourth rule is that it doesn’t require $w\ \leq\ w’’$. One way to restrict this is using modal logic IS5, which requires IS4 to be symmetric, another way is using a technique called tethering.

Semantics for Validity

Examples in Multiple-World Intuitionistic Modal Logic

\[\begin{align*} K^\Diamond &: \square(A \supset B) \supset (\Diamond A \supset \Diamond B)\ @\ h \\ &= \lambda x\ @\ h. \lambda y\ @\ h. \mathbf{let} \langle h \leq \alpha \rangle z = y \ \mathbf{in} \ \langle h \leq \alpha \rangle ((x[h \leq \alpha]) z) \end{align*}\]

The function $K^{\Diamond}$ takes a mobile function $x$ and a reference to a remote value at some world $\alpha$, moves $x$ to $\alpha$, applies it there, and returns a reference to the answer here.

\[\begin{align*} 4^{\Diamond} &: \Diamond \Diamond A \supset \Diamond A \\ &= \lambda x\ @\ h.\mathbf{let} \langle h \leq \alpha \rangle y = x\ \mathbf{in}\ \mathbf{let} \langle \alpha \leq \beta \rangle z = y\ \mathbf{in}\ \langle h \leq \beta \rangle z \end{align*}\]

The function $4^{\Diamond}$ takes a reference to a remote reference to a value $V$ of type $A$ at some world $\beta$ and return a direct reference to $V$.

Disjunction creates the the necessity for an effect at a distance. Observe that in the very first rule (eval/case) there is a non-local transfer of control, from $w’’$ to $w$, even though $w’’$ and $w$ may not be interaccessible. In order to effect this transfer, the case construct should be annotated with the location of $M$ by adding one bit of information need to be communicated from $w$ to $w’’$ so that the appropriate branch can be selected at $w’’$. We would like the $\Box$ internalize the judgement of validity, so that it coincide with the intuitionistic notion of validity. We use sequent $\Gamma^{\leq}$ to denote the hypotheses in $\Gamma^{\leq}$ that $w’$ is accessible from w according to the current assumptions about the accessibility relation, and $\Psi$ for context of reachable hypotheses. But $ (\Diamond A \supset \Box B)\supset \Box (A\supset B)$ show that the rules are incomplete with respect to IS4.

Judgemental S4

So we introduce Judgemental S4, we first have the axioms for intuitionistic logic and modus ponens, we need to add the rule of necessitation for $\Box$:

\[\frac{\vdash A}{\vdash \Box A} \quad (\text{Nec})\]

and K, T, 4 for both $\Box$ and $\Diamond$. Compared to IS4, JS4 doesn’t have the followings:

\[\begin{align*} \Diamond \lor : \quad \Diamond (A \lor B) \supset \Diamond A \lor \Diamond B \\ \Diamond \bot : \quad \Diamond \bot \supset \bot \\ \Diamond \Box : \quad (\Diamond A \supset \Box B) \supset \Box (A \supset B) \end{align*}\]

In IS4, semantically, $\Diamond A \lor \Diamond B$ agree that if either $A$ or $B$ is possible, then at least one of them must be true. But since we want to construct a validation for either $\Diamond A$ or $\Diamond B$ in JS4, we cannot allow this disjunction to be valid. Similar idea applies to $\Diamond \bot$ and $\Diamond \Box$.