Questions: Syntactic Consequence (⊢) Versus Semantic Consequence (⊨)

Question 1

A logician says: 'I can verify that Γ ⊢ φ by checking all possible interpretations.' What is wrong with this?

• A. Nothing — checking all interpretations is exactly how ⊢ is defined
• B. The ⊢ relation is syntactic: it is verified by inspecting a finite proof derivation, not by examining models
• C. You can only check interpretations for propositional logic, not first-order logic
• D. The statement should use ⊨, not ⊢, since both notations mean the same thing

Answer: (B)

Γ ⊢ φ (syntactic consequence) means a finite derivation exists from Γ to φ using the proof system's rules. Verification is mechanical: examine the sequence of rule applications. Γ ⊨ φ (semantic consequence) is the one defined by checking all models — an infinitary claim. Using 'check all interpretations' to verify ⊢ confuses the two notions. Option D reflects the common error of treating ⊢ and ⊨ as synonymous; their coincidence for FOL is a theorem (soundness + completeness), not a definition.

Question 2

Gödel's completeness theorem for first-order logic states:

• A. Every true sentence in any model of arithmetic is provable in FOL
• B. If Γ ⊨ φ (φ is true in every model of Γ), then Γ ⊢ φ (φ is provable from Γ)
• C. No consistent formal system can prove all truths about the natural numbers
• D. Every syntactically valid FOL formula is also semantically valid

Answer: (B)

Completeness (⊨ ⇒ ⊢) is the direction that says: if φ holds in every model where Γ holds, then φ is provable from Γ in the proof system. This is non-trivial — it says the proof system is powerful enough to capture all semantic truth expressible in FOL. Option C describes Gödel's *incompleteness* theorem for arithmetic (a different, later result). Option A confuses FOL completeness with second-order or arithmetic completeness. Option D mixes up 'syntactically valid formula' with 'semantically valid formula', neither of which captures the Γ ⊢ φ / Γ ⊨ φ distinction.

Question 3

Soundness of a proof system means: anything provable (⊢) is semantically valid (⊨).

• T. True
• F. False

Answer: True

Soundness (⊢ ⇒ ⊨) says the proof system is trustworthy — it cannot derive a false conclusion from true premises. Proof: show that every axiom is semantically valid, then show by structural induction that every inference rule preserves truth. A sound system never produces a provable but false formula. Without soundness, the proof system would be useless for establishing truth. Completeness is the converse direction (⊨ ⇒ ⊢) — a much harder theorem.

Question 4

Because Γ ⊢ φ and Γ ⊨ φ are equivalent for first-order logic (by soundness and completeness), they refer to the same concept and the distinction between them is merely notational.

• T. True
• F. False

Answer: False

Extensional equivalence (same extension — same set of provable/valid pairs) does not imply conceptual identity. ⊢ is defined syntactically: a finite proof derivation exists. ⊨ is defined semantically: truth in every model (an infinitary claim). Their definitions are completely independent; their coincidence for classical FOL is a theorem. The distinction matters: in second-order logic, ⊢ and ⊨ come apart — there are semantic truths with no second-order proof (incompleteness). In intuitionistic logic, ⊢ and ⊨ diverge in different ways. Preserving the conceptual distinction is what lets us recognize and reason about logics where they fail to align.

Question 5

Why is the distinction between ⊢ and ⊨ conceptually important even in classical first-order logic, where they coincide by soundness and completeness?

Model answer: The distinction separates two fundamentally different questions: 'What can be proved?' (computational, proof-search, syntactic) versus 'What is true in all models?' (model-theoretic, semantic). Even when they have the same answer in FOL, they are answered by entirely different methods and can come apart in other logics. Second-order logic is sound but not complete — ⊨ is strictly larger than ⊢. Intuitionistic logic has different ⊢ and ⊨ relations. Understanding the distinction as conceptual rather than notational is what lets you recognize incompleteness (when ⊨ outstrips ⊢) and what the completeness theorem actually achieves: it identifies classical FOL as a fortunate special case where the two coincide.

A student who treats ⊢ and ⊨ as notational variants cannot understand what Gödel's incompleteness theorems say — because those theorems are precisely about the gap between provability and truth in certain formal systems. The completeness theorem closes the gap for FOL; incompleteness opens it for arithmetic. Neither result makes sense without a clear prior understanding that ⊢ and ⊨ are defined independently and can diverge.