To prove P → Q, assume P and derive Q.
This is the most common proof opening. Whenever your goal is an implication, you begin by assuming the antecedent and working towards the consequent. The assumption is marked with a superscript label (here ¹) that ties it to the rule application that discharges it.
[P]¹ ⋮ Q ——————— →-Intro¹ P → Q
The square brackets around P indicate a discharged assumption: P was temporarily assumed and is no longer needed after the rule fires. The superscript ¹ links the assumption to the specific rule application that discharges it.
| Prover | Syntax |
|---|---|
| Lean 4 | intro h |
| Coq | intro H |
| Agda | λ h → |
Draw the Gentzen tree for ⊢ P → (Q → P). Which rule do you use twice?
You need to introduce two implications. Each one requires →-Intro. Start by assuming P, then assume Q, and notice that P is already in your assumptions.
[P]²
——————— →-Intro¹
Q → P
——————————— →-Intro²
P → (Q → P)
You use →-Intro twice — once to discharge the assumption of Q (labelled ¹) and once to discharge P (labelled ²).
See also: Logic §02 — Implication | Strategies §01 — Direct proof