Proof strategy · printable packet

Deciding the last line from the shape of the conclusion, turning what that rule demands into new goals, and recognizing a legitimate step that leads nowhere.

Paper packet. Every task here also exists on screen, where it is checked automatically; answers written on paper are not assessed by Nydus. When you are back at a device, enter your answers there.

1. What you will learn

By the end of this lesson you will be able to choose the last rule of a proof from the shape of its conclusion, turn that rule's demands into goals and work backwards to the premises, write the finished proof forwards in the right order, count the lines a derivation needs, recognize a legitimate step that no later line can use, and read the conclusion's vocabulary as a planning clue.

2. What you already have

You know the rules and can check a proof line by line. What is left is finding one: deciding which rule the last line will use before writing the first.

3. Terms to use precisely

4. Planning a derivation

Term	What it means
Goal	The exact formula the final line must establish.
Backward planning	Asking which rule could produce the goal and what inputs it needs.
Forward derivation	Applying a permitted rule to lines already available.
Dead end	A legitimate derived line that does not supply the missing input needed for this goal.

Proofs are written forwards and found backwards. Start from the conclusion and ask which rule could produce a line of that shape: a conjunction comes from conjunction introduction, a disjunction from disjunction introduction, a conditional from the chain rule, a bare letter from detaching a conditional or opening a disjunction. That rule's demands become the new goals, and the process repeats until every remaining goal is a premise or something obviously reachable from one. Then work forwards and write the proof down in the opposite order. Two shortcuts save most of the effort. Look at where the conclusion occurs among the premises: if it is a disjunct, the last step is probably disjunctive syllogism, and the real goal is the denial of the other disjunct. And look at the vocabulary: a letter in the conclusion that no premise mentions can only have got there by disjunction introduction.

Another way: steps

Name the main connective of the conclusion and the rule that introduces it.
Write down what that rule demands; those are the new goals.
Repeat until the goals are premises or one step from them.
Write the proof forwards, premises first.

Another way: example

Goal $S$, premises including $P \vee S$. $S$ is a disjunct, so plan disjunctive syllogism as the last line; the goal becomes $\neg P$, and the other premises exist to supply it.

5. Plan backward, write forward

If the goal is R and a premise is (P & Q) -> R, the missing input is P & Q. If P and Q are separately available, andI builds that input. MP then yields R. The plan looks backward from R, but the finished derivation cites only earlier lines. A future line cannot be used as a reference.

If the goal is a conjunction, plan to establish its two parts before using andI. If a required part is inside an available conjunction, andE extracts it. If a denial is the goal, inspect conditionals whose antecedents match what must be denied; a denial of their consequent enables MT. A rule is useful only if its exact inputs are available.

Read the allowed-rule list on each exercise. The course's bounded editor permits rules such as MP, MT, andI, andE, orI, DS, HS and DN when listed. It does not accept arbitrary obvious steps. Temporary assumptions require assume and impI to be explicitly allowed, as taught in the previous lesson. A shorter proof is convenient, but validity matters before brevity: every line must be supported and the last must be the stated target. After writing a derivation, audit the references independently of the plan that produced it.

6. Turn the target into smaller obligations

A proof search begins with two lists: the formulas you have and the formula you need. These lists have different roles. Available formulas may justify a new line. A desired formula is only a planning target until a rule actually establishes it. Keeping that distinction visible prevents circular proofs in which a writer quietly treats the desired conclusion as an extra premise.

Inspect the outermost connective of the target. A conjunction such as R & S suggests andI, which creates two obligations: obtain R and obtain S. Neither obligation is optional. You may already have one conjunct while the other needs several steps. Write down the missing part specifically instead of restarting the whole search. Once both are accessible lines, joining them is a single justified operation.

A conditional target suggests a different plan when assume and impI are allowed. To prove P -> R, temporarily assume P and try to derive R inside that scope. The assumption is not a new permanent premise. The finished conditional must discharge it. If the editor does not list those rules, inspect the available flat rules and premises instead: a suitable chain may permit HS. The target alone does not authorize a rule that the task has excluded.

An atomic goal has no connective to build. Look for a conditional with that atom as consequent, a conjunction containing it, or a disjunction from which the alternative can be excluded. These are candidate routes, not guarantees. If Q -> R is available, ask whether Q can be obtained. If R & S is available, andE gives R directly. If R | S and ~S are available, DS supplies R. The useful route depends on actual inputs, not on which rule you used most recently.

For a denied goal ~P, a conditional P -> Q and an accessible ~Q offer an MT route. If the target is ~(P & Q), preserve those parentheses while searching: a denial of P alone is a different formula. Planning with complete formulas avoids a common mistake in which a solver chooses a rule for a single letter and loses the target's scope. After choosing a route, return to the available list and confirm each required input.

7. Alternate backward plans with forward construction

Consider premises P & Q, Q -> R, and R -> S with target S. Backward planning identifies R as the input needed for the last conditional. It then identifies Q as the input needed for the preceding conditional. Forward construction extracts Q from the conjunction, derives R by MP, and derives S by MP. The discovery order and the justification order differ. A finished proof records the latter, so every reference points to an earlier line.

