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$

References

Search for Consequentia mirabilis on Wikipedia.

Search for Double-negation translation on Wikipedia.

• Dialogical Logic by Thomas Piecha at Internet Encyclopedia of Philosophy
• Why Peirce's law implies law of excluded middle? (answer by dtldarek) at Math StackExchange.