G4m and nkm provers for modal logic

The meaning of \(\Box\) and \(\Diamond\) is given by Kripke’s semantics [3] (a good introduction is Hughes and Cresswell [4]). Think of a set \(W\) of worlds: ways things could be. Between worlds there is a relation \(R\) of accessibility: \(w \mathrel{R} v\) means that \(v\) is possible from the point of view of \(w\) (it is an “alternative” to \(w\)). A pair \((W, R)\) is a frame; a model adds, for each atom \(p\), the set of worlds where \(p\) is true.

The connectives are read at each world as usual: \(A \land B\) is true at \(w\) when \(A\) and \(B\) are both true at \(w\), and so on. The two modal operators look at the accessible worlds:

• \(\Box A\) is true at \(w\) when \(A\) is true at every world \(v\) such that \(w \mathrel{R} v\);
• \(\Diamond A\) is true at \(w\) when \(A\) is true at some world \(v\) such that \(w \mathrel{R} v\).

So \(\Box\) is a “for every accessible world” and \(\Diamond\) a “there is an accessible world”: the two operators behave like the quantifiers \(\forall\) and \(\exists\), restricted to the worlds that \(R\) reaches. This analogy is the key to everything that follows.

Two consequences are worth noting at once.

• If no world is accessible from \(w\), then \(\Box A\) is true at \(w\) for every \(A\) (there is no world where \(A\) could fail), and \(\Diamond A\) is false at \(w\) for every \(A\). A world that sees nothing makes everything necessary and nothing possible.
• \(\Box A\) and \(\neg \Diamond \neg A\) say the same thing (“\(A\) everywhere” and “nowhere not-\(A\)”), and so do \(\Diamond A\) and \(\neg \Box \neg A\). This duality holds in classical logic; we will see in section 5.4 that one half of it is not intuitionistic.

A formula is valid in a frame if it is true at every world of every model on that frame; it is valid in a class of frames if it is valid in each frame of the class.

The system K is the set of formulas valid in every frame. Its characteristic principle is the distribution of \(\Box\) over \(\to\): \[ \Box(p \to q) \to (\Box p \to \Box q). \] (If at every accessible world \(p\) implies \(q\), and \(p\) holds at every accessible world, then \(q\) holds at every accessible world.)

The other systems restrict the class of frames by a condition on \(R\), and each condition makes one more principle valid:

Each line can be understood without any machinery. Take T: if \(w\) sees itself and \(\Box p\) is true at \(w\), then \(p\) is true at every world that \(w\) sees, \(w\) included; so \(p\) is true at \(w\). Without reflexivity this fails: a world that sees nothing makes \(\Box p\) true, whatever \(p\) is, while \(p\) may be false there. We will meet exactly this countermodel in section 4.

The systems are named after their conditions:

S4 and S5 go back to C. I. Lewis; S4 is the logic of necessity in Fitch’s book (see section 6.3 below), S5 the logic of a necessity for which every world is possible from every other one. In the provers the conditions can also be combined freely (for instance K4 with a symmetric relation).

To show that a formula is not valid in a system, it is enough to give one model, on a frame of the right class, with a world where the formula is false: a countermodel. To show that it is valid, one needs a proof. The provers do both, in this order.

The tree tries to build a model where the formula is false. It starts from the denial of the formula at \(w\) and applies rules that say what must then be true. The tree is unsigned, in the style of Jeffrey [8] and Copeland [9]: its lines are labelled formulas and their negations. Each line has a number, and on the right the rule that produced it and the lines it comes from:

A branch closes (×) when it contains a formula and its negation at the same world, or \(\bot\): no model can make it all true. If every branch closes, the formula is valid in the system. If a branch stays open (○) when no rule can add anything new, it describes a model, and that model is a countermodel; the prover checks it on the formula before printing it.

Run it in SWI-Tinker

=== □p → p
    system: N(K) + refl (T)
    Countermodel tree:
    1   w : ¬(□p → p)                             denied conclusion
    2   w R w                                     refl
    3   w : □p                                    ¬→ 1
    4   w : ¬p                                    ¬→ 1
    5   w : p                                     □ 3, 2
    ×  closed: 5, 4

    The countermodel tree closes: valid in every reflexive frame.

