Questions: Counterexamples and Refutation

Question 1

You claim: 'From the premises All mammals breathe air and All whales are mammals, it follows that All whales breathe air.' A classmate says this inference fails. What would the classmate need to produce to refute your claim?

• A. A formal derivation showing the conclusion cannot be derived from the premises using inference rules
• B. A specific interpretation — a domain and predicate assignments — where both premises are true but the conclusion is false
• C. An alternative argument that leads to the opposite conclusion from the same premises
• D. A dictionary definition of 'mammal' that does not include whales

Answer: (B)

To refute Γ ⊨ φ (semantic consequence), one must produce a counterexample: a specific interpretation where all premises in Γ are satisfied but φ is false. This is exactly a model of Γ ∪ {¬φ}. In this case, no such interpretation exists because the argument is valid — but the task of refutation is always to construct this model. A derivation failure (option A) concerns syntactic provability, not semantic consequence, and the two can diverge in first-order logic.

Question 2

An automated theorem prover attempts to prove Γ ⊨ φ by adding ¬φ to the premises and using resolution to derive a contradiction. Why is this the correct strategy rather than trying to directly construct a proof of φ?

• A. Resolution can only operate on formulas in negation normal form, and adding ¬φ converts φ into the required form
• B. Γ ⊨ φ holds if and only if Γ ∪ {¬φ} is unsatisfiable — deriving ⊥ from the combined set shows no interpretation can make all premises true while making φ false
• C. Direct proof of φ would require checking all possible interpretations, which is infinite, while refuting Γ ∪ {¬φ} requires only finite search
• D. The prover cannot verify φ directly; it can only check whether a given set of formulas is satisfiable or unsatisfiable

Answer: (B)

By the fundamental logical equivalence: Γ ⊨ φ ⟺ Γ ∪ {¬φ} is unsatisfiable. If there is no interpretation where Γ is all-true and φ is false — i.e., where Γ ∪ {¬φ} is satisfied — then φ must hold in every model of Γ. Resolution proves unsatisfiability by deriving the empty clause (⊥). So refuting Γ ∪ {¬φ} is not a workaround; it is logically equivalent to proving Γ ⊨ φ. This equivalence is the theoretical foundation of all refutation-based automated reasoning.

Question 3

A counterexample to the semantic consequence Γ ⊨ φ is precisely a satisfying model of the formula set Γ ∪ {¬φ}.

• T. True
• F. False

Answer: True

True, and this equivalence is the central insight of the topic. A counterexample is an interpretation where all formulas in Γ are true but φ is false. 'φ is false' is the same as '¬φ is true.' So a counterexample satisfies Γ and satisfies ¬φ — exactly satisfying Γ ∪ {¬φ}. This transforms the question of semantic consequence (does every model of Γ satisfy φ?) into a question about satisfiability (does Γ ∪ {¬φ} have any model?), which is computationally more tractable and directly connects to proof search.

Question 4

If no counterexample can be found after exhaustively checking most possible interpretations over domains of size 1, 2, and 3, then Γ ⊨ φ is proven to hold.

• T. True
• F. False

Answer: False

False. For first-order logic, failing to find a counterexample over small finite domains does not constitute a proof. A counterexample might require a larger or even infinite domain. First-order logic is only semi-decidable: if Γ ⊨ φ holds, a resolution prover will eventually find a proof (completeness), but if Γ ⊭ φ, the counterexample search over finite domains may run forever without terminating. Counterexample search is valuable for quickly refuting false claims but cannot replace proof when the entailment actually holds — finite domain failure is evidence, not proof.

Question 5

Explain why finding a counterexample to Γ ⊨ φ is equivalent to finding a satisfying assignment for Γ ∪ {¬φ}, and why this equivalence matters for automated theorem proving.

Model answer: Γ ⊨ φ means every interpretation making Γ all-true also makes φ true — equivalently, no interpretation makes Γ all-true and φ false. A counterexample is precisely such an interpretation: all of Γ satisfied, φ false. But φ false means ¬φ is true, so a counterexample satisfies Γ ∪ {¬φ}. The equivalence is: Γ ⊨ φ holds if and only if Γ ∪ {¬φ} has no satisfying model (is unsatisfiable). For automated theorem proving, this converts the problem of proving a consequence (checking all models — an infinitary condition) into the problem of showing a formula set is unsatisfiable (finding a contradiction — something resolution procedures do mechanically). If the resolution prover derives ⊥, the proof is complete; if it finds a satisfying assignment, it has discovered a counterexample.

This equivalence is foundational to the architecture of all refutation-based systems (DPLL SAT solvers, resolution provers, SMT solvers). Rather than constructing proofs directly, these systems attempt to find a model of the negation of the claim. Proof and counterexample search are two sides of the same coin: either the search terminates with a counterexample (the claim is false) or it terminates with a refutation (the claim is true). The theoretical underpinning is this biconditional equivalence.