Conditional Proof: Discharge the Right Assumption and Keep the Others Visible

Discharge a complete subproof, not every assumption in sight

To prove A→B by conditional introduction, assume A temporarily, derive B in that subproof, and cite the whole range from the assumption to B. The rule discharges that opening assumption. Any surrounding assumptions and premises remain available dependencies; they are not erased merely because the result is a conditional.

This guide follows the classical TFL natural-deduction package in forall x: Calgary. Its conditional-introduction label is →I. We use numbered lines and explicit nested blocks, because indentation alone can conceal where an assumption is still open.

Formal background: [1].

Our original seven-line proof starts with (P∧Q)→R and establishes P→(Q→R). It shows two discharges at different levels and an invalid attempt to export Q afterward. A semantic truth check supports the result, while the line audit checks whether this particular derivation uses its rules correctly.

Read the nested goal from the outside inward

Premise: (P ∧ Q) → R
Goal: P → (Q → R)

Outer task: assume P; derive Q → R.
Inner task: assume Q; derive R.

The main connective of the goal is the outer arrow. Its consequent is itself a conditional. Open the P subproof first, then the Q subproof inside it. The premise needs P∧Q as input, so the two assumptions will let you construct that conjunction and obtain R.

An assumption is permission to reason conditionally, not a claim that the assumed sentence is actually true. The final goal explicitly records what was derived if those assumptions were supplied in the relevant order.

Follow all seven lines and their open blocks

On a narrow screen, scroll inside this table. Keyboard users can focus the region and use the arrow keys.

Download the complete proof, block ranges and invalid export

Line 4 combines accessible P and Q. Line 5 uses the premise’s whole antecedent P∧Q, not P alone, to eliminate its conditional. Line 6 closes the Q block, whose range is 3–5, and writes Q→R at the P block’s level.

Line 7 closes the outer block. Its endpoint is line 6, where Q→R is available at the outer block’s own level. The inner R at line 5 is not a substitute endpoint for that goal. It belongs to the deeper Q subproof.

The rightmost column lists open temporary assumptions, rather than all proof dependencies. The premise on line 1 remains undischarged throughout and supports the final result. “None” in the last row therefore means no temporary assumption is open; it does not mean the proof has no premise.

Check the endpoint’s level as well as its formula

A valid →I range starts with the assumption being discharged and ends with the consequent at that subproof’s own level. You may use nested subproofs while deriving it, but an endpoint still inside an inner block does not finish the surrounding block. Close the inner work and obtain the needed sentence at the correct level first.

For example, citing 2–5 in this proof as though it established P→R would take an endpoint that still depends on the temporary Q assumption. That shortcut does not discharge Q. At P=T,Q=F,R=F, the original premise is true because P∧Q is false, yet P→R is false. The shortcut changes the claim and is invalid.

Formal background: [1].

The correct range 2–6 ends at Q→R, so the consequent of the outer conditional is precisely Q→R. Match formulas as structured sentences, not just their final letters. P→(Q→R) differs from P→R.

Reject a line that leaks out of a closed block

Proposed line 8: Q     Reiteration, 3
Diagnosis: not licensed; line 3 belongs to a closed subproof.

After line 7, both temporary blocks are closed. You may cite the exported conditional at line 7, and you still have premise line 1. You may not cite line 3 individually to reiterate Q outside its block. Its earlier line number does not make it accessible.

A complete countervaluation makes the danger visible: take P=F,Q=F,R=F. Premise (P∧Q)→R is F→F=T and the legitimate final conditional P→(Q→R) is T, but Q is false. Exporting Q would convert a temporary assumption into an unsupported conclusion.

Range citation and ordinary line citation do different work. →I may cite a recently completed subproof range to discharge its assumption. Reiteration needs an individually accessible earlier line. Permission to cite the range never gives blanket permission to reuse every line inside it.

Carry surrounding premises and assumptions honestly

If you prove A→B while another assumption C is still open, the conditional may still depend on C. →I removes the discharged A assumption from that subproof; it does not discharge C or an undischarged premise. Record the outer context before applying the rule.

This distinction helps when translating a proof into prose. The seven-line result says that, given the original premise, if P holds then Q would imply R. It does not establish P, Q or R unconditionally. You can later use →E if you separately have P, and then use it again if you separately have Q.

When auditing your own proof, mark each assumption’s start, its intended endpoint, and the level where the exported conditional will appear. Check each cited individual line against the current open blocks. This prevents a polished-looking indentation diagram from hiding a dependence error.

Try six discharge and accessibility checks

Use the displayed seven-line proof unless a different assignment is specified.