Read it line by line. Line 1 supposes the formula false at \(w\). Since the system is T, \(w\) sees itself (line 2). A conditional is false when its antecedent is true and its consequent false (lines 3 and 4). From \(w : \Box p\) and \(w \mathrel{R} w\), the rule □ gives \(w : p\) (line 5), which contradicts line 4: the branch closes, and the formula is valid in every reflexive frame.

Run it in SWI-Tinker

=== □p → p
    system: N(K)
    Countermodel tree:
    1   w : ¬(□p → p)                             denied conclusion
    2   w : □p                                    ¬→ 1
    3   w : ¬p                                    ¬→ 1
    ○  open branch: countermodel

    Countermodel (frame):
      W = {w}
      R = {}
      V(p) = {}
    => not derivable in N(K) (soundness).

In K nothing forces \(w\) to see any world, so the rule □ has nothing to apply to, and the branch stays open. The countermodel is the one announced in section 2.2: a single world \(w\) that sees nothing (\(R\) is empty), where \(p\) is false (\(V(p)\) is empty). There \(\Box p\) is true, since there is no accessible world at all, and \(p\) is false. “Not derivable (soundness)” means: since every derivable formula is valid, a formula with a countermodel cannot be derived. The prover stops here and gives no proof.

Run it in SWI-Tinker

=== □(p ∨ q) → □p ∨ □q
    system: N(K)
    Countermodel tree:
    1   w : ¬(□(p ∨ q) → □p ∨ □q)                 denied conclusion
    2   w : □(p ∨ q)                              ¬→ 1
    3   w : ¬(□p ∨ □q)                            ¬→ 1
    4   w : ¬□p                                   ¬∨ 3
    5   w : ¬□q                                   ¬∨ 3
    6   w R s                                     ¬□ 4 (new world s)
    7   s : ¬p                                    ¬□ 4, 6
    8   s : p ∨ q                                 □ 2, 6
    ├─ 9   s : p                                  ∨ 8
    │  ×  closed: 9, 7
    └─ 10  s : q                                  ∨ 8
       11  w R w                                  ¬□ 5 (existing world w)
       12  w : ¬q                                 ¬□ 5, 11
       13  w : p ∨ q                              □ 2, 11
       ├─ 14  w : p                               ∨ 13
       │  ○  open branch: countermodel
       └─ 15  w : q                               ∨ 13
          ×  closed: 15, 12

    Countermodel (frame):
      W = {s, w}
      R = {w R s, w R w}
      V(p) = {w}
      V(q) = {s}
    => not derivable in N(K) (soundness).

“Necessarily \(p\) or \(q\)” does not imply “necessarily \(p\), or necessarily \(q\)”: it may be that \(p\) holds at some accessible worlds and \(q\) at the others. The tree finds such a model. Line 4, \(w : \neg\Box p\), asks for an accessible world where \(p\) is false: a new world \(s\) (lines 6 and 7). At \(s\), \(p \lor q\) holds (line 8), so the tree branches (lines 9 and 10); the left branch closes. On the right, line 5 asks for an accessible world where \(q\) is false. Before creating a new world, the tree tries the existing ones, to keep the countermodel small: here it takes \(w\) itself (line 11), which is allowed in K. The left sub-branch stays open, and gives the countermodel: \(w\) sees \(s\) and itself, \(p\) is true at \(w\), \(q\) at \(s\). One can check it by hand: every world seen by \(w\) has \(p\) or \(q\), but not every one has \(p\) (\(s\)), and not every one has \(q\) (\(w\)).

G4m proves sequents. A sequent is written \[ G \;;\; \Gamma \vdash x : A \] where \(G\) is a list of relational formulas (the part of the frame known so far), \(\Gamma\) a list of labelled formulas (the assumptions), and \(x : A\) the goal. It reads: “in any model where the relations \(G\) hold and the formulas \(\Gamma\) are true, \(A\) is true at \(x\)”. When \(G\) is empty, it is omitted.

