Questions: Soundness Theorem and Validity of Proof Systems

Question 1

A formal proof system derives φ from premises Γ (written Γ ⊢ φ). What does soundness guarantee about this derivation?

• A. That φ is a tautology — true in all models regardless of what Γ says
• B. That Γ ⊨ φ — every model satisfying all formulas in Γ also satisfies φ
• C. That Γ ⊢ φ can also be derived in every other proof system
• D. That Γ is itself consistent and contains no contradictions

Answer: (B)

Soundness says: if there is a formal derivation Γ ⊢ φ, then Γ ⊨ φ (semantic consequence). The proof system never derives a false conclusion from true premises. Option A is wrong — soundness does not require φ to be a tautology; it only guarantees φ is true in every model of Γ. A tautology is true in all models unconditionally; a semantic consequence is true in all models that happen to satisfy Γ. Soundness is the 'safety' direction: ⊢ implies ⊨.

Question 2

Gödel's incompleteness theorems show that certain true statements about natural numbers cannot be proved within Peano arithmetic. What does this imply about the soundness of first-order logic?

• A. First-order logic is unsound for sufficiently complex theories — it eventually derives false statements
• B. First-order logic is incomplete — there are valid formulas in the language that no proof system can derive
• C. Nothing about soundness — incompleteness is about specific theories lacking the power to prove all their truths; first-order logic itself remains sound and (by Gödel's completeness theorem) complete
• D. The proof system for Peano arithmetic must be unsound, since it fails to prove things that are true

Answer: (C)

Gödel's incompleteness theorems apply to specific sufficiently strong *theories* (like Peano arithmetic with its fixed axioms), not to first-order logic as a proof system. First-order logic's proof calculus is sound (Γ ⊢ φ implies Γ ⊨ φ) and complete (Γ ⊨ φ implies Γ ⊢ φ) — this is Gödel's *completeness* theorem. The *incompleteness* theorems say that Peano arithmetic as a theory cannot prove all truths about natural numbers within that theory's fixed axioms. The logic itself is fine; the particular theory doesn't have enough axioms to prove everything true in its intended model.

Question 3

Soundness is the forward direction of correctness: if a formula is provable (⊢ φ), then it is valid (⊨ φ).

• T. True
• F. False

Answer: True

Soundness is precisely this forward implication: ⊢ implies ⊨. Provability entails validity. The reverse direction — ⊨ implies ⊢ — is completeness. Soundness is the 'safety' or 'correctness' direction: the proof system only certifies things that are actually true. Completeness is the 'power' direction: the proof system can prove everything that is true. Together they give the equivalence ⊢ iff ⊨. Soundness is easier to establish (holds for any well-designed system); completeness is the deeper result.

Question 4

Gödel's incompleteness theorems demonstrate that first-order logic is unsound when applied to sufficiently complex mathematical theories like Peano arithmetic.

• T. True
• F. False

Answer: False

This confuses soundness with completeness, and confuses the logic with the theory. First-order logic as a proof system is sound and complete (Gödel's completeness theorem, 1929). The incompleteness theorems (1931) show that Peano arithmetic — a specific theory formulated in first-order logic — cannot prove all truths expressible in its language. This is a limitation of the theory's axioms, not a failure of soundness. A sound proof system can still be based on insufficient axioms; it will simply fail to prove some true things (incompleteness), but it will never prove false things (soundness is preserved).

Question 5

Explain why soundness of a proof system is not trivially obvious, and give an example of how a proof system could fail to be sound.

Model answer: Soundness requires careful verification that every axiom is valid and every inference rule preserves truth — it is not guaranteed by intent. A proof system fails to be sound if any axiom is not logically valid, or if any inference rule allows a false conclusion to follow from true premises. For example, adding the axiom schema φ ∧ ¬φ (a contradiction) makes the system unsound: from a contradiction, any formula is derivable (ex falso quodlibet), including false ones. Historically, Frege's Basic Law V in naive set theory was intended as an axiom but turned out to be inconsistent (Russell's paradox), making any system built on it trivially unsound.

The proof of soundness proceeds by structural induction on derivations: verify all axioms are valid (base case), then show each inference rule preserves semantic truth (inductive step). This is nontrivial work, not an assumption. The history of logic is full of systems that seemed correct but contained subtle flaws — soundness proofs exist precisely to rule these out rigorously.