peirce_iff_excluded_middle

peirce_iff_excluded_middle.v

Require Import Classical_Prop.
Require Import ClassicalFacts.

(* https://math.stackexchange.com/questions/447098/why-peirces-law-implies-law-of-excluded-middle *)

Definition strengthen : 
  forall P : Prop,
  (P \/ ~P -> False) -> ~P
:= 
  fun P H p => 
  let e : ~P := fun p => H (or_introl p) in 
  H (or_intror e) 
.

Definition relax : 
  forall P : Prop,
  P -> P \/ ~P 
:= 
  fun P p => 
  or_introl p
.

Definition peirce 
  := forall P:Prop,  ((P -> False) -> P) -> P.

Definition excluded_middle_imply_peirce : 
  excluded_middle -> 
  peirce
:= 
  fun em P H => 
    let e1 := em P in 
    match e1 with 
    | or_introl l => l 
    | or_intror r =>  H r 
    end 
.

Theorem peirce_imply_excluded_middle  : 
  peirce -> 
  excluded_middle.
Proof.
  unfold excluded_middle.
  intros H P.
  apply H.
  intro.
  unfold not in H0.
  apply strengthen in H0.
  apply or_intror.
  exact H0.
Qed.


Definition peirce_iff_excluded_middle
  := conj peirce_imply_excluded_middle excluded_middle_imply_peirce.