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?

  • $\begingroup$ 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. $\endgroup$ Jul 19, 2013 at 12:59
  • 1
    $\begingroup$ 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 $\endgroup$
    – Robbo
    Jul 19, 2013 at 13:10
  • $\begingroup$ 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). $\endgroup$ Jul 19, 2013 at 19:49
  • $\begingroup$ 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. $\endgroup$ Jul 20, 2013 at 0:22

5 Answers 5



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$

  • $\begingroup$ 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. $\endgroup$ Jul 19, 2013 at 12:53
  • 2
    $\begingroup$ @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). $\endgroup$
    – dtldarek
    Jul 19, 2013 at 13:13
  • $\begingroup$ 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? $\endgroup$ Aug 5, 2013 at 23:08
  • $\begingroup$ @DougSpoonwood Because the answer was already lengthy, and I didn't want to complicate it anymore. $\endgroup$
    – dtldarek
    Aug 6, 2013 at 7:10
  • $\begingroup$ @DougSpoonwood Edited, I hope it's more to you liking now. $\endgroup$
    – dtldarek
    Aug 6, 2013 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$.

  • $\begingroup$ 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? $\endgroup$
    – Robbo
    Jul 19, 2013 at 11:51
  • $\begingroup$ 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. $\endgroup$ Jul 19, 2013 at 16:53

The most concise approach is to note that whenever $P\to Q$ holds, $P$ is equivalent to $P\land Q$. In turn, one finds $((P\to Q)\to P)\to P$ is equivalent to the variant in which the second $P$ is replaced with $P\land Q$. Assuming the principle and considering $Q=\bot$, with $(P\land Q)=\bot$ we arrive at $\neg\neg P\to P$. And the double-negated excluded middle is intuitionistically valid.

For completeness, the other direction also has a quick proof: We want to first consider the simple schema $(P\lor R)\to ((R\to P)\to P)$, which holds via implication introduction on the one hand and modus ponens on the other. Now consider $A:=(P\to Q)$ and observe that the principle of explosion says $\neg P\to A$. The above thus gives $(P\lor \neg P)\to (((P\to Q)\to P)\to P)$.


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


First, let us prove that $$\big((P \vee \neg P) \rightarrow \text{False}\big) \rightarrow \neg P$$ by thinking of proofs of an implication $Q \rightarrow R$ as functions from $Q$ to $R$, and of $\neg P$ as the implication $P \rightarrow \text{False}$ (by definition of $\neg P$).

To prove the implication above, assume that we are given a proof $f$ of $(P \vee \neg P) \rightarrow \text{False}$ (i.e. a function from $P \vee \neg P$ to $\text{False}$). We then want to construct a proof of $P \rightarrow False$, meaning a function from $P$ to $\text{False}$. To do that, we start with a proof $p$ of $P$. Recall now that $P$ implies $P \vee \neg P$ (this implication is a tautology: regardless of $P$, we have a function $l : P \rightarrow (P \vee \neg P)$, by definition of $\vee$). So we can associate to $p$ a proof $l(p)$ of $P \vee \neg P$. Then $f(l(p))$ is a proof of $\text{False}$ and we are done.

Second, let us note that, since $\neg P \rightarrow (P \vee \neg P)$ is also a tautology (meaning that, regardless of $P$, we have a function $r : \neg P \rightarrow (P \vee \neg P)$, again by definition of $\vee$), we can construct a proof $t := r(f(l(p)))$ of $(P \vee \neg P)$. Thus, the function $f \mapsto t$ is a proof of the implication $$\big((P \vee \neg P) \rightarrow \text{False}\big) \rightarrow (P \vee \neg P).$$

If we now assume that we have a proof of Peirce's law, meaning a function $$ \pi : \big((Q \rightarrow R) \rightarrow Q\big) \rightarrow Q$$ and apply it with $Q = P \vee \neg P$ and $R = \text{False}$, we obtain a proof $\pi(t)$ of $P \vee \neg P$.

PS: The arguments above can be checked in a proof assistant. I post below the corresponding Lean 4 code.

theorem LEM_from_LEM_implies_False (P : Prop) : ((P ∨ ¬P) → False) → (P ∨ ¬P) :=
  fun (f : (P ∨ ¬P) → False) => Or.inr (fun (p : P) => f (Or.inl p))

axiom Peirce (Q R : Prop) : ((Q → R) → Q) → Q

theorem LEM_from_Peirce (P : Prop) : P ∨ ¬P :=
  Peirce (P ∨ ¬P) False (LEM_from_LEM_implies_False P)

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .