G4m and nkm — provers for modal logic
Countermodels, proofs in a labelled G4 sequent calculus (G4m: G4+ for modal logic) with the weakest logic in which the formula is valid, and derivations in labelled natural deduction (nkm, on the core of the temporal prover nkt). Write a formula or a sequent, choose a system, and run it in SWI-Tinker.
v : p and w R v for other worlds. ASCII also works: [] <> ~ & | => <=> # |-. As in G4+, a principal biconditional A ↔ B is proved in its two directions.How to read the answer
The prover first builds a countermodel tree (unsigned, in the style of Jeffrey and Copeland, with worlds as labels). An open branch gives a countermodel, which is checked, and then no derivation exists. If the tree closes, G4m gives a proof in its labelled sequent calculus, in the layout of G4+, and names the weakest logic in which the formula is valid: minimal, intuitionistic or classical. G4m is Dyckhoff's contraction-free G4 at each world, with the modal rules of Simpson's labelled calculus and the frame conditions as a closure of the accessibility relation; at the classical level, as in G4+, the rule IP (indirect proof). Then nkm searches for a derivation in labeled natural deduction and checks it: the rules □I, □E, ◇I, ◇E, and for the frame conditions the relational rules refl, sym, trans, eucl and ser, which discharge relational assumptions. In SWI-Tinker, press Ctrl-M to see the derivation as a tree and in Fitch style; the countermodel tree is given as qtree source.
The Fitch proof follows Fitch's Symbolic Logic (1952, §§ 11–12), with the worlds kept as labels: □ in the margin marks a strict subproof, whose flag is its world, and the relation to that world is implicit. R□ reiterates □A into the strict subproof as A (K); R4 reiterates □A as □A (transitivity: Fitch's own system, S4); □E gives A from □A at the same world (reflexivity: Fitch's nec elim), and ◇I gives ◇A from A there (pos int); ◇E is Fitch's pos elim, which gives ◇C from ◇A and a strict subproof from A to C. Fitch's system stops at S4: for symmetry and euclideanity (B, K5, S5) the relational subproofs stay, with explicit lines w R v. The tree-style derivation is the labelled one of Simpson and Viganò; check “labelled Fitch proof” to write the relations as lines in the Fitch proof as well.
| system | conditions on R | characteristic axiom |
|---|---|---|
| K | none | □(p → q) → (□p → □q) |
| D | serial | □p → ◇p |
| T | reflexive | □p → p |
| B | reflexive, symmetric | p → □◇p |
| K4 | transitive | □p → □□p |
| S4 | reflexive, transitive | T and 4 |
| S5 | reflexive, symmetric, transitive | ◇p → □◇p |
| K5 | euclidean | ◇p → □◇p |
| KD45 | serial, transitive, euclidean | D, 4 and 5 (belief) |
The conditions can be added to any system, for instance K4 with a symmetric R.