Hilbert Systems

Origin. Gottlob Frege's Begriffsschrift (1879) is the first: six axioms over implication and negation, with modus ponens as the rule. David Hilbert and Wilhelm Ackermann, Grundzüge der theoretischen Logik (1928), and David Hilbert and Paul Bernays, Grundlagen der Mathematik (I 1934, II 1939), made the format the standard vehicle of metamathematics, which is why it carries Hilbert's name rather than Frege's. Jan Łukasiewicz simplified Frege's axiomatization — one of Frege's axioms is derivable from the others — and his three-axiom basis for classical propositional logic became the textbook standard.

Models. A logic presented as its set of theorems: axiom schemas generate, one or two rules extend, and a proof is a finite sequence in which every line is an axiom instance or follows from earlier lines by a rule. The format's identity is its asymmetry: all logical content sits in the axioms, almost none in the rules. Natural deduction and the sequent calculus were invented against exactly this — Gentzen (1934–35) set out to replace a format remote from how mathematicians argue — and the formats divide the labour: Hilbert systems for proving facts about a logic, Gentzen systems for proving facts inside it.

Formalism.

Format: Axiom schemas + modus ponens. First-order: add generalization — from A infer ∀x A. Modal: add necessitation — from A infer □A.

Modus ponens: A → B A ────────── B

The implicational core: K. A → (B → A) S. (A → (B → C)) → ((A → B) → (A → C)) These two with modus ponens prove every theorem of implicational intuitionistic logic, and they are the types of the combinators K and S, with modus ponens as application.

Łukasiewicz's basis (classical propositional): L1. p → (q → p) L2. (p → (q → r)) → ((p → q) → (p → r)) L3. (¬p → ¬q) → (q → p)

A proof in the format:

1. (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)) [S]
2. p → ((p → p) → p) [K]
3. (p → (p → p)) → (p → p) [1, 2, MP]
4. p → (p → p) [K]
5. p → p [3, 4, MP]

Deduction theorem (Tarski): If Γ ∪ {A} ⊢ B then Γ ⊢ A → B. Proved by induction on the derivation: the axiom and assumption cases use K, the case B = A uses the p → p derivation, the modus ponens case uses S. First-order: generalization in the derivation must not bind a variable free in A. Modal: necessitation applies to theorems, not to assumptions, so the theorem holds for local consequence only.

Normal modal logics, defined Hilbert-style: K = classical tautologies + □(A → B) → (□A → □B), closed under modus ponens, uniform substitution, and necessitation. Every normal system in Modal is a Hilbert system by definition.

Symbols.

Metatheory. The format is built for induction over proofs: with modus ponens as the only rule, a property of theorems is established by checking each axiom schema and one closure case — the shape of soundness proofs, and of the Lindenbaum–Tarski algebraization, which quotients the formula algebra by provable equivalence and reads the axioms as equations. The deduction theorem (Tarski) is the bridge back to reasoning under hypotheses, and under Curry–Howard the bridge is bracket abstraction: Hilbert proofs are combinator terms, natural deduction proofs are λ-terms, and the deduction theorem is combinatory completeness — the principal types of K and S are the two axiom schemas, as recorded in Combinatory Logic. Completeness results belong to the particular logics: Łukasiewicz's basis is complete for classical propositional logic, and the first-order completeness theorem was proved for a Hilbert-style calculus, as recorded in Godel Completeness Theorem. The definition of a normal modal logic is Hilbert-style: a set of formulas containing the K axiom, closed under modus ponens, substitution, and necessitation.

Applies to. Defining logics, modal logics above all. Algebraic logic. Soundness and conservativity arguments by induction over proofs. Combinatory logic and the Curry–Howard correspondence. Textbook presentations of first-order logic.

Limitations. No subformula property and no analyticity: modus ponens invents its premise A, so backward search branches over all formulas at every step, and there is no cut-elimination theorem to prove: translated into sequent form, every modus ponens step is a cut. Proofs are long and unstructured — five lines for p → p — and reasoning under hypotheses must be compiled away through the deduction theorem, whose translation is bracket abstraction and inflates proofs exponentially in the nesting depth of discharged assumptions, as recorded in Combinatory Logic. The format has no notion of open assumption, so everything natural deduction expresses by discharge must be simulated. In modal systems the deduction theorem's failure under necessitation forces the distinction between local and global consequence, a standing source of error in axiomatic modal reasoning. The format answers questions about a logic and resists questions posed inside it: the searchable calculi in Proof-Systems — sequents, tableaux, resolution — exist because this one resists search.

© 2026 Lingenic LLC