Questions: Hilbert System for Propositional Logic

Question 1

A student attempts to prove φ → φ in a Hilbert system by writing: 'Assume φ; therefore φ. Proof complete.' What is wrong with this reasoning?

• A. Nothing is wrong — any formula that follows from itself is a tautology and is automatically provable
• B. In a Hilbert system the only inference rule is modus ponens; there is no 'assumption' step — a proof must begin from axiom instances and proceed entirely through MP
• C. φ → φ is not a tautology, so the Hilbert system cannot prove it
• D. The student must first prove φ as an independent theorem before using it as a premise

Answer: (B)

A Hilbert proof is a finite sequence of formulas where each is either an axiom schema instance or follows from two earlier formulas by modus ponens. There is no assumption or 'hypothesis discharge' step in a raw Hilbert derivation — that bookkeeping belongs to the deduction theorem, which is a metatheorem. To prove ⊢ φ → φ (as a theorem from no assumptions) requires several steps using axioms K and S, making even this trivial tautology laborious.

Question 2

A logician wants to prove that adding a new axiom schema to propositional logic creates a conservative extension (it proves no new propositional tautologies). Which proof system is most convenient for this metatheoretical investigation?

• A. Natural deduction, because its introduction and elimination rules make explicit proofs easy to construct
• B. A Hilbert system, because all logical content lives in the axioms while the single inference rule keeps structural analysis of derivations simple
• C. Truth tables, because semantic methods are more powerful than syntactic ones for metatheoretical results
• D. Sequent calculus, because its cut-elimination theorem makes all metatheoretical results automatic

Answer: (B)

Hilbert systems isolate all logical content in the axiom schemas — the single inference rule (modus ponens) is structurally uniform. To compare two systems or study what a new axiom adds, you modify the axioms; the derivation structure remains the same. Natural deduction and sequent calculi have multiple rules, adding cases to every inductive argument about proofs. This is why Hilbert systems are the standard tool for metatheory despite being awkward for constructing proofs.

Question 3

The deduction theorem is a metatheorem about the Hilbert system — proved by induction on derivation length — rather than an axiom schema within the system itself.

• T. True
• F. False

Answer: True

The deduction theorem states: if Γ ∪ {φ} ⊢ ψ, then Γ ⊢ φ → ψ. This is not a formula that appears in derivations; it is a statement about derivations. The proof proceeds by induction on derivation length, showing that for each step deriving ψ from Γ ∪ {φ}, you can construct a corresponding derivation of φ → (that step) from Γ alone — using K for axiom and assumption base cases, and S for the modus ponens inductive step. Because it is a metatheorem, it lets you use hypotheses as a shorthand, but it does not live inside the formal system.

Question 4

Because the Hilbert system has mainly one inference rule (modus ponens), it can derive mainly a limited subset of propositional tautologies and is therefore incomplete.

• T. True
• F. False

Answer: False

Despite having only modus ponens as an inference rule, a Hilbert system with axiom schemas K, S, and DN is complete for propositional logic: every propositional tautology is derivable. The axiom schemas carry all the combinatorial logical content. Soundness holds because each schema is a tautology and MP preserves tautologies. Completeness requires a separate proof (e.g., via maximal consistent sets). The minimalism of the rule apparatus makes the system awkward to use but does not restrict what is provable.

Question 5

In your own words, explain why Hilbert systems are described as 'awkward for finding proofs but powerful for proving metatheorems about proofs.' Give one example of each side of this tradeoff.

Model answer: They are awkward because every proof step must be either an axiom instance or an application of modus ponens — there are no shortcut rules for conjunctions, disjunctions, or hypothetical assumptions. Even proving φ → φ requires multiple steps. They are powerful for metatheory because every derivation has exactly the same one-rule structure, making inductive arguments about all derivations clean: you only ever need to handle the 'axiom instance' and 'modus ponens step' cases.

As a metatheory example: proving the deduction theorem requires induction over derivation structure. With one rule, there are only two inductive cases to handle. In natural deduction, there would be a separate case for each introduction and elimination rule (∧I, ∧E, →I, →E, etc.), making the induction far more complex. The Hilbert system trades ergonomics for structural simplicity — a worthwhile exchange when you are studying the logic rather than reasoning within it.