6

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.

  • You can see the proof here – Mauro ALLEGRANZA Sep 13 '14 at 8:12
  • This is Peirce's original explanation : "That it is true appears as follows. It can only be false by the final consequent x being false while its antecedent (x−><y)−>x is true. If this is true, either its consequent x is true, when the whole formula would be true, or its antecedent x−>y is false. But in the last case the antecedent of x−>y, that is x, must be true." – Mauro ALLEGRANZA Sep 13 '14 at 8:14
  • For the rejection of LEM by intuitionists, see the ansewr to this post – Mauro ALLEGRANZA Sep 13 '14 at 8:52
  • Thus, being equivalent to LEM, Intuitionistic logic rejects also Peirce's law. – Mauro ALLEGRANZA Sep 13 '14 at 10:55
3

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 :

  • ⊢ ¬(P ∨ ¬ P) ↔ (¬P ∧ ¬¬ P) --- for the intuitionistically valid De Morgan's laws, see Intuitionistic logic

and :

  • ⊢ ¬¬(P ∨ ¬ P).

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

1

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:

  1. (T implies T) is T
  2. (T implies F) is F
  3. (F implies T) is T
  4. (F implies F) is T
  1. suppose p=T and q=T
  • ((T implies T) implies T) implies T
  • T
  1. suppose p=T and q=F
  • ((T implies F) implies T) implies T
  • (F implies T) implies T
  • T implies T
  • T
  1. suppose p=F and q=T
  • ((F implies T) implies F) implies F
  • (T implies F) implies F
  • F implies T
  • T
  1. suppose p=F and q=F
  • ((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.

  • But why is saying that it is a tautology make it equivalent to LEM? – DLV Sep 13 '14 at 15:37
  • 1
    @David - in classical logic every two tautologies are (trivially) equivalent (they are always eveluated to T by truth-table). The interesting issue is to prove their equivalence in intuitionistic logic, where the concept of tautology does not apply, and thus the truth-table algorithm doesn not work ... – Mauro ALLEGRANZA Sep 13 '14 at 17:19
  • @MauroALLEGRANZA: There is another interesting perspective on this which is that we've reduced LEM to a proposition involving only implication; hence we can examine a fragment of logic involving only implication. Does this lead anywhere - I don't know; but it bears examining; and probably has been. – Mozibur Ullah Sep 13 '14 at 18:41
  • @MauroALLEGRANZA: I didn't know that truth-tables failed in intuitionistic logic; why is that - and should I ask a separate question? – Mozibur Ullah Sep 13 '14 at 18:42
  • @MoziburUllah - what I mean is that truth-table "incorporate" classical semantics; in intuitionsitic logic not all tautologies are valid (see LEM). Thus, we cannot use them to prove an intuitionistically valid law. – Mauro ALLEGRANZA Sep 13 '14 at 18:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.