# Why Peirce's law implies law of excluded middle?

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?

-
You can prove this by using uniform substitution, modus ponens, and the law of simplification, given that Peirce's law and the law of the excluded middle are axioms. –  Doug Spoonwood Jul 19 '13 at 12:59
law of the excluded middle is not an axiom, I want to prove that if the Peirce's law is true implies that the law of excluded middle is true –  Robbo Jul 19 '13 at 13:10
You need to know what system you're talking about before you can answer your question, before you can prove that Peirce's law implies the law of excluded middle. In the implicational calculus, Peirce's law holds, but (P∨¬P) does not, because there does not exist any ¬ connective, nor any ∨ connective. In classical logic and some non-classical logics you can prove (P∨¬P) without it coming as an axiom, also prove (((P→Q)→P)→P) and then use ((P→Q)→P)→P to prove (P∨¬P) again (within the system). –  Doug Spoonwood Jul 19 '13 at 19:49
What formal system do you have in mind? From my understanding of definitions of a formal system, you can consider Peirce's law under just modus ponens, and uniform substitution as a formal system. It still has a potential infinity of theorems (all less general than Peirce's law). You certainly can't derive the law of the excluded middle in that system. See the end of my answer. –  Doug Spoonwood Jul 20 '13 at 0:22

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$

-
I think you've confused a rule of inference with a logical theorem. You've also assumed that "∨" (as well as ¬) comes as a meaningful connective in a system. In some logical systems, it just abbreviates other formulas. –  Doug Spoonwood Jul 19 '13 at 12:53
@DougSpoonwood Indeed, I mixed rules and theorems (the proof would be painful otherwise), and I do assume nontrivial things about $\neg$ and $\lor$. In various systems this proof would look different, I picked intuitionistic logic (with $\lor$) and that's it. In fact this proof is a rewritten $\lambda$-term: $$\mathrm{with\_return}\ (\lambda k.\ \mathrm{Right}\ \lambda p.\ k\ (\mathrm{Left}\ p)),$$ where $\mathrm{with\_return}$ has the Peirce's law type and Left/Right are constructors of sum type (there are the $\lor$-related assumptions). –  dtldarek Jul 19 '13 at 13:13
Ignoring the problem that this answer assumes a lot more than we know that the question asker allows, the original question states Peirce's law. This answer applies Peirce's rule of inference. It is not at all difficult to start with Perice's law and derive Peirce's rule of inference. Why did this not get done? –  Doug Spoonwood Aug 5 '13 at 23:08
@DougSpoonwood Because the answer was already lengthy, and I didn't want to complicate it anymore. –  dtldarek Aug 6 '13 at 7:10
@DougSpoonwood Edited, I hope it's more to you liking now. –  dtldarek Aug 6 '13 at 7:36

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$.

-
In line 3 it assumes that the negation of excluded middle is false, is not this equivalent to assuming that the excluded middle is true? –  Robbo Jul 19 '13 at 11:51
Good point. You're right that that line seems to assume what's trying to be proven, but (if you click on the link to that "rule") you'll notice that they derive it by deriving that $\neg(p \vee \neg p)$ implies $\neg p \wedge \neg \neg p$, using one of De Morgan's Laws. And it turns out that this particular De Morgan law is valid for most standard logics with negation, though indeed it is still an implicit assumption in the proof. –  Alex Kocurek Jul 19 '13 at 16:53

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.

-