# Proof Strategy

Philosophy I · Logic · https://tryals.app/learn/philosophy-i/proof-strategy

## Reading the Proof Off the Goal

Knowing the rules does not tell you which to apply. Strategy does, and the central insight is that **the shape of the goal dictates the method**.

| Goal has the form | Strategy |
|---|---|
| $P \rightarrow Q$ | Assume $P$, aim for $Q$ |
| $\neg P$ | Assume $P$, aim for a contradiction |
| $P \wedge Q$ | Prove each separately, then conjoin |
| $P \vee Q$ | Prove either disjunct, or use cases |
| Anything, when stuck | Assume its negation, aim for a contradiction |

Working **backwards from the goal** is almost always more productive than working forwards from the premises. Forward reasoning generates whatever the rules happen to allow, most of which is irrelevant; backward reasoning generates only what would actually help.

**Indirect proof**, assume the negation of the goal and derive a contradiction, is the universal fallback, available whatever the goal looks like. It is often the only route when the goal is atomic, since an atom has no connective to guide you.

Subproofs **nest**, and the nesting has a strict discipline: an inner subproof may use lines from any subproof still open around it, but never from one already closed. Depth is often necessary, proving $P \rightarrow (Q \rightarrow R)$ requires two nested assumptions, one for each conditional.

Several **derived rules** are provable from the basic ones and then used freely as shorthand:

- **Modus tollens**: from $P \rightarrow Q$ and $\neg Q$, infer $\neg P$
- **Hypothetical syllogism**: from $P \rightarrow Q$ and $Q \rightarrow R$, infer $P \rightarrow R$
- **Disjunctive syllogism**: from $P \vee Q$ and $\neg P$, infer $Q$
- **Contraposition**: $P \rightarrow Q$ is equivalent to $\neg Q \rightarrow \neg P$

Derived rules add no power, anything provable with them is provable without, but they shorten proofs enormously, which matters in practice.

> **Common pitfall:** grinding forwards from the premises hoping the conclusion appears. It rarely does. Look at the goal first: a conditional goal tells you to assume its antecedent, and that single move often turns an intractable problem into a routine one.

## Practice questions

6 of this lesson's 11 practice questions, with answers. The full set is in the app.

### 1. Modus tollens, hypothetical syllogism, disjunctive syllogism and contraposition are all derived rules. How many additional arguments become provable once they are added to the basic system?

**Answer:** 0

**Why:** **None.** Derived rules are theorems of the basic system, so they add no power whatever, only brevity. That is exactly why they are safe to use freely.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/modus-tollens-hypothetical-syllogism-disjunctive-syllogism-and

### 2. Derived rules add no logical power to a system, yet proof construction relies on them extensively. What explains this tension, and how does it influence practical strategy?

A. They allow forward reasoning to bypass goal-directed strategies
B. They permit shorter proofs without altering what is derivable
C. They expand theorem scope without introducing formal unsoundness
D. They eliminate the necessity of discharging assumptions manually

**Answer:** B. They permit shorter proofs without altering what is derivable

**Why:** Derived rules are mere abbreviations for subproof patterns rather than new formal mechanics. Confusing proof brevity with system strength or structural shortcuts overlooks that every valid step remains strictly reducible to primitive natural deduction rules.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/derived-rules-add-no-logical-power-to-a-system-yet-proof

### 3. The most productive strategy is to apply rules forwards from the premises until the conclusion appears.

**Answer:** False

**Why:** False, forward search generates everything the rules allow, almost all of it irrelevant. Working **backwards** from the goal generates only steps that would actually close the proof, which is why it is the standard discipline.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/the-most-productive-strategy-is-to-apply-rules-forwards-from-the

### 4. Why is indirect proof available whatever the shape of the goal?

A. Every complex formula can be systematically rewritten into an equivalent negated conditional
B. It is the only valid inference rule in natural deduction that operates without any subproof
C. Assuming the negation of any sentence is always permitted, and a contradiction refutes it
D. Derived rules like contraposition automatically transform any arbitrary goal into an atomic claim

**Answer:** C. Assuming the negation of any sentence is always permitted, and a contradiction refutes it

**Why:** Indirect proof makes no demand on the goal’s form: you may assume the negation of anything, and a contradiction refutes it. That universality is why it is the fallback when the goal offers no guidance.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/why-is-indirect-proof-available-whatever-the-shape-of-the-goal

### 5. Arrange the steps of an indirect proof in order.

**Answer:**

1. Assume the negation of the goal
2. Derive consequences from that assumption together with the premises
3. Reach a contradiction
4. Discharge the assumption
5. Conclude the original goal

**Why:** Assume the denial, derive an absurdity, and conclude the original. Since the assumption led to contradiction it cannot hold, so its negation, the goal, must. Discharge comes before the conclusion is asserted.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/arrange-the-steps-of-an-indirect-proof-in-order

### 6. Sort each move by whether it is a legitimate step in a natural deduction proof.

**Answer:**

- Legitimate: Using a premise at any point in the proof, Using a line from a subproof still open around you, Assuming the negation of the goal to seek a contradiction
- Not permitted: Using a line from a subproof that has been closed, Concluding while an assumption remains undischarged

**Why:** Premises and still-open subproofs are always available; closed subproofs never are. Concluding with an assumption still open would leave the result conditional on a supposition rather than on the premises.

Page: https://tryals.app/practice/philosophy-i/proof-strategy/sort-each-move-by-whether-it-is-a-legitimate-step-in-a-natural