A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Proof strategies in natural deduction are techniques for constructing proofs efficiently. Key strategies include: working backward from the goal (backward chaining), identifying what hypotheses are needed to derive the goal, using introduction rules to build complex formulas, and using elimination rules to break down given formulas. For existential goals, guess a witness; for universal goals, assume an arbitrary element. Understanding the structure of the goal formula guides which rules to apply. These heuristics transform proof construction from trial-and-error into a systematic process.
Work through proofs step-by-step, making strategy choices explicit. Discuss why certain rule applications are more productive than others. Practice both simple and complex proofs, building intuition for which strategies apply. Relate strategies to the logical structure of the goal.
From your study of natural deduction for propositional and first-order logic, you have a complete inventory of inference rules: introduction and elimination rules for each connective and quantifier, plus structural rules. The rules are sound — you cannot derive falsehoods — and complete — any valid consequence is reachable. But knowing the rules is not the same as knowing how to construct proofs. Rules give you the vocabulary; proof strategies give you the grammar for using that vocabulary purposefully.
The first and most important insight is goal-directed reasoning. Look at the formula you want to prove. Its outermost connective tells you which *introduction* rule to try. If the goal is A ∧ B, use ∧-Introduction — reduce the goal to proving A and proving B separately. If the goal is A → B, use →-Introduction — assume A as a hypothesis and prove B. If the goal is ∀x φ(x), use ∀-Introduction — introduce a fresh variable a and prove φ(a). This "read the goal, apply the matching introduction rule" strategy handles the majority of proof steps automatically. You are essentially working backward from the goal, decomposing it into simpler subgoals until everything is in the hypotheses.
The complementary strategy is hypothesis exploitation. Look at what you have been given. Each hypothesis also has an outermost connective that suggests an *elimination* rule. From A ∧ B you can extract A or B via ∧-Elimination. From A → B and a proof of A, you get B via Modus Ponens. From ∃x φ(x), introduce a fresh constant a with the assumption φ(a) via ∃-Elimination. This forward chaining from hypotheses generates new facts that can unlock further steps. The skill is knowing when to work backward from the goal versus forward from the hypotheses — and the answer depends on which side is "richer" at a given moment.
Two special strategies break out of the main pattern. For proofs by contradiction (assuming ¬φ and deriving ⊥), use when the goal φ has no obvious introduction rule or when a hypothesis would contradict ¬φ directly. For existential witnesses, when the goal is ∃x φ(x), you must *guess* the right term t and then prove φ(t) — this is the one step that requires creativity rather than purely mechanical decomposition. Finding the witness often requires understanding what the proof "wants" before you can complete it.
A practical discipline: keep the proof tree in mind as a tree with the conclusion at the root and assumptions at the leaves. Every rule application either decomposes the goal (working down in the tree) or uses a hypothesis (connecting a leaf). Proofs get stuck when neither strategy applies — which signals a missing lemma, an incorrect conjecture, or a need to restate what you are actually trying to show. The strategies do not guarantee finding proofs, but they convert proof search from a random walk into a systematic exploration with clear decision points.