Questions: Deductive Reasoning and Formal Proof Systems

Question 1

The Completeness Theorem for first-order logic states which of the following?

• A. Every first-order sentence is either provable or its negation is provable
• B. If Γ ⊢ φ, then Γ ⊨ φ — every formally derivable statement is semantically valid
• C. If Γ ⊨ φ, then Γ ⊢ φ — every semantically valid statement has a formal proof
• D. Every proof can be reduced to a finite sequence of applications of modus ponens

Answer: (C)

Completeness is the direction ⊨ implies ⊢: if φ is a semantic consequence of Γ (true in every model that satisfies Γ), then there exists a formal derivation of φ from Γ. This is the deep and surprising direction — it says the syntactic machinery of proof systems is powerful enough to capture all of semantic truth for first-order logic. Option B describes soundness (the easy direction: provable implies valid). Option A is a different property (completeness for a specific logic like classical propositional logic, but not what the theorem says).

Question 2

A researcher switches from natural deduction to resolution calculus hoping it will let her prove theorems that natural deduction could not. What does the Completeness Theorem tell us about this hope?

• A. Resolution is indeed more powerful for first-order logic because it works on clausal normal form
• B. Natural deduction is more powerful because it directly mirrors mathematical reasoning
• C. Both systems prove exactly the same theorems for first-order logic — the choice affects proof style and computational efficiency, not which sentences are provable
• D. Resolution can prove more sentences for decidable fragments, but natural deduction wins on undecidable ones

Answer: (C)

The Completeness Theorem guarantees that all sound and complete proof systems for first-order logic prove exactly the same sentences. Natural deduction, sequent calculus, Hilbert-style axiom systems, and resolution all derive the same theorems — because they all prove exactly the semantically valid consequences of the premises. Switching systems changes how proofs look and how efficiently they can be found by algorithms, but not what can be proved in principle.

Question 3

Soundness of a proof system means that if Γ ⊢ φ (φ is formally derivable from Γ), then Γ ⊨ φ (φ is a semantic consequence of Γ).

• T. True
• F. False

Answer: True

True. Soundness is the 'correctness' direction: the proof system never derives false conclusions from true premises. Every inference rule in a sound system preserves semantic truth, so any chain of rule applications starting from valid premises produces a valid conclusion. Soundness is usually straightforward to prove by checking each rule individually. Completeness — the reverse direction — is what requires deep work.

Question 4

A formal proof of φ from premises Γ establishes that φ is absolutely true in most possible worlds, regardless of whether Γ is true.

• T. True
• F. False

Answer: False

False. A proof of φ from Γ establishes a conditional: if Γ is true, then φ must be true. The proof is valid (as a derivation) even if Γ contains false premises — the logical machinery makes no assumptions about whether premises are true. If you want to conclude φ is absolutely true (a tautology), you need Γ to be empty and φ to be provable from no premises at all. Formal proof is about inference, not certification of absolute truth — it guarantees that truth is preserved from premises to conclusion, nothing more.

Question 5

What is the difference between soundness and completeness of a proof system, and which direction is more surprising and harder to prove?

Model answer: Soundness (⊢ implies ⊨): everything the proof system can derive is actually semantically valid — the system makes no mistakes. Completeness (⊨ implies ⊢): everything semantically valid can be derived — the system misses nothing. Completeness is the surprising and hard direction. Soundness can be verified by checking that each inference rule preserves truth. Completeness requires showing that for every semantic consequence, there exists a finite formal derivation — a non-constructive existence proof. Gödel's 1929 completeness theorem established this for first-order logic, making it a landmark result. His later incompleteness theorems then showed that sufficiently strong formal systems (like arithmetic) cannot be both consistent and complete.

The slogan: soundness says 'you can't prove false things'; completeness says 'you can prove all true things.' The surprising one is completeness — it is far from obvious that the finite syntactic game of proof can capture all of infinite semantic truth.