# Peirce's law from an intuitionistic viewpoint

Peirce's Law may serve as a purely implicational axiom which can substitute for Tertium Non Datur as a basis for classical logic. What is remarkable about it is that it contains no instance of NOT ($\neg$), no instance of FALSUM ($\bot$), besides not containing any conjunction or disjunction; also it contains no subformula that would be obviously equivalent to FALSUM.

## Proving Peirce's Law from TND (Tertium Non Datur)

The formula
    $\phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$
is valid because it is an instance of Axiom THENiC (THEN introduction Consequent).
Following is a proof of $\neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$:
| index | formula | justification |
| 1 | $\neg \phi$ | Hypothesis |
| 2 | $\neg \phi \supset (\phi \supset \psi )$ | Theorem ECQ |
| 3 | $\phi \supset \psi$ | MP 1, 2 |
| 4 | $(\phi \supset \psi )\supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$ | Quoted MP (see below) |
| 5 | $((\phi \supset \psi )\supset \phi )\supset \phi$ | MP 3, 4 |
| 6 | $\neg \phi \vdash ((\phi \supset \psi )\supset \phi )\supset \phi$ | Summary 1; 5 |
| 7 | $\vdash \neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$ | DT 6 |
Quoted MP:
| index | formula | justification |
| 1 | $\alpha ,\ \alpha \supset \beta \vdash \beta$ | Modus Ponens |
| 2 | $\alpha \vdash (\alpha \supset \beta )\supset \beta$ | DT 1 |
| 3 | $\vdash \alpha \supset ((\alpha \supset \beta )\supset \beta )$ | DT 2 |
Main:
| index | formula | justification |
| 1 | $(\alpha \supset \beta )\supset ((\neg \alpha \supset \beta )\supset (\alpha \vee \neg \alpha \supset \beta ))$ | Axiom ORiA (OR introduction Antecedent) |
| 2 | $\phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$ | Axiom THENiC |
| 3 | $\neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$ | Theorem (just proved above) |
| 4 | $(\neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ])\supset (\phi \vee \neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ])$ | MP 2, 1; letting $\alpha =\phi$ and $\beta =((\phi \supset \psi )\supset \phi )\supset \phi$ |
| 5 | $\phi \vee \neg \phi \supset [((\phi \supset \psi )\supset \phi )\supset \phi ]$ | MP 3, 4 |

## Proving TND from Peirce's Law

Proving the converse is harder. Here is a proof sketch: From assuming Peirce's Law may be derived the Consequentia Mirabilis. From Consequentia Mirabilis may be derived DNe (Double Negation elimination). From $\neg \neg {\mbox{TND}}$ and DNe may be derived TND.
| index | formula | justification |
| 1 | $((\phi \supset \psi )\supset \phi )\supset \phi$ | Peirce's Law |
| 2 | $((\phi \supset \bot )\supset \phi )\supset \phi$ | Replace $\psi$ with $\bot$ in 1. |
| 3 | $(\phi \supset \bot )\equiv \neg \phi$ | Definition of NOT (axiom) |
| 4 | $(\neg \phi \supset \phi )\supset \phi$ | Substitute 3 in 2 |
This is the Consequentia Mirabilis. This is the one (out of two versions) which is classically valid but not generally intuitionistically valid. Here it is intuitionistically true because of the assumption of Peirce's Law. The other version is:
    $(\phi \supset \neg \phi )\supset \neg \phi$
