Hypothetical syllogism

The idea

Chain implications: if P → Q and Q → R, then P → R.

This is transitivity of implication. It combines →-Intro and →-Elim in a single proof, making it the first multi-rule derivation in this track. You assume P (via →-Intro), apply P → Q to get Q (via →-Elim), then apply Q → R to get R (via →-Elim again).

How the tree grows

Watch how the proof tree is built step by step. First we open the assumption, then we chain two eliminations, and finally the introduction rule closes the assumption.

        [P]¹    P → Q
        ———————————— →-Elim
            Q       Q → R
           ———————————— →-Elim
                 R
        ———————————————— →-Intro¹
              P → R

Watch the proof build

In any prover

Prover	Syntax
Lean 4	`intro hp; exact hqr (hpq hp)`
Coq	`intro HP; apply HQR; apply HPQ; exact HP`
Agda	`λ hp → hqr (hpq hp)`

Your turn

Extend to four: given P → Q, Q → R, R → S, construct the Gentzen tree for P → S.

Hint

The structure is the same — you just chain one more →-Elim. Assume P, apply P → Q, then Q → R, then R → S.

Solution

  [P]¹  P → Q
  —————————— →-Elim
      Q    Q → R
     —————————— →-Elim
          R    R → S
         —————————— →-Elim
              S
—————————————————— →-Intro¹
           P → S

Three →-Elim applications chained inside one →-Intro.

← Modus ponens ∧-Intro →