A proof is built from the bottom up: the sequent to prove is at the bottom (in a tree) or at the top (in the text output, where each step is followed, indented, by the sequents it reduces to). Each step replaces the sequent by simpler ones; a branch ends with an axiom (Ax.): the goal is among the assumptions, or (rule L⊥) \(\bot\) is.

The propositional rules are those of G4+, with the same names. Their names say on which side of \(\vdash\) the formula is decomposed (L left, R right) and which connective:

The rules L∧→, L∨→, L→→ are Dyckhoff’s contribution [1]. In a naive calculus, using an implication \(A \to B\) among the assumptions means keeping it while trying to prove \(A\); the same step can then be tried again and again, and the search never ends. G4 looks at the form of \(A\) and replaces the implication by something smaller: \((C \land D) \to B\) by \(C \to (D \to B)\), \((C \lor D) \to B\) by \(C \to B\) and \(D \to B\), and so on. Every step makes the sequent smaller, and the search terminates. (Dyckhoff called his calculus LJT; “G4” is its name in the numbering of Troelstra and Schwichtenberg’s Basic Proof Theory.) This is what G4m inherits from G4+.

The modal rules are the rules of labelled sequent calculi (Negri [7], Simpson [5]); they are the four rules of section 3, read on sequents:

L□→ and L◇→ complete Dyckhoff’s list for modal antecedents; they follow Iemhoff’s construction of G4-style calculi for intuitionistic modal logics [10] [11].

The frame conditions (reflexivity, symmetry, transitivity, euclideanity) are not rules of G4m: they act on \(G\) as a closure. When L□ or R◇ needs \(x \mathrel{R} v\), it may use a relation that follows from \(G\) by the conditions of the system, as in Simpson’s calculus. When it does so, the conditions are written after the rule: L□ (trans) means “the relation used here is not in the sequent, it follows from it by transitivity”. In SWI-Tinker (Ctrl-M) the same information is a subscript, \(L\Box_{\mathrm{trans}}\).

G4m first looks for a proof in minimal logic, then in intuitionistic logic, then in classical logic, and reports the first level at which it succeeds, as G4+ does for first-order formulas.

• Minimal logic has the rules of the connectives and nothing more; \(\bot\) is an atom like the others, and \(\neg A\) abbreviates \(A \to \bot\).
• Intuitionistic logic adds ex falso: from \(\bot\), anything follows (rule L⊥).
• Classical logic adds the excluded middle, or equivalently double negation elimination: from \(\neg\neg A\), conclude \(A\). At this level G4m, like G4+, stays in G4 and adds one rule, IP (indirect proof): to prove \(x : A\), assume \(x : \neg A\) and prove \(x : \bot\).

The intuitionistic level of G4m is intuitionistic modal logic in the sense of Simpson [5]: \(\Box\) and \(\Diamond\) are not defined from each other, and the rules of section 5.2 are those of his labelled sequent calculus. Most of the characteristic principles of section 2.2 are already minimal: K, T, D, B, 4 and 5 need no ex falso and no excluded middle. The differences appear with negation. Three examples:

\(\Box p \to \neg\Diamond\neg p\): run it

--- Intuitionistic logic ---
   ⊢ w : □p → ¬◇¬p   (R→)
    w : □p ⊢ w : ¬◇¬p   (R→)
      w : □p, w : ◇¬p ⊢ w : ⊥   (L◇)
        w R s ; s : ¬p, w : □p ⊢ w : ⊥   (L□)
          w R s ; s : p, s : ¬p, w : □p ⊢ w : ⊥   (L0→)
            w R s ; s : ⊥, s : p, w : □p ⊢ w : ⊥   (L⊥)

The contradiction appears at \(s\) (\(s : \bot\)), but the goal is \(w : \bot\): falsity at the world \(w\). Minimal logic cannot pass from one to the other; ex falso can (L⊥). Hence the intuitionistic level. The same holds, in its simplest form, for \(\Diamond\bot \to \bot\) (run it): a world where \(\bot\) holds makes \(\bot\) hold here, by ex falso only.

\(\neg\Diamond\neg p \to \Box p\): run it

