Why Peirce's law implies law of excluded middle?

Question

Why if in a formal system the Peirce's law $((P\rightarrow Q)\rightarrow P) \rightarrow P$ is true, the law of excluded middle $P \lor \neg P$ is true too?

Answer 1

Intuition:

Peirce's law is of the form $$\big((A \to B) \to A\big) \quad \to \quad A,$$ that is, given $(A \to B) \to A$ we could deduce $A$. Therefore, we will try to construct $$((P \lor \neg P) \to \bot) \to (P \lor \neg P).$$ The trick is that for any $A \to B$ we can strengthen $A$ or relax $B$, for example:

\begin{align} P\lor \neg P &\to \bot &\text{implies}&& P &\to \bot,\\ P &\to P &\text{implies}&& P &\to P \lor \neg P. \end{align} So we could start with a tautology (I assume that negation is just a shorthand for $\to \bot$) \begin{align} \neg P &\to \neg P \\ (P \to \bot) &\to \neg P \end{align} strengthen left side $$(P \lor \neg P \to \bot) \to \neg P$$ and relax right side $$(P \lor \neg P \to \bot) \to P \lor \neg P.$$

Now we apply Peirce's law, and we are done ;-)

Things used:

• negation $\neg P$ is a shorthand for $P \to \bot$,
• identity: $\dfrac{\quad}{\Gamma, A \vdash A}[\alpha]$
• application: $\dfrac{\Gamma \vdash A, A \to B}{\Gamma \vdash B}[\beta]$
• finite composition $\dfrac{\Gamma \vdash A_1 \to A_2, A_2 \to A_3, \ldots, A_{n-1} \to A_n}{ \Gamma \vdash A_1 \to A_n}[\gamma]$,
• disjunction introduction: $\dfrac{}{\Gamma, A \vdash A \lor B}[\delta]$,
• implication: $\dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B}[\iota]$,
• Peirce's law $\dfrac{}{\Gamma \vdash ((A\to B) \to A) \to A}[\pi]$.

The proof:

The premise

$$ \dfrac{ \dfrac{ \dfrac{ \frac{}{P \to P \lor \neg P}{[\delta,\iota]}, \quad \frac{}{P \lor \neg P \to \bot \vdash P \lor \neg P \to \bot}[\alpha] }{P\lor\neg P \to \bot \vdash P \to \bot}[\gamma] }{(P\lor\neg P\to \bot) \to \neg P}[\iota], \quad \dfrac{\quad}{\neg P \to P \lor \neg P}[\delta, \iota] }{(P \lor \neg P \to \bot) \to P \lor \neg P}[\gamma] $$

and final derivation

$$ \dfrac{ \dfrac{\text{from above} }{(P \lor \neg P \to \bot) \to P \lor \neg P}, \ \dfrac{}{((P \lor \neg P \to \bot) \to P \lor \neg P) \to P \lor \neg P}[\pi] }{P \lor \neg P}[\beta] $$

There are various shortcuts, and implicit assumptions, most notably negation $\neg P$ is a shorthand for $P \to \bot$, be careful! Nevertheless, I hope it still helps $\ddot\smile$

Answer 2

This is probably what you're looking for: Peirce's Law Equivalent to Law of Excluded Middle. Note, however, that this proof depends on a few assumptions which are not embodied in every logic. For instance, in relevance logic, the move from $\neg p$ to $p \rightarrow q$ is invalid, since $p$ may not be relevant to $q$.

Answer 3

Why? Because you can prove it. A formal system has no (or minimal) reference to meaning, and consequently any logical theorem holds, because you can prove it given the axiom set and the rules of inference of the system. I'll outline a formal system where you can prove the law of the excluded middle ApNp and Peirce's law CCCpqpp. First formation rules:

1. All lower case letters of the Latin alphabet qualify as formulas.
2. If $\alpha$ qualifies as a formula, so dose N$\alpha$
3. If $\alpha$ and $\beta$ qualify as a formulas, so does C$\alpha$$\beta$, and A$\alpha$$\beta$.
4. The above rules come as sufficient for what follows.

