Conditional proof · printable packet

Assuming an antecedent to derive a consequent, discharging the assumption, and the theorem that says why the finished conditional rests on the premises alone.

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 lay out a conditional proof in order, say which lines rest on the assumption and which do not, state what discharging entitles you to write, test an argument with a conditional conclusion semantically, state the deduction theorem, and recognize when the chain rule reaches the same conclusion without an assumption.

2. What you already have

You can plan a derivation from the shape of its conclusion. When that conclusion is a conditional and no two premises chain into it, the rules met so far have nothing to offer, and this lesson supplies what is missing.

3. Terms to use precisely

4. Conditional proof and the deduction theorem

Term	What it means
Temporary assumption	A supposition used inside a subproof, not an added permanent premise.
Discharge	Closing a subproof and asserting the conditional it establishes.
Dependency	The premises and open assumptions a derived line relies on.
Hypothetical syllogism	The flat rule HS: from P -> Q and Q -> R, infer P -> R.

To prove $\phi \to \psi$: write $\phi$ as an assumption, derive $\psi$ using it and the premises, then discharge the assumption and write $\phi \to \psi$. Two things make this work. First, the bookkeeping: every line derived while the assumption is in force rests on it, and the discharged conditional is the only line that does not — which is why $\psi$ itself may not be carried outside. Second, the deduction theorem: $\Gamma \cup \{\phi\} \vdash \psi$ exactly when $\Gamma \vdash \phi \to \psi$. On the semantic side the same equivalence holds for $\models$, and it is easy to see why: restricting attention to the rows where $\phi$ is true is exactly what a conditional conclusion asks for. Assumptions may be nested — a conclusion with two arrows needs two of them — and each discharge removes one, in the reverse of the order they were made.

Another way: steps

The goal is $\phi \to \psi$: assume $\phi$, and note that the goal is now $\psi$.
Derive $\psi$ from the premises and the assumption.
Discharge: write $\phi \to \psi$, citing the whole subproof.
If $\psi$ is itself a conditional, repeat inside.

Another way: example

Premises $P \to Q$ and $Q \to R$; goal $P \to R$. Assume $P$; modus ponens twice gives $R$; discharge to get $P \to R$. The chain rule does the same thing in one line, and is what conditional proof generalizes.

5. Entering and closing a subproof

A conditional proof assumes its antecedent temporarily, derives its consequent, and closes the assumption. The consequent is not thereby established without the assumption. From Q as a premise, assume P, derive P & Q, and discharge P to get P -> (P & Q). You have not established P.

In the proof table, select assume for a temporary assumption and leave its references empty. To close the subproof, select impI and cite two line numbers: the assumption that opens it and its final line. That final line must be immediately above the impI line. Write the conditional with the assumption as antecedent and the final formula as consequent. A one-line subproof of P -> P cites the same assumption line twice.

Nested assumptions close from the inside outward. After closing an assumption, you may use the resulting conditional, but not the lines inside that closed scope. The rule reit copies one earlier accessible formula when you need it as the final line inside a subproof. A premise remains available in nested subproofs, as does a still-open outer assumption. All assumptions must be closed when you finish. Read the allowlist: rules not listed in an exercise are unavailable.

Some examples use DS, disjunctive syllogism: from P | Q and ~P derive Q. HS chains P -> Q and Q -> R into P -> R. Both preserve truth, but an item requiring conditional proof can omit HS so that you must show the intermediate reasoning. An assumption must never be mislabeled as a premise.

6. Why an assumption is not circular reasoning

When the target is a conditional, temporarily accepting its antecedent does not assume the whole conclusion. Suppose the target is P -> R. You grant P inside a restricted piece of reasoning and ask whether R can be established from it together with the original premises. If the attempt succeeds, the result is a statement about what follows from P, not a declaration that P is true. The restriction is part of the argument, not an optional warning written beside it.

Compare two attempted proofs. In the first, someone writes P as an assumption and stops with P. That gives no unconditional reason to believe P. In the second, someone writes P as an assumption and closes it by deriving P -> P. This conditional says only that P follows if P is granted. It is true whether P is true or false. The second proof succeeds because its conclusion records the very condition the first attempt concealed.

You can check this distinction semantically. A false conditional requires a true antecedent and a false consequent. For P -> R, a countermodel must therefore make P true and R false while keeping the original premises true. Inside the subproof you temporarily add exactly P, the antecedent a countermodel would need. If truth-preserving rules then establish R, that candidate countermodel is impossible. On assignments where P is false, the material conditional already holds. Together these observations explain why the completed conditional follows from the original premises.

This explanation also shows why the rule does not predict a real event. Deriving 'if the request is approved, a confirmation is sent' does not show that a request exists, that it will be approved, or that anybody has sent a message. Those are additional claims. A conditional proof preserves the distinction between a dependency and the actual occurrence of its antecedent. It is particularly useful when checking plans, requirements and proposals before deciding whether to put them into effect.

7. Reading the dependency record

Imagine that each line carries a small record of the assumptions currently open. A premise copied before any assumption has an empty record. After you assume P, lines written inside that scope carry P in their record. If you next assume Q, the inner lines carry both P and Q. Closing Q removes Q from the record of the conditional you have just established, while P remains. Closing P removes the last temporary assumption. This is why nested conclusions are built from the inside outward.

