Intereting Posts

Relating $\operatorname{lcm}$ and $\gcd$
Independence and Events.
How to calculate interpolating splines in 3D space?
Classic birthday problem turned on its head: With $N$ people, how many are likely to share most common birthday?
Maximum amount willing to gamble given utility function $U(W)=\ln(W)$ and $W=1000000$ in the game referred to in St. Petersberg's Paradox?
What is the probability of having a pentagon in 6 points
Get the last two digits of $16^{100}$ and $17^{100}$
Monte Carlo double integral over a non-rectangular region (Matlab)
Stirling-like sum equal to zero when $k>n$
Getting the sequence $\{1, 0, -1, 0, 1, 0, -1, 0, \ldots\}$ without trig?
Sequence of measurable functions
Ways to prove $\displaystyle \int_0^\pi dx \dfrac{\sin^2(n x)}{\sin^2 x} = n\pi$
What does it mean that we can diagonalize the metric tensor
Uniqueness of continuous extension from $A$ to $\overline{A}$ for maps into a Hausdorff space
Analytic continuation for $\zeta(s)$ using finite sums?

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?

- Help me put these enormous numbers in order: googol, googol-plex-bang, googol-stack and so on
- Is it possible to iterate a function transfinite times?
- What is the Tarski–Grothendieck set theory about?
- Prove :(P → Q) ∨ (Q → P) using natural deduction
- What are good resources for learning predicate logic / predicate calculus?
- An (apparently) vicious circle in logic
- What is a type?
- Boolean algebras without atoms
- Justification of ZFC without using Con(ZFC)?
- Proving that a propositional theory of any cardinality has an independent set of axioms

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

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

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:

- All lower case letters of the Latin alphabet qualify as formulas.
- If $\alpha$ qualifies as a formula, so dose N$\alpha$
- If $\alpha$ and $\beta$ qualify as a formulas, so does C$\alpha$$\beta$, and A$\alpha$$\beta$.
- 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.

- A calculus problem with functions such that $f''(x) = g(x)$ and $g''(x) = f(x)$
- Question about Subrings and integraly closed
- Bound on nilpotency index of endomorphisms
- What is the expected value of the number of die rolls necessary to get a specific number?
- Explicit homeomorphism between open and closed rational intervals?
- Applied ODEs in trajectory problem
- Proof of the affine property of normal distribution for a landscape matrix
- Integrate $ \int_0^\infty ( x A+I)^{-1} A -I \frac{1}{c+x} dx $ where $A$ is psd and $c>0$
- Hamilton's three dimensional algebra
- Method of Steepest descent integral
- REVISITED $^2$: Does a solution in $\mathbb{R}^n$ imply a solution in $\mathbb{Q}^n$?
- Every order topology is regular (proof check)
- What is spectrum for Laplacian in $\mathbb{R}^n$?
- Why are these geometric problems so hard?
- If $a$ is a quadratic residue modulo every prime $p$, it is a square – without using quadratic reciprocity.