--- Classical logic ---
   ⊢ w : ¬◇¬p → □p   (R→)
    w : ¬◇¬p ⊢ w : □p   (R□)
      w R s ; w : ¬◇¬p ⊢ s : p   (IP)
        w R s ; s : ¬p, w : ¬◇¬p ⊢ s : ⊥   (L◇→)
          w R s ; s : ¬p, w : ¬◇¬p ⊢ s : ¬p   (Ax.)
          w R s ; s : ¬p, w : ⊥ ⊢ s : ⊥   (L⊥)

This is the converse, and it is classical: from “there is no accessible world where \(p\) fails” one concludes “\(p\) holds at every accessible world” only by an indirect proof, at each world. Read the proof: to show \(\Box p\), R□ takes a world \(s\) seen by \(w\); there IP supposes \(s : \neg p\) and looks for a contradiction. The assumption \(w : \neg\Diamond\neg p\) is \(\Diamond\neg p \to \bot\) at \(w\): an implication whose antecedent is a \(\Diamond\)-formula, used by L◇→. Its left branch proves the antecedent \(\Diamond\neg p\) by choosing \(s\), where \(\neg p\) has just been supposed (Ax.); its right branch gets \(w : \bot\), and ex falso closes it (L⊥). Without IP the proof is impossible, so the duality of section 2.1 is intuitionistic in one direction and classical in the other; that is why G4m treats \(\Box\) and \(\Diamond\) as two primitive operators.

Two more examples to try: \(\Diamond(p \lor q) \to \Diamond p \lor \Diamond q\) is minimal (run it); \(\Box(p \lor q) \land \Box\neg p \to \Box q\), the modal disjunctive syllogism, is intuitionistic, because eliminating \(p\) uses ex falso (run it).

Peirce’s law \(((p \to q) \to p) \to p\) is classical, but its double negation is intuitionistic, and so is its necessitation in K:

Run it in SWI-Tinker

--- Intuitionistic logic ---
   ⊢ w : □¬¬(((p → q) → p) → p)   (R□)
    w R s ; ⊢ s : ¬¬(((p → q) → p) → p)   (R→)
      w R s ; s : ¬(((p → q) → p) → p) ⊢ s : ⊥   (L→→)
        w R s ; s : ¬p, s : (p → q) → p ⊢ s : p   (L→→)
          w R s ; s : p, s : ¬p, s : q → p ⊢ s : q   (L0→)
            w R s ; s : ⊥, s : p, s : q → p ⊢ s : q   (L⊥)
          w R s ; s : p, s : ¬p ⊢ s : p   (Ax.)
        w R s ; s : ⊥ ⊢ s : ⊥   (Ax.)

The modal part is a single step: R□ takes a new world \(s\), and \(w \mathrel{R} s\) is then carried along unchanged. Everything above it happens at \(s\), and is, label for label, the proof that G4+ finds for \(\neg\neg(((p \to q) \to p) \to p)\) (run it). This is why the example is instructive: the modal layer is thin, and what shows through is the propositional engine, G4, and what distinguishes it from a G3 calculus.

In the intuitionistic sequent calculus G3 of Troelstra and Schwichtenberg, the rule for an implication among the assumptions keeps it in the left premiss: to use \(A \to B\), prove \(A\) with \(A \to B\) still available, then go on with \(B\). The assumption \(\neg(((p \to q) \to p) \to p)\) must here be used twice: once to reduce the goal \(\bot\) to Peirce’s law, and once more, higher up, under the assumption \(p\), to get \(\bot\) again and hence \(q\) by ex falso. Since the formula stays in the sequent, a search procedure may also use it a third time, a fourth time, and so on: this is where G3 loops.

G4 never uses the same implication twice. Read the first L→→: the assumption \(\neg(((p \to q) \to p) \to p)\), that is \(((C \to D) \to B)\) with \(C = (p \to q) \to p\), \(D = p\), \(B = \bot\), is consumed, and its left premiss receives \(C\) and a smaller formula, \(D \to B = p \to \bot = \neg p\). This residue \(\neg p\) does the work of the second use: three lines higher, L0→ applies it to \(s : p\) and gets \(s : \bot\), and L⊥ gives \(s : q\). The big formula has been replaced by a smaller piece of itself, the sequents get smaller at every step, and the search ends without any loop check. This is Dyckhoff’s idea [1] at work.