The record describes scope, not merely which symbols appear in a formula. An inner line containing only P can still be inside the Q subproof. It cannot be exported just because the letter Q is absent from its text. Conversely, a conditional containing Q can be available outside the Q subproof, because the implication records the assumption that was discharged. Looking only at the letters in a formula is therefore an unreliable way to decide which lines can be cited.

Consider the theorem P -> (Q -> P). Assume P, then assume Q. The earlier P remains accessible because its scope surrounds the Q scope. Reiterate P as the last line of the inner subproof. Discharge Q to obtain Q -> P; this new line still depends on the outer P. Then discharge P to obtain the whole target. Nothing required deriving P from Q alone. The outer assumption supplied P, and the final nested conditional states that dependency honestly.

Now suppose you close a P subproof and later open a different Q subproof. The earlier interior P line is not available inside the new sibling scope. Closing a box does not place all its contents in a common store of established facts. You may use the conditional produced by closing the box, or repeat an original premise, but you may not revive the discharged supposition with reit. This is the central error to look for when a proof seems to establish an arbitrary statement too easily.

8. Planning and auditing a conditional proof

Begin with the outermost connective of the target. For P -> (Q & R), there is one outer arrow. Assume P and make Q & R the local goal. You will normally need to obtain Q and R separately and combine them with andI. For P -> (Q -> R), there are two nested arrows. After assuming P, the local goal is itself a conditional, so you may open a second assumption Q and work toward R. These targets use the same letters but demand different final constructions.

Before opening a new scope, inspect the premises and the rules allowed in the exercise. If a needed consequence is already a premise, reit can bring an accessible copy to the end of the subproof. If a conditional needs a conjunction as its antecedent, construct that whole conjunction before applying MP. A plan that says only 'use the premises' is too vague: name the next formula you need and the rule whose inputs would produce it.

The completed derivation is written forward even when its plan was worked out backward. Every ordinary reference points to an earlier accessible line. For impI, the first reference identifies the innermost open assumption and the second identifies the immediately preceding end line. The new formula must have exactly those formulas as antecedent and consequent. Check these three conditions separately; the correct-looking arrow alone does not establish a valid discharge.

Finally audit the proof without following your original plan in your head. Read each cited line afresh, compare its complete formula with the rule's inputs, and track the open assumptions after every discharge. Check that the final formula is the requested target and that no temporary assumption remains open. A misplaced reference is repairable, but until it is repaired the written argument does not supply the justification it claims. This audit is a way to make reasoning inspectable by someone who did not already know what you meant.

9. Reasoning about a proposed service change

A fictional service team accepts two rules: if a request is approved, it is scheduled; if it is scheduled, a confirmation is sent. Let A mean approved, S mean scheduled, and C mean confirmation sent. The desired conclusion is A -> C. Nothing states that any particular request has been approved.

To reason conditionally, suppose A for the moment. From A and A -> S, infer S. From S and S -> C, infer C. Close the supposition and conclude A -> C. The final claim depends on the two original rules, while the intermediate S and C also depended on the temporary A. Those intermediate claims cannot be announced unconditionally about an actual request.

The flat derivation reaches the same conditional by HS from A -> S and S -> C. Its three lines are the two premises followed by A -> C, citing lines 1 and 2. An exercise that allows HS can use this shorter route. An exercise that omits HS requires the explicit assumption and discharge instead.

If a team member now asks whether a confirmation has actually been sent, the correct answer is that these premises alone do not settle that. A false, S false, C false satisfies both rules. To establish C for a real request, add evidence that A holds, then use the resulting conditional. Keeping a hypothetical workflow separate from an actual event prevents a plan from being mistaken for a status report.

10. Where this goes wrong

The first error is carrying a line out of the subproof: $\psi$ was derived on a supposition and does not survive the discharge, only $\phi \to \psi$ does. The second is treating the assumption as a premise, so that the finished proof quietly claims something nobody granted. The third is discharging in the wrong order when assumptions are nested, which produces a conditional with its halves in the wrong places.

11. A consequent already available as a premise

12. Derive a consequence through two rules

13. Two nested assumptions and a compound input

14. From S, prove R -> (R & S)

15. Guided practice

16. Guided practice

Complete the dependency record while proving P -> (Q -> P). Count only temporary assumptions still open.

17. Guided practice

With no premises prove S -> S. You may close a one-line subproof by citing its assumption twice.

18. Practice

A means approved and C means confirmation sent. Express the conditional guarantee that approval implies a confirmation, without asserting that approval happened.

19. Practice

20. Somewhere new

With no premises derive P -> (Q -> P). Use assume, reit and impI; close both assumptions.

21. Lesson test

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

22. Test question

From R derive Q -> (Q & R). Open an assumption and discharge it; give each rule and its references.

23. What you can do now

You can build and read a conditional proof and say what each line rests on. Say in your own words why the formula derived under an assumption cannot be carried out of the subproof.

Working for the steps left to you

The assumption and the original premise are both accessible.

The implication records the dependency on R rather than asserting R.

#	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