Inference Rules — Reference

Every rule of natural deduction, in four notations. Bookmark this page.

Implication (→)

→-Intro (Conditional proof)

  [P]¹
   ⋮
   Q
——————— →-Intro¹
 P → Q

Rule	Lean 4	Coq	Agda
→-Intro	`intro h`	`intro H`	`λ h →`

To prove P → Q: assume P, derive Q.

Practice: Proof Theory §01

→-Elim (Modus ponens)

 P    P → Q
——————————— →-Elim
      Q

Rule	Lean 4	Coq	Agda
→-Elim	`exact h hp` or `apply h`	`apply H`	`h hp`

If you have P and P → Q, conclude Q.

Practice: Proof Theory §02

Conjunction (∧)

∧-Intro

  P       Q
————————— ∧-Intro
   P ∧ Q

Rule	Lean 4	Coq	Agda
∧-Intro	`constructor` or `exact ⟨hp, hq⟩`	`split`	`hp , hq`

To prove P ∧ Q: prove P and prove Q separately.

Practice: Proof Theory §04

∧-Elim&sub1; and ∧-Elim&sub2;

 P ∧ Q              P ∧ Q
—————— ∧-Elim&sub1;     —————— ∧-Elim&sub2;
   P                  Q

Rule	Lean 4	Coq	Agda
∧-Elim&sub1;	`exact h.1`	`destruct H as [HP HQ]`	`proj&sub1; h`
∧-Elim&sub2;	`exact h.2`	`destruct H as [HP HQ]`	`proj&sub2; h`

From P ∧ Q, extract P (project left) or Q (project right).

Practice: Proof Theory §05

Disjunction (∨)

∨-Intro&sub1; and ∨-Intro&sub2;

    P                   Q
——————— ∨-Intro&sub1;    ——————— ∨-Intro&sub2;
  P ∨ Q              P ∨ Q

Rule	Lean 4	Coq	Agda
∨-Intro&sub1;	`exact Or.inl hp`	`left`	`inj&sub1; hp`
∨-Intro&sub2;	`exact Or.inr hq`	`right`	`inj&sub2; hq`

To prove P ∨ Q, it suffices to prove P alone (inject left) or Q alone (inject right).

Practice: Proof Theory §06

∨-Elim (Case analysis)

            [P]¹    [Q]²
             ⋮       ⋮
 P ∨ Q      R       R
——————————————————— ∨-Elim¹⋅²
            R

Rule	Lean 4	Coq	Agda
∨-Elim	`rcases h with hp \| hq`	`destruct H as [HP \| HQ]`	pattern matching with two clauses

If you have P ∨ Q, and both P → R and Q → R, then R.

Practice: Proof Theory §07

Negation (¬)

¬-Intro

 [P]¹
  ⋮
  ⊥
————— ¬-Intro¹
 ¬P

Rule	Lean 4	Coq	Agda
¬-Intro	`intro h` (since ¬P = P → False)	`intro H`	`λ h → …`

¬P means P → ⊥. To prove ¬P: assume P, derive a contradiction.

Practice: Proof Theory §08

⊥-Elim (Ex falso quodlibet)

  ⊥
————— ⊥-Elim
  P

Rule	Lean 4	Coq	Agda
⊥-Elim	`exact absurd hp hnp` or `contradiction`	`contradiction` or `exfalso`	`⊥-elim`

From ⊥ (absurdity), derive anything. Ex falso quodlibet.

Practice: Proof Theory §09

Quantifiers (∀, ∃)

Exercises coming soon. The rules are shown here for reference.

∀-Intro and ∀-Elim

  P(a)                ∀x. P(x)
———————— ∀-Intro*    ————————— ∀-Elim
∀x. P(x)              P(t)

* a must not appear free in any
  undischarged assumption

Rule	Lean 4	Coq	Agda
∀-Intro	`intro x`	`intro x`	`λ x →`
∀-Elim	`exact h t` or `specialize h t`	`specialize H t` or `apply H`	`h t`

∀-Intro: to prove ∀x. P(x), let x be arbitrary and prove P(x). The variable must be fresh. ∀-Elim: from ∀x. P(x), substitute any specific term t to get P(t).

∃-Intro and ∃-Elim

  P(t)                         [P(a)]¹
———————— ∃-Intro               ⋮
∃x. P(x)            ∃x. P(x)    C
                     ——————————————— ∃-Elim¹
                              C

                     * a must not appear free in C
                       or any undischarged assumption

Rule	Lean 4	Coq	Agda
∃-Intro	`exact ⟨t, ht⟩` or `use t`	`exists t`	`t , ht`
∃-Elim	`obtain ⟨a, ha⟩ := h`	`destruct H as [a Ha]`	pattern matching

∃-Intro: to prove ∃x. P(x), provide a specific witness t and a proof of P(t). ∃-Elim: from ∃x. P(x), introduce a fresh name a and assume P(a), then derive C (where a does not appear in C).

Notation guide

Symbol	Meaning
horizontal bar ———	From the above (premises), conclude the below (conclusion). This is the core of each inference rule.
[P]ⁿ	A discharged assumption. P was temporarily assumed during the derivation and is no longer needed after the rule labelled ⁿ fires.
⊢	"We can prove" — the turnstile. Γ ⊢ P means "from assumptions Γ, we can prove P."
⊥	Absurdity / falsehood. A proposition with no proof. Reaching ⊥ signals a contradiction.
⋮	A sub-derivation — one or more intermediate steps omitted for brevity.

← Home Proof Theory →