List of equivalents to Law of the Excluded Middle under intuitionistic logic

350 Views Asked by At

What are commonly-known equivalents of LEM among logicians, assuming intuitionistic axioms? I'll list a few to begin with. Below, $\varphi$ and $\psi$ denote arbitrary sentences.

  1. (DNE) Double negation elimination: $\neg \neg \varphi \vdash \varphi$
  2. (RAA) Reductio ad absurdum: $\neg \varphi \to \psi, \neg \varphi \to \neg \psi \vdash \varphi$
  3. (P) Peirce's Law: $\vdash ((\varphi \to \psi) \to \varphi) \to \varphi$

LEM → DNE

01. ¬¬φ        premise
02. φ∨¬φ       LEM
  03. ¬φ       assumption
  04. ⊥        contradiction 03 01
  05. φ        explosion 04
06. ¬φ→φ       →intro 03-05
  07. φ        assumption
08. φ→φ        →intro 07-07
09. φ          ∨elim 02 08 06

DNE → LEM

  01. ¬[φ∨¬φ]  assumption
    02. φ      assumption
    03. φ∨¬φ   ∨intro 02
    04. ⊥      contradiction 03 01
  05. ¬φ       ¬intro 02-04
  06. φ∨¬φ     ∨intro 05
  07. ⊥        contradiction 06 01
08. ¬¬[φ∨¬φ]   ¬intro 01-07
09. φ∨¬φ       DNE

LEM → RAA

01. ¬φ→ψ       premise
02. ¬φ→¬ψ      premise
03. φ∨¬φ       LEM
  04. ¬φ       assumption
  05. ψ        MP 01 04
  06. ¬ψ       MP 02 04
  07. ⊥        contradiction 05 06
  08. φ        explosion 07
09. ¬φ→φ       →intro 04-08
  10. φ        assumption
11. φ→φ        →intro 10-10
12. φ          ∨elim 03 11 09

RAA → LEM

  01. ¬[φ∨¬φ]   assumption
    02. φ       assumption
    03. φ∨¬φ    ∨intro 02
    04. ⊥       contradiction 03 01
  05. ¬φ        ¬intro 02-04
06. ¬[φ∨¬φ]→¬φ  →intro 01-05
  07. ¬[φ∨¬φ]   assumption
    08. ¬φ      assumption
    09. φ∨¬φ    ∨intro 02
    10. ⊥       contradiction 09 07
  11. ¬¬φ       ¬intro 08-10
12. ¬[φ∨¬φ]→¬¬φ →intro 07-11
13. φ∨¬φ        RAA 06 12

LEM → P

  01. [φ→ψ]→φ   assumption
    02. ¬φ      assumption
      03. φ     assumption
      04. ⊥     contradiction 03 02
      05. ψ     explosion 04
    06. φ→ψ     →intro 03-05
    07  φ       MP 01 06
  09. ¬φ→φ      →intro 02-07
    10. φ       assumption
  11. φ→φ       →intro 10-10
  12. φ∨¬φ      LEM
  13. φ         ∨elim 12 11 09
14. [[φ→ψ]→φ]→φ →intro 01-13

P → LEM

01. [[[φ∨¬φ]→⊥]→[φ∨¬φ]]→[φ∨¬φ] P
  02. [[φ∨¬φ]→⊥]               assumption
    03. [φ∨¬φ]                 assumption
    04. ⊥                      MP 02 03
  05. ¬[φ∨¬φ]                  ¬intro 03-04
    06. φ                      assumption
    07. φ∨¬φ                   ∨intro 06
    08. ⊥                      contradiction 07 05
  09. ¬φ                       ¬intro 06-8
  10. φ∨¬φ                     ∨intro 09
11. [[φ∨¬φ]→⊥]→[φ∨¬φ]          →intro 02-10
12. φ∨¬φ                       MP 01 11