Questions: Proof Strategies and Heuristics in Natural Deduction

Question 1

Your goal is to prove A → (B → C), and you have A, B, and C in your hypotheses. What does goal-directed reasoning prescribe as the first step?

• A. Apply Modus Ponens to the hypotheses to derive something useful before touching the goal
• B. Assume A as a hypothesis and set the new subgoal to B → C, then assume B and set the new subgoal to C
• C. Introduce B and C simultaneously using ∧-Introduction since both are available
• D. Search the hypotheses for a formula whose outermost connective matches the goal

Answer: (B)

The goal A → (B → C) has outermost connective →, so goal-directed reasoning immediately prescribes →-Introduction: assume A and prove B → C. That subgoal again has outermost connective →, so assume B and prove C. C is already a hypothesis, so the proof closes. This illustrates how reading the goal's connective drives the entire strategy — you apply introduction rules top-down until subgoals match hypotheses, without needing to search the hypothesis set first.

Question 2

Your hypothesis is ∃x P(x). Which strategy correctly exploits this hypothesis in a natural deduction proof?

• A. Apply ∀-Introduction to generalize the existential into a universal statement
• B. Introduce a fresh constant a with assumption P(a) via ∃-Elimination, then prove your goal using P(a)
• C. Set the proof goal to ∀x P(x) since an existential claim implies the property holds for all x
• D. Use Modus Ponens with P(x) as the antecedent, treating the existential as a conditional

Answer: (B)

∃-Elimination says: from ∃x P(x), you may introduce a fresh constant a (one not mentioned elsewhere in the proof) and assume P(a), then proceed. The freshness condition is critical — a must be arbitrary, not an already-named term — because you are reasoning about 'some unnamed element' without knowing which one. This is forward chaining from a hypothesis: you extract information from ∃x P(x) to generate a useful new assumption P(a). Applying ∀-Introduction to the existential is a category error — universals and existentials are separate quantifiers requiring separate rules.

Question 3

In goal-directed reasoning, the outermost connective of the goal formula tells you which introduction rule to try next.

• T. True
• F. False

Answer: True

This is the central heuristic of goal-directed proof construction. A goal of A ∧ B calls for ∧-Introduction (split into two subgoals). A goal of A → B calls for →-Introduction (assume A, prove B). A goal of ∀x φ(x) calls for ∀-Introduction (introduce a fresh variable, prove φ). A goal of A ∨ B calls for ∨-Introduction (choose a disjunct and prove it). Reading the outermost connective converts proof search from random rule application into a systematic top-down decomposition.

Question 4

Forward chaining from hypotheses and backward chaining from the goal are incompatible strategies — using one means you can seldom use the other in the same proof.

• T. True
• F. False

Answer: False

Both strategies are routinely combined in the same proof. A common pattern: work backward from the goal (applying introduction rules) until you reach a subgoal that is not immediately in the hypotheses, then switch to forward chaining (applying elimination rules to hypotheses) to generate new facts that satisfy the subgoal. The strategies are complementary: backward chaining decomposes the goal, forward chaining enriches the available facts. Expert proof construction fluidly alternates between the two depending on which 'side' of the proof tree is richer at each moment.

Question 5

A proof attempt is stuck — neither working backward from the goal nor working forward from the hypotheses is making progress. Describe two strategies you might try to get unstuck, and explain when each applies.

Model answer: First, try proof by contradiction: assume the negation of the goal (¬φ) as a hypothesis and try to derive a contradiction (⊥). This is useful when the goal lacks an obvious introduction rule or when a hypothesis would directly contradict ¬φ. Second, look for a missing lemma — restate what you are actually trying to prove as a simpler intermediate claim, prove that first, then use it. Getting stuck often signals that the path to the goal requires an intermediate step that neither current hypotheses nor direct goal decomposition reveals. A third option (for existential goals) is choosing a different witness: if ∃x φ(x) is the goal and your current witness guess produces a stuck subgoal, try a different term.

The strategies do not guarantee success, but they give structure to the search. Proof by contradiction is the escape hatch when no introduction rule applies and hypotheses seem to conflict with the goal but not obviously enough to close directly. Lemma extraction is the escape hatch when the gap between hypotheses and goal is too large to bridge in one step — identifying the right intermediate claim is often the hardest creative act in proof construction.