I have no training in formal logic and have tried to understand how Peirce's law is equivalent to the law of the excluded middle to no avail. I hope someone can explain this to me.
Also, in passing, I wanted to know why intuitionistic logic rejects the law of the excluded middle?
Thanks a lot.
For the first part :
(P ∨ ¬ P) ⊢ [((P→Q)→P)→P]
we can prove it using the following axiom system for (propositional) Intuitionistic logic and modus ponens.
Proof
1) P --- assumed
2) ((P→Q)→P)→P --- from axiom A → (B → A), with P in place of A and ((P→Q)→P) as B, and 1), by modus ponens
3) P → [((P→Q)→P)→P] --- from 1) and 2) by Deduction Theorem (or →-introduction in Natural Deduction), "discharging" assumption 1)
4) ¬P --- assumed
5) (P→Q) --- from axiom ¬A → (A → B) (ex falso quodlibet) and 4), by modus ponens
6) (P→Q)→P --- assumed
7) P --- from 5) and 6), by modus ponens
8) ((P→Q)→P)→P --- from 6) and 7), by Deduction Theorem, "discharging" assumption 6)
9) ¬P → [((P→Q)→P)→P] --- from 4) and 8) by Deduction Theorem, "discharging" assumption 4)
Now that we have derived : P → [((P→Q)→P)→P] (3) and ¬P → [((P→Q)→P)→P] (9), we use the axiom (A → C) → ((B → C) → (A ∨ B → C)) with P in place of A, ¬P in place of B and ((P→Q)→P)→P as C to derive, by modus ponens twice :
10) (P ∨ ¬ P) → [((P→Q)→P)→P].
For the other part, we can prove :
if ⊢ [((P→Q)→P)→P], then ⊢ (P ∨ ¬ P)
using two additonal laws, which are intuitionistically valid :
and :
Proof of : ¬¬(P ∨ ¬ P)
1) ¬(P ∨ ¬ P) --- assumed
2) (¬P ∧ ¬¬ P) --- from 1) by De Morgan (see above)
3) ¬P --- from 2) and axiom A & B → A, by *modus ponens
4) ¬¬ P --- from 3) and axiom A & B → B, by *modus ponens
5) ¬(P ∨ ¬ P) → ¬P --- from 1) and 3) by Deduction Theorem
6) ¬(P ∨ ¬ P) → ¬¬P --- from 1) and 4) by Deduction Theorem
7) ¬¬(P ∨ ¬ P) --- from 5) and 6) and axiom (A → B) → ((A → ¬B) → ¬A), by modus ponens twice.
Now for the main Proof, where we use the falsum ⊥ and define negation through the abbreviation : ¬P for P → ⊥.
1) (P ∨ ¬ P) → ⊥ --- assumed
2) ¬(P ∨ ¬ P) --- from 1) and the abbreviation above
3) ¬¬(P ∨ ¬ P) --- we have proved it above
4) (P ∨ ¬ P) --- from 3) and 2) and the axiom : ¬A → (A → B), by modus ponens twice
5) ((P ∨ ¬ P) → ⊥) → (P ∨ ¬ P) --- from 1) and 4) by Deduction Theorem
6) [((P ∨ ¬ P) → ⊥) → (P ∨ ¬ P)] → (P ∨ ¬ P) --- from Peirce's law : ((A→B)→A)→A with (P ∨ ¬ P) as A and ⊥ as B
7) (P ∨ ¬ P) --- from 5) and 6) by modus ponens.
Comment
We can summarize the situation as follows.
In classical logic we have : ⊢((P→Q)→P)→P and : ⊢ P ∨ ¬ P , because both are tautologies.
Also :
⊢ (P ∨ ¬ P) <-> [((P→Q)→P)→P]
is a valid logical law.
In intuitionistic logic we have that : ⊢ [((P→Q)→P)→P] iff ⊢ (P ∨ ¬ P), and also ⊢(P ∨ ¬ P) → [((P→Q)→P)→P].
But not ⊢ [((P→Q)→P)→P] → (P ∨ ¬ P).
You have two questions here, which don't really relate to each other. It may be worth asking two seperate ones. I'll answer the first here.
Pierces law states: ((p implies q) implies p) implies p
This is equivalent to the law of the excluded middle in propositional logic. One can prove this by using truth tables (a la Wittgenstein).
First observes the truth table for material implication:
- (T implies T) is T
- (T implies F) is F
- (F implies T) is T
- (F implies F) is T
- ((T implies T) implies T) implies T
- T
- ((T implies F) implies T) implies T
- (F implies T) implies T
- T implies T
- T
- ((F implies T) implies F) implies F
- (T implies F) implies F
- F implies T
- T
- ((F implies F) implies F) implies F
- (T implies F) implies F
- F implies T
- T
Since the expression always simplifies to true for any assignment of truth value to the propositions p and q; we must have that the entire expression is always true; that is it is a tautology.
An alternative proof could use the equivalence of (p implies q) with (not p or q) and use the de Morgan laws to simplify.