Not every legal derivation advances the plan. Extracting P from P & Q is legitimate, but it does not supply the Q required by Q -> R. Calling that line a dead end means it is unhelpful for this particular route, not that it is false or forbidden. If another premise were P -> S, the same extraction would become useful. Strategy concerns relevance to the current target while validity concerns whether each operation is justified.

Avoid trying every possible disjunction introduction. From P, orI can produce P | Q, P | R, and indefinitely many other formulas. This freedom does not make every expansion a productive move. Introduce a disjunction when the target or an available conditional specifically requires it. For example, with (P | Q) -> R, deriving P | Q from P supplies a definite missing input. The target gives the expansion a reason.

Conjunction introduction also works best with a specified purpose. If the target is R and the available rule is (P & Q) -> R, forming P & Q is useful once P and Q are available. Forming P & P is legal in classical logic but does not match that antecedent. A proof checker compares the formulas actually written; it cannot substitute a more helpful conjunction for the one you entered.

When a plan stalls, state the missing formula before making another move. If no premise or permitted rule can supply it, try another route. You may also use a truth-table check to investigate whether the premises entail the goal at all. Finding a countermodel settles that no sound derivation from those premises can establish the goal. Failing to find a proof immediately does not establish invalidity: the search may simply be incomplete. Distinguish a demonstrated countermodel from a report that you have not yet found a derivation.

8. Audit the finished proof independently

Once the target appears, read the proof again as a skeptical reader who did not see your plan. For each premise line, check membership in the supplied premise list. For each derived line, retrieve the cited formulas and match them to the named rule. This audit can reveal a skipped extraction, a reversed conditional, a reference to a future line, or a correct formula justified by the wrong operation.

Check scope separately when temporary assumptions occur. An interior result is usable while its assumptions remain open. After impI closes a subproof, its resulting conditional is available outside, but the interior assumption is not. A proof can have correct local rule shapes yet fail because a reference reaches into a discharged scope. The assumption stack is part of the record, not merely a visual indentation convention.

Check the last line as well. A derivation that establishes something stronger or related may still need a final operation to reach the exact target. If the target is R and you have R & S, append andE. If the target is R & S and you have separate R and S lines, append andI. Ending at an intermediate result leaves the written task unfinished even when the remaining step is easy.

Only after these checks should you consider shortening the proof. Redundant legal lines usually affect clarity rather than truth preservation. Removing one may require renumbering all later references. A short proof with a broken dependency is worse evidence than a longer proof whose every step can be checked. Keep the explanatory record accurate as you simplify it, and preserve the distinction between what follows from the premises and whether those premises accurately describe the world.

9. Auditing a two-condition release decision

A fictional publishing team uses the rule that a document may be released when both its content check and its accessibility check are complete. Let C mean content checked, A mean accessibility checked, and R mean release permitted. The premises are C, A, and (C & A) -> R. The target is R.

Work backward: the conditional can yield R, but it requires the whole antecedent C & A. Neither C alone nor A alone matches it. Work forward: write C as line 1, A as line 2, and the conditional as line 3. Use andI on lines 1 and 2 to obtain C & A at line 4. Use MP on lines 3 and 4 to obtain R at line 5. The proof has two derived lines after its three premises.

Now audit a shortcut that cites only lines 1 and 3 for R. It fails because line 1 supplies only C, not C & A. A correct conclusion elsewhere in the record does not fix that unsupported step. The missing accessibility check is exactly what the compound antecedent was designed to preserve.

The example does not claim that these two checks are a sufficient real publication policy. They are the declared premises of a bounded exercise. In actual work, the policy and the evidence for completion need independent review. A derivation checks whether a decision follows from the specified requirements; it does not prove the requirements are complete or that a recorded check was genuinely performed.

10. Where this goes wrong

The commonest failure is working forwards only: applying every rule that fits and hoping the conclusion appears. It sometimes does, and on a longer problem it produces pages of legitimate, useless lines. The second is treating a legitimate step as progress; the test is whether a later line can cite it. The third is stopping when the conclusion becomes available rather than written — a proof ends on its conclusion, as a line.

11. Extract, then apply

12. Build the missing input

13. Plan two connected applications

14. Supply the other conjunct

15. Guided practice

16. Guided practice

Complete a backward-plan audit for target Q & S, given Q and R -> S. Count the conjunct goals still unproved.

17. Guided practice

18. Practice

19. Practice

20. Somewhere new

C means content checked, A accessibility checked, and R release permitted. Given C, A and (C & A) -> R, derive R with each dependency explicit.

21. Lesson test

Lesson test: one question per skill, one attempt each, no hints. Your answers are checked when you submit.

22. Test question

23. What you can do now

You can plan a derivation backwards from its conclusion and then write it forwards. Say in your own words why a letter occurring only in the conclusion tells you which rule the last line must use.

Working for the steps left to you

Q, R give Q & R by andI.

Both inputs are now established.

#	Formula	Rule	Lines
1
2
3
4
5
6

#	Formula	Rule	Lines
1
2
3
4
5
6

#	Formula	Rule	Lines
1
2
3
4
5
6

#	Formula	Rule	Lines
1
2
3
4
5
6