G4+ — a prover for propositional and first-order logic
Minimal, intuitionistic and classical logic, in Dyckhoff's contraction-free sequent calculus G4, with Otten's nanoCoP as a validity check. Write a formula or a sequent, and run it in SWI-Tinker.
∀x (s(x) → m(x)). ASCII also works: ~ & | => <=> # ![x]: ?[x]: |-.How to read the answer
G4+ tries minimal logic first, then intuitionistic logic, then classical logic, and names the weakest of the three in which the formula is valid. With prove, it gives the proof in the sequent calculus G4 and in natural deduction, as a tree and in Fitch style; in SWI-Tinker, press Ctrl-M to see them rendered. A biconditional is proved in both directions, each in its own logic. A sequent P1, P2 ⊢ C is sent to G4+ as the formula (P1 ∧ P2) → C. Formulas with equality or function symbols are proved by nanoCoP alone, as a connection proof. If no proof is found, G4+ reports it with an SZS status.
| logic | what it adds | example |
|---|---|---|
| minimal | the rules for →, ∧, ∨, ∀, ∃, with ¬A as A → ⊥ | (p → q) → (¬q → ¬p) |
| intuitionistic | ex falso: ⊥ → A | ¬p → (p → q) |
| classical | excluded middle, or double negation elimination | ((p → q) → p) → p |