The system (and almost all of the proofs below can get credited to the work of Jan Lukasiewicz and the publishers and translators of Lukasiewicz's Elements of Mathematical Logic) has three axioms:

1 CCpqCCqrCpr (hypothetical syllogism)

2 CCNppp

3 CpCNpq

In words you can translate the first axiom as saying "if the first (proposition) implies the second, if the second implies the third, then the first implies the third". The second axiom can get translated into English as saying "if the negation of the first implies the first, then the first." The third axiom can get translated as saying "if the first, then, if not the first, then the second." The system has one definition

4' Apq:=CNpq

It has three inference rules

S: For any lower case letter $\lambda$ within any axiom we may uniformly substitute it with any other formula, provided that such substitution happens for all lower case letters equiform with $\lambda$ in that formula. For instance, were it the case that CpCqp came as an axiom of our system, we could substitute p with Cpp in CpCqp (substitutions will get abbreviated by the notation p/Cpp hereafter) and obtain C Cpp Cq Cpp, but not C Cpp C qp. We can also apply such uniform substitution to any theorem we have derived already.

R: For any formula where Xpq, or some substitution instance of Xpq, we may replace Xpq with Yrs, where we have a definition such that we have definition Yrs:=Xpq, where the variables of Yrs contain only equiform variables with Xpq. Such replacement does not have to happen uniformly for the formula. It can happen only in one place within a formula. In particular here this means that if we have some theorem like CCNpqCqCNpq, we may replace either instance of CNpq in CCNpqCqCNpq with Apq, to yield CApqCqCNpq.

D: If we have a theorem C$\alpha$$\beta$ and $\alpha$ qualifies as a theorem also, we may detach $\beta$ as a theorem also.

So, first we'll prove the law of the excluded middle, in symbols ApNp. The notation "1, p/q" indicates that we will uniformly substitute formula p in the formula reference by the numeral 1 with q. The "=" sign gets used to indicated that the formula on the left of the "=" sign comes as equiform with the formula on the right side of the "=" sign. The notation C1-2 indicates that formula 1 comes as the antecedent or first formula which the C on the leftmost of the formula connects, 2 comes as the consequently or second formula which the C on the leftmost of the formula connects, and the "-" indicates that we will detach formula 2 as a theorem. The notation 3 R = 4 indicates that we will replace formula 3, which comes as a substitution instance of CNpq, with the formula Apq (p and q remain equiform throught CNpq and Apq) and obtain theorem 4.

1 CCpqCCqrCpr axiom

2 CCNppp axiom

3 CpCNpq axiom

 1 q/CNpq = 4

4 C CpCNpq CCCNpqrCpr

 4 = C 3 - 5

5 CCCNpqrCpr

 5 q/p, r/p = 6

6 C CCNppp Cpp

 6 = C 3 - 7

7 Cpp

 7 p/Np = 8

8 CNpNp

 8 R = 9

9 ApNp

Next we'll prove prove CqCpq so that we can prove any two theorems from another theorem within this system.

  1 p/Cpq, q/CCqrCpr, r/s = 10

10 C CCpqCCqrCpr CCCCqrCprsCCpqs

  10 = C 1 - 11

11 CCCCqrCprsCCpqs

  11 q/Cqr, r/Csr, s/CCsqCpCsr = 12

12 C CCCCqrCsrCpCsrCCsqCpCsr CCpCqrCCsqCpCsr

  11 p/s, s/CpCsr = 13

13 CCCCqrCsrCpCsrCCsqCpCsr

  12 = C 13 - 14

14 CCpCqrCCsqCpCsr

  11 s/CCCprsCCqrs = 15    

15 C CCCqrCprCCCprsCCqrs CCpqCCCprsCCqrs

  1 p/Cqr, q/Cpr, r/s = 16

16 CCCqrCprCCCprsCCqrs

  15 = C 16 - 17

17 CCpqCCCprsCCqrs

  14 p/Cpq, q/CCprs, r/CCqrs, s/t = 18

18 C CCpqCCCprsCCqrs CCtCCprsCCpqCtCCqrs

  18 = C17 - 19

19 CCtCCprsCCpqCtCCqrs

  5 r/CCCNpppCCqpp = 20

20 C CCNpqCCCNpppCCqpp CpCCCNpppCCqpp

  17 p/Np, r/p, s/p = 21

21 CCNpqCCCNpppCCqpp

  20 = C 21 - 22

22 CpCCCNpppCCqpp

  22 p/CCNppp = 23

23 C CCNppp CCCNCCNpppCCNpppCCNpppCCqCCNpppCCNppp

  23 = C 2 -24

24 C CCNCCNpppCCNpppCCNppp CCqCCNpppCCNppp

  2 p/CCNppp = 25

25 CCNCCNpppCCNpppCCNppp

  24 = C 25 - 26

26 CCqCCNpppCCNppp

  5 p/t, q/CCNppp, r/CCNppp = 27

27 C CCNtCCNpppCCNppp CtCCNppp

  26 q/Nt = 28

28 CCNtCCNpppCCNppp

  27 = C 28 - 29

29 CtCCNppp

  19 p/Np, r/p, s/p = 30 

30 C CtCCNppp CCNpqCtCCqpp

  30 = C 29 - 31

31 CCNpqCtCCqpp

  1 p/CNpq, q/CtCCqpp = 32

32 C CCNpqCtCCqpp CCCtCCqpprCCNpqr

  32 = C 31 - 33

33 CCCtCCqpprCCNpqr

  33 t/NCCqpp, r/CCqpp = 34

34 C CCNCCqppCCqppCCqpp CCNpqCCqpp

  2 p/CCNqpp = 35

35 CCNCCNqppCCNqppCCNqpp

  35 = C 34 - 36

36 CCNpqCCqpp

  5 r/CCqpp = 37

37 C CCNpqCCqpp CpCCqpp

  37 = C 36 - 38

38 CpCCqpp

  38 p/q, q/Np = 39

39 CqCCNpqq

  14 p/q, q/CNpq, r/q, s/p = 40

40 C CqCCNpqq CCpCNpqCqCpq

  40 = C 39 - 41

41 C CpCNpq CqCpq

  41 = C 3 - 42

42 CqCpq

In words theorem 42 can get translated as "The first proposition implies that the second proposition implies the first proposition." Or equivalently, "The first proposition implies that if the second proposition, then the first proposition." On the strength of that you can show any proposition on the basis of any other proposition within this system (you might want to note exactly what the rule of substitution S says and what it does not say). Now we'll prove Peirce's law CCCpqpp.

  1 p/q, q/Cpq = 43

43 C CqCpq CCCpqrCqr

  43 = C 42 - 44 

44 CCCpqrCqr

  44 p/Nq, q/p, r/CCpqq = 45

45 C CCNqpCCpqq CpCCpqq

  36 p/q, q/p = 46

46 CCNqpCCpqq

  45 = C 45 - 47

47 CpCCpqq

  14 p/q, q/Cqr, s/p = 48

48 C CqCCqrr CCpCqrCqCpr

  47 p/q, q/r = 49

49 CqCCqrr

  48 = C 49 - 50

50 CCpCqrCqCpr

  1 p/CpCqr, q/CqCpr, r/s = 51

51 C CCpCqrCqCpr CCCqCprsCCpCqrs

  51 = C 50 - 52

52 CCCqCprsCCpCqrs

  52 q/Np, r/q, s/CCCpqpp = 53

53 C CCNpCpqCCCpqpp CCpCNpqCCCpqpp

  36 q/Cpq = 54 

54 CCNpCpqCCCpqpp

  53 = C 54 - 55

55 CCpCNpqCCCpqpp

  55 = C 3 - 56

56 CCCpqpp

So, now we'll prove the law of the excluded middle ApNp from Peirce's law CCCpqpp in this system.

  42 q/ApNp, p/CCCpqpp

57 C ApNp CCCCpqppApNp

  57 = C 9 - 58

58 CCCCpqppApNp

  58 = C 56 - 59

59 ApNp

But, even here, there exists a catch...

What what if we only had Perice's law with the rules of inference S, D, and R above? Could we prove the law of the excluded middle? Prover9 gave me the following matrix (with condensed detachment as a rule of inference, but that won't end up mattering here):

 A|  0  1|C| 0 1|N 
------------------
 0*| 1  0|0| 0 1|0
 1|| 0  0|1| 0 0|0

I've starred 0 to indicate it as the designated element here. If you write out the truth tables for CCCpqpp and ApNp here, you can see that CCCpqpp always evaluates to the designated element 0. However, when p=0, ApNp=A0N0=A00=1. Also, and it does come as important to check this also, if Cpq=0, and p=0, then q=0, so rule D comes as valid for this system. Rules R and D hold for this system, since the matrix above implies A, C, and N as truth-functional. Thus, from Peirce's law "alone" (the rules mentioned above preferably will get understood as implicit in this statement), you simply cannot derive the law of the excluded middle.