The two natural deductions (nkm’s tree, and G4+’s on the propositional formula) show the same fact from the other side: the assumption \([\neg(((p \to q) \to p) \to p)]^1\) is discharged twice. In natural deduction the double use cannot be avoided; G4 compiles it into the rule L→→, and the rule \(\to\to\)E of G4+’s natural deductions is its trace.

One caveat: Negri’s G3K [7] is a classical calculus, with several formulas on the right of \(\vdash\); it proves Peirce’s law directly, and has no need of the double negation. The contrast drawn here is with the intuitionistic G3, at the level where this proof lives.

nkm derives labelled formulas in natural deduction, in the style of Simpson [5] and Viganò [6], on the core of nkt [2]. Its logic is classical: its rule \(\bot\)E concludes \(x : A\) from a derivation of \(\bot\) under the assumption \(x : \neg A\) (reductio ad absurdum). Besides the rules for the connectives (\(\to\)I, \(\to\)E, \(\land\)I, \(\land\)E, \(\lor\)I, \(\lor\)E, \(\bot\)E), it has the four modal rules of section 3 and one rule per frame condition:

Square brackets mark assumptions that the rule discharges: the rule □I, for instance, uses a derivation that may depend on \(w \mathrel{R} s\), and the conclusion \(w : \Box A\) no longer depends on it. The relational rules all have the same shape: “if the frame condition gives you this relation, you may use it as an assumption”. Every derivation found is checked by an independent checker before it is printed.

Axiom D: run it

[w : □p]¹    [w R s]²
────────────────────── □E
        s : p                [w R s]²
─────────────────────────────────────── ◇I
                w : ◇p
──────────────────────────────────────────── ser, 2
                   w : ◇p
───────────────────────────────────────────────────── →I, 1
                     w : □p → ◇p

A tree is read from the top (the assumptions) to the bottom (the conclusion). Each horizontal line is one application of the rule written on its right. The small numbers link an assumption to the rule that discharges it: \([w : \Box p]^1\) is discharged by “→I, 1”, \([w \mathrel{R} s]^2\) by “ser, 2”. Here: assume \(\Box p\) at \(w\) and a world \(s\) seen by \(w\); by □E, \(p\) holds at \(s\); by ◇I, \(\Diamond p\) holds at \(w\). The rule ser says that such an \(s\) exists in every serial frame, so the assumption \(w \mathrel{R} s\) can be dropped; →I discharges \(w : \Box p\). It is the same argument as the G4m proof of section 5.3, read in the other direction.

The Fitch presentation writes the same derivation as a list of numbered lines; an assumption opens a subproof, drawn as a vertical bar with a horizontal stroke under the assumption, and the bar ends when the assumption is discharged. The justification on the right gives the rule and the lines it uses (\(i\)–\(j\) for a subproof).

nkm follows Fitch’s own treatment of necessity, in his Symbolic Logic [12], sections 11 and 12, with the worlds kept as labels. Fitch proves \(\Box A\) with a strict subproof: a subproof marked \(\Box\) in the margin, into which only necessary formulas may be brought (“reiterated”). In nkm a strict subproof is a subproof about a world: its flag, the boxed label \([s]\), is the world it reasons about, and the relation from the outer world to \(s\) is implicit. The rules of Fitch then read as follows:

In Fitch’s book the reiteration of \(\Box A\) as \(\Box A\) is the only one allowed, and his system is essentially S4 (his section 11.9). In section 11.10 he considers a reiteration that drops the box, \(\Box A\) outside and \(A\) inside, which gives a system close to Lewis’s S2; in nkm this reiteration, R□, is the rule of K, and R4 is added only when the relation is transitive. In SWI-Tinker (Ctrl-M) the \(\Box\) of a strict subproof is drawn in the margin, to the left of its vertical bar, as in Fitch’s book, and R□ and R4 are written \(R_\Box\) and \(R_4\).