Questions: Deduction Theorem for Propositional Logic

Question 1

In a Hilbert-style proof system, you want to show that P → Q is derivable from a set of axioms Γ. The deduction theorem says this is equivalent to which proof task?

• A. Showing that P and Q are both provable from Γ independently
• B. Showing that Q is derivable from Γ together with the hypothesis P
• C. Showing that P → Q is an axiom instance or follows from modus ponens alone
• D. Showing that Q can be derived from P by a single application of modus ponens

Answer: (B)

The deduction theorem states Γ ⊢ φ → ψ if and only if Γ, φ ⊢ ψ. To prove P → Q from Γ, it suffices to assume P as a hypothesis and derive Q — a far more natural proof strategy than constructing a derivation of the implication from scratch. Option A is wrong because deriving P and Q separately says nothing about whether P implies Q. Option D is too restrictive — Q might require many steps from P, not just one modus ponens application.

Question 2

A student applies the deduction theorem to convert a proof of ψ from {Γ, φ} into a proof of φ → ψ from Γ. They then conclude: 'Since I derived ψ assuming φ, I can also conclude that φ is true.' What error have they made?

• A. The deduction theorem requires ψ to follow by modus ponens, not arbitrary derivation
• B. The deduction theorem only converts the proof into φ → ψ; it says nothing about the truth of φ itself
• C. The conclusion is valid — if ψ follows from φ, then both φ and ψ must hold
• D. The deduction theorem cannot be applied when Γ is empty

Answer: (B)

The deduction theorem converts Γ, φ ⊢ ψ into Γ ⊢ φ → ψ — an implication. It says: *if* φ holds, *then* ψ follows. It does not assert that φ actually holds. The proof assumed φ as a hypothesis to derive ψ; that assumption is discharged when the implication is concluded. Confusing 'proved under assumption φ' with 'proved that φ is true' is a category error between object-level truth and meta-level derivability.

Question 3

The deduction theorem is an object-level theorem — it proves a specific formula in propositional logic.

• T. True
• F. False

Answer: False

The deduction theorem is a *meta-logical* result: it is a theorem *about* the ⊢ relation itself, not a formula derivable within propositional logic. It says something about the structure of proofs in a Hilbert system — specifically, that the derivability relation and the implication connective are tightly coupled. Meta-logical results like the deduction theorem, soundness, and completeness belong to a higher level of analysis than the object-language formulas they concern.

Question 4

The deduction theorem compensates for the absence of a hypothesis-discharge rule in Hilbert systems by showing that any proof using hypothesis φ can be mechanically transformed into a proof of the corresponding implication.

• T. True
• F. False

Answer: True

Natural deduction has the →-introduction rule, which lets you discharge a hypothesis φ and conclude φ → ψ as a primitive step. Hilbert systems have no such rule — they rely on axiom schemas and modus ponens only. The deduction theorem recovers this capability as a derived result: by induction on proof length, every step in a derivation of ψ from hypothesis φ can be 'wrapped' in the implication φ → (—), producing a proof of φ → ψ without using φ as a hypothesis. This makes Hilbert systems practically usable for reasoning about conditionals.

Question 5

What does it mean to say the deduction theorem connects the 'object level' and the 'meta level' in logic, and why is this coupling significant?

Model answer: The object level is the system of formulas and derivations within propositional logic — what can be proved. The meta level is reasoning *about* that system — properties of the ⊢ relation itself. The deduction theorem says that a meta-level fact (ψ is derivable from Γ ∪ {φ}) is equivalent to an object-level fact (the formula φ → ψ is derivable from Γ). This means the implication connective → exactly mirrors the derivability relation ⊢, so reasoning inside the logic about implications can substitute for reasoning outside it about derivability.

The significance is practical: it means you can prove implications by doing ordinary proofs with hypotheses, and any such proof can be mechanically converted into a proof of the implication. This coupling is so natural that systems like natural deduction build it in as a primitive rule. In Hilbert systems, the deduction theorem restores this capability as a derived result, making the otherwise austere Hilbert proof system usable for everyday conditional reasoning.