A subproof can contain another subproof. That lets you prove conclusions like $p \to (q \to r)$, where the consequent is itself a conditional, and even prove statements from no premises at all. This builds on Indirect Proof (IP) and Conditional Proof (CP).
🔑 Key idea
Subproofs nest like parentheses: the last one opened is the first one closed. Inside an inner subproof you may cite lines from the outer subproofs that are still open; after a subproof is closed, none of its lines can be cited. A proof must end with every subproof closed.
💡 Why it works
Each assumption is a supposition that holds only inside its own box. An inner box sits inside the outer one, so both suppositions are in force there. When the inner box closes, its supposition is discharged (turned into the antecedent of a conditional, or denied by IP), but the outer supposition is still on. Closing the outer box first would leave the inner supposition dangling, with nothing to discharge it.
Nested conditional proofs.
Theorems
A theorem is a formula that can be proved from no premises at all. Every theorem is a tautology. With CP and IP you can prove them: line 1 is an assumption, and the last line stands outside every subproof.
A theorem: no premises, two nested subproofs.
Worked examples
✏️ Worked example: Plan the assumptions
You want $(p \to q) \to (\neg q \to \neg p)$ from no premises. Plan.
The main connective is $\to$: assume $p \to q$ (line 1).
The consequent $\neg q \to \neg p$ is a conditional: assume $\neg q$ (line 2).
Line 3: $\neg p$ by MT 1, 2.
Close: line 4 $\neg q \to \neg p$ by CP 2–3; line 5 the theorem by CP 1–4.
Answer: Five lines.
✏️ Worked example: Which lines are available?
In the first proof above, can line 5 cite line 2?
Line 2 is the outer assumption; at line 5 the outer subproof is still open.
Answer: Yes.
Every formula proved from no premises is a tautology, and every tautology of statement logic can be proved this way.
Why prove theorems at all? A theorem is a logical truth: something that holds whatever the facts are. Proving one from nothing shows that the rules alone produce it, and it confirms the truth table, which would show the same formula is a tautology. Later, in Soundness and Completeness, you will see that this agreement is no accident.
⚠️ Common mistake
Closing the outer subproof before the inner one, or ending the proof with a subproof still open. Close innermost first, each with CP or IP citing its own range. The last line of the whole proof must stand at the left margin, outside every box; if it does not, it still depends on an assumption and has not been proved.
Practice
Pass with 3 right answers, the last 2 in a row. Each right answer earns 3 XP.