and this one is valid intuitionistically; it is called Clavius's Law.
From Consequentia Mirabilis derive DNe.
| index | formula | justification |
| 1 | $\neg \neg \alpha$ | Hypothesis |
| 2 | $\neg \neg \alpha \equiv (\neg \alpha \supset \bot$) | Definition of NOT (axiom) |
| 3 | $\neg \alpha \supset \bot$ | Substitute 2 in 1 |
| 4 | $\bot \supset \alpha$ | Axiom EFQ (Ex Falso Quodlibet) |
| 5 | $\neg \alpha \supset \alpha$ | THEN Transitivity (IR) 3, 4 |
| 6 | $(\neg \alpha \supset \alpha )\supset \alpha$ | Consequentia Mirabilis |
| 7 | $\alpha$ | MP 5, 6 |
| 8 | $\neg \neg \alpha \vdash \alpha$ | Summary 1; 7 |
| 9 | $\vdash \neg \neg \alpha \supset \alpha$ | DT 8 |
Transitivity of Implication, a theorem which may be proven with the Deduction Theorem:
| index | formula | justification |
| 1 | $\alpha \supset \beta$ | Hypothesis |
| 2 | $\beta \supset \gamma$ | Hypothesis |
| 3 | $\alpha$ | Hypothesis |
| 4 | $\beta$ | MP 3, 1 |
| 5 | $\gamma$ | MP 4, 2 |
| 6 | $\alpha \supset \beta ,\ \beta \supset \gamma ,\ \alpha \vdash \gamma$ | Summary 1, 2, 3; 5 |
| 7 | $\alpha \supset \beta ,\ \beta \supset \gamma \vdash \alpha \supset \gamma$ | DT 6 |
| 8 | $\alpha \supset \beta \vdash (\beta \supset \gamma )\supset (\alpha \supset \gamma )$ | DT 7 |
| 9 | $\vdash (\alpha \supset \beta )\supset ((\beta \supset \gamma )\supset (\alpha \supset \gamma ))$ | DT 8 |
Line 7 shows the Inference Rule (IR) form of it. Another name for this theorem is Hypothetical Syllogism, and it may well be that in some proof systems it is an axiom.
Proof of $\neg \neg {\mbox{TND}}$:
| index | formula | justification |
| 1 | $\phi \supset \phi \vee \neg \phi$ | Axiom ORiL (OR introduction Left) |
| 2 | $\neg \phi \supset \phi \vee \neg \phi$ | Axiom ORiR (OR introduction Right) |
| 3 | $\neg (\phi \vee \neg \phi )\supset \neg \phi$ | Contraposition (IR) 1 |
| 4 | $\neg (\phi \vee \neg \phi )\supset \neg \neg \phi$ | Contraposition (IR) 2 |
| 5 | $(\alpha \supset \beta )\supset ((\alpha \supset \neg \beta )\supset \neg \alpha )$ | Reductio Ad Absurdum |
| 6 | $(\neg (\phi \vee \neg \phi )\supset \neg \neg \phi )\supset \neg \neg (\phi \vee \neg \phi )$ | MP 3, 5 where $\alpha =\neg (\phi \vee \neg \phi )$, $\beta =\neg \phi$ |
| 7 | $\neg \neg (\phi \vee \neg \phi )$ | MP 4, 6 |
Note that $\neg \neg {\mbox{TND}}$ is intuitionistically valid. A generalization of this fact is Glivenko's Theorem, which states that for any classically valid formula, its double negation is intuitionistically valid.
Exercise: Prove the Law of Contraposition: $\alpha \supset \beta \vdash \neg \beta \supset \neg \alpha$.
Main part:
| index | formula | justification |
| 1 | $\neg \neg (\phi \vee \neg \phi )$ | Theorem $\neg \neg {\mbox{TND}}$ |
| 2 | $\neg \neg (\phi \vee \neg \phi )\supset (\phi \vee \neg \phi )$ | DNe |
| 3 | $\phi \vee \neg \phi$ | MP 1, 2 |
That is all. $\Box$
NB: $[((\phi \supset \psi )\supset \phi )\supset \phi ]\supset [\phi \vee \neg \phi ]$ is not generally true (intuitionistically); i.e., it is not valid. What does instead hold is that
    $\vdash ((\phi \supset \psi )\supset \phi )\supset \phi \qquad \Longrightarrow \qquad \vdash \phi \vee \neg \phi$;
