a terminal engine for formal logic practice
logic26 is a terminal program for practicing formal logic in the Kalish–Montague natural deduction system. It presents derivation and symbolization exercises as sequences of checkable moves: the user enters a move, the engine expands the work, validates the rule, and keeps the developing exercise visible on screen.
The exercises and workflow follow UCLA's Logic 2010, reworked as a fast, keyboard-driven interface in the spirit of vim: modal editing, single-key moves, and command-line saves. It is free and runs anywhere a terminal does.
Proof problems are worked by entering compact moves for premises, show-lines, rule applications, and discharges. The engine infers each resulting formula from the cited lines, validates the rule, manages nested show-line scopes, and boxes and cancels completed subderivations.
show conc
pr1
pr2
2 3 mt
4 dd
The rule set covers the full course sequence: propositional rules and derived rules, quantifier rules with their variable restrictions, the identity rules (self-identity, symmetry, and Leibniz's Law, including partial-occurrence replacement), and the definite-description rules for proper and improper ℩-terms. A theorem library makes previous results citable — in the honest way: a theorem must be proven before it can be used in later work. Cited theorems apply schematically, as in Logic 2010: free variables match arbitrary terms, bound variables rename to alphabetic variants, and predicate letters take whole formula schemes — typed out, inferred from the cited lines, or filled in through a stepped prompt.
Symbolization problems ask the user to translate an English sentence into logical notation — not by typing a finished answer, but by reducing the sentence through visible operations: split off a conditional, a conjunction, a negation, a quantifier; edit the remaining text; and atomize a piece only when it matches the problem's legend of sentence letters, predicates, and names.
Every dog barks.
∀x (x is a dog → x barks)
∀x(Dx → Bx)
The engine handles the full language: sentence letters, many-place predicates, quantifiers, identity, and operation terms. Finished formulas are checked by logical equivalence, decided by exhaustive model checking — truth tables for propositional formulas, all small-domain interpretations for quantified ones — so any formula that says the same thing as the expected answer is accepted, whatever its form. Reading "every sweet is good" as ∼∃x(Hx ∧ ∼Fx) counts.
The interface is a full-screen modal TUI. A vim-style front screen lists the problem chapters with per-problem completion marks; progress is saved with :w and restored when a problem is reopened, and a searchable rule reference is one keystroke away from anywhere. Beyond the fixed exercises, both modes have a sandbox: enter any sequent to attempt a derivation, or any sentence with a legend to practice symbolization.
The engine and problem library are substantially complete. The library holds 897 exercises from the Logic 2010 problem set — 567 derivation problems and 330 symbolization problems spanning the course's six chapters, from propositional logic through definite descriptions — and every symbolization exercise now checks against an answer key. Exercises with special instructions display them alongside the sentence.
The whole library is verified mechanically: every problem must load, open cleanly in its engine, and replay its stored solution to completion. The answer keys have been vetted three further ways — each key is checked for well-formedness against its problem's legend; the readings of each ambiguous sentence are confirmed logically distinct (and the fifteen exercises whose English sentences are genuine logical truths, the classic identity truths among them, are verified as exactly that); and every key has been re-read against its English sentence. One honest caveat remains: most keys were newly authored for logic26 rather than recovered from original data, so play-testing may still surface an occasional contested reading.
Play-testing — working through the exercise set in the interface itself, the one kind of vetting no automated check can substitute for.
Interface polish — command completion and per-user progress profiles.
Release — packaging logic26 for anyone to install and run, as a free companion to the logic material on this site.
© Logicae. A logic reference project.