Hilbert Calculus

Definition

Hilbert Calculus

A Hilbert calculus is a proof system built from axiom schemata and a few inference rules, typically including modus ponens:

The name describes a style of proof system, not one fixed choice of axioms and rules. Different choices can prove the same formulas; the propositional Hilbert calculus is one such choice.

Contrast with Other Calculi

• Hilbert calculus: derives formulas; logical principles are primarily encoded in axiom schemata.
• Sequent calculus: derives sequents , with assumptions and possible conclusions ; logical principles are primarily encoded in connective-specific left and right rules.
• Natural deduction: derives formulas using introduction and elimination rules for connectives; temporary assumptions can be discharged, for example when deriving from a derivation of under assumption .
• Resolution calculus: combines clauses by eliminating complementary literals; deriving the empty clause establishes that the input clauses are unsatisfiable.

Logical structure is encoded in axioms

In the propositional system, every non-axiom line uses the same rule: modus ponens. Reasoning about different connectives comes from choosing axiom instances, rather than applying separate rules for each connective.

Few rules need not mean short proofs: even takes five lines in the displayed proof.

Derived inference rules can shorten proofs: each application stands for a derivation using the primitive axioms and rules. Introduction and elimination rules can be used this way without becoming primitive rules of the calculus.

Variants

Propositional

Definition

Hilbert Calculus ( Propositional Logic)

One Hilbert calculus for propositional logic has the following axiom schemata, for arbitrary formulas :

Its only inference rule is modus ponens. Here, denotes implication.

Link to original