in words, if Peirce's Law is valid then TND must be valid.
Dialogical disproof of $[((\phi \supset \psi )\supset \phi )\supset \phi ]\supset [\phi \vee \neg \phi ]$:
Game 1
| index | player | play | motive | |
| 0 | P | $[((\phi \supset \psi )\supset \phi )\supset \phi ]\supset [\phi \vee \neg \phi ]$ | | |
| 1 | O | $((\phi \supset \psi )\supset \phi )\supset \phi$ | A0 | |
| 2 | P | $\phi \vee \neg \phi$ | D0 | |
| 3 | O | $?\vee$ | A2 | |
| 4 | P | $\neg \phi$ | D2 | |
| 5 | O | $\phi$ | A4 | |
| 6 | P | $(\phi \supset \psi )\supset \phi$ | | A1 |
| 7 | O | $\phi$ | | D1 |
In the "motive" column, A stands for "attack on", D stands for "defense of". Proponent's attack on 1 at 6 fails, because Opponent defends 1 at 7 and Proponent cannot attack 7. Proponent cannot parry Opponent's attack on 4 at 5, so Proponent's defense of 2 at 4 falls. Thus, Proponent's defense of 0 at 2 falls, so Opponent's attack on 0 at 1 stands. Opponent wins.
Game 2
| index | player | play | motive | |
| 0 | P | $[((\phi \supset \psi )\supset \phi )\supset \phi ]\supset [\phi \vee \neg \phi ]$ | | |
| 1 | O | $((\phi \supset \psi )\supset \phi )\supset \phi$ | A0 | |
| 2 | P | $(\phi \supset \psi )\supset \phi$ | | A1 |
| 3 | O | $\phi$ | | D1 |
| 4 | P | $\phi \vee \neg \phi$ | D0 | |
| 5 | O | $?\vee$ | A4 | |
| 6 | P | $\phi$ | D4 | |
Each attack of the Opponent is parried with a defense by the Proponent, so Proponent wins.
Game 3
| index | player | play | motive | | |
| 0 | P | $[((\phi \supset \psi )\supset \phi )\supset \phi ]\supset [\phi \vee \neg \phi ]$ | | | |
| 1 | O | $((\phi \supset \psi )\supset \phi )\supset \phi$ | A0 | | |
| 2 | P | $(\phi \supset \psi )\supset \phi$ | | A1 | |
| 3 | O | $\phi \supset \psi$ | | | A2 |
Proponent cannot answer Opponent's attack on 2 at 3, because Proponent cannot introduce $\phi$, since it is atomic and it has not been previously introduced by Opponent. So Opponent's attack on 2 at 3 stands, so Proponent's attack on 1 at 2 falls, so Opponent's attack on 0 at 1 stands, so Proponent's initial proposition at 0 falls. Opponent wins. Proponent has no winning strategy, therefore the proposed proposition is (intuitionistically) invalid.
Proof of Reductio Ad Absurdum.
| index | formula | justification |
| 1 | $\alpha \supset \beta$ | Hypothesis |
| 2 | $\alpha \supset \neg \beta$ | Hypothesis |
| 3 | $\beta \supset \neg \alpha$ | Pisces Thm. (IR) 2 |
| 4 | $\alpha \supset \neg \alpha$ | THEN Transitivity (IR) 1, 3 |
| 5 | $(\alpha \supset \neg \alpha )\supset \neg \alpha$ | Lex Clavia |
| 6 | $\neg \alpha$ | MP 4, 5 |
| 7 | $\alpha \supset \beta ,\ \alpha \supset \neg \beta \vdash \neg \alpha$ | Summary 1, 2; 6 |
| 8 | $\alpha \supset \beta \vdash (\alpha \supset \neg \beta )\supset \neg \alpha$ | DT 7 |
| 9 | $\vdash (\alpha \supset \beta )\supset ((\alpha \supset \neg \beta )\supset \neg \alpha )$ | DT 8 |
Exercise: Intuitionistically prove the Pisces Theorem: $(\alpha \supset \neg \beta )\supset (\beta \supset \neg \alpha )$.
Exercise: Intuitionistically prove Lex Clavia.
Proof of Ex Contradictione (Sequitur) Quodlibet (ECQ).
| index | formula | justification |
| 1 | $\neg \phi$ | Hypothesis |
| 2 | $\neg \phi \equiv (\phi \supset \bot )$ | Axiom Definition of NOT |
| 3 | $\phi \supset \bot$ | Substitute 2 in 1 |
| 4 | $\bot \supset \psi$ | Axiom EFQ |
| 5 | $\phi \supset \psi$ | Thm. THEN Transitivity 3, 4 |
| 6 | $\neg \phi \vdash \phi \supset \psi$ | Summary 1; 5 |
| 7 | $\vdash \neg \phi \supset (\phi \supset \psi )$ | DT 6 |
In some proof systems RAA and ECQ are axioms.

### Alternative proof of TND from PL

Start by showing that Peirce's Law entails the Consequentia Mirabilis (as was done previously). Then
| index | formula | justification |
| 1 | $P\supset P\vee \neg P$ | ORiL |
| 2 | $\neg (P\vee \neg P)\supset \neg P$ | Contraposition (IR) 1 |
| 3 | $\neg P\supset P\vee \neg P$ | ORiR |
| 4 | $\neg (P\vee \neg P)\supset P\vee \neg P$ | THEN Composition 2, 3 |
| 5 | $[\neg (P\vee \neg P)\supset P\vee \neg P]\supset P\vee \neg P$ | Consequentia Mirabilis |
| 6 | $P\vee \neg P$ | MP 4, 5 |
THEN Composition is another name for THEN Transitivity; the implications may be thought as composing like the morphisms of a thin category. $\Box$