Skip to content

Instantly share code, notes, and snippets.

@methylene
Last active December 11, 2015 05:28

Revisions

  1. methylene revised this gist Jan 17, 2013. 1 changed file with 3 additions and 2 deletions.
    5 changes: 3 additions & 2 deletions peirce_implies_lem.v
    Original file line number Diff line number Diff line change
    @@ -9,7 +9,8 @@ http://en.wikipedia.org/wiki/Peirce_law
    Definition peirce := forall (p q : Prop),
    ((p -> q) -> p) -> p.

    Definition lem := forall p, p\/ ~ p.
    Definition lem := forall p : Prop,
    p\/ ~ p.

    Theorem peirce_implies_lem: peirce -> lem.

    @@ -48,4 +49,4 @@ Proof.
    intro.
    intro.

    (* How to prove w1_implies_lem? *)
    (* How to finish proof of w1_implies_lem? *)
  2. methylene revised this gist Jan 17, 2013. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions peirce_implies_lem.v
    Original file line number Diff line number Diff line change
    @@ -41,11 +41,11 @@ Qed.
    (* How to prove w0_implies_w1 without 'firstorder magic'? *)


    Lemma lem_from_w1: w1 -> lem.
    Lemma w1_implies_lem: w1 -> lem.

    Proof.
    unfold w1, lem.
    intro.
    intro.

    (* How do I prove theorem? *)
    (* How to prove w1_implies_lem? *)
  3. methylene revised this gist Jan 16, 2013. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions peirce_implies_lem.v
    Original file line number Diff line number Diff line change
    @@ -31,14 +31,14 @@ Definition w1 := forall (p : Prop),
    (p \/ ~ p -> ~ (p \/ ~ p)) -> p \/ ~ p.


    Lemma w1_from_w0: w0 -> w1.
    Lemma w0_implies_w1: w0 -> w1.

    Proof.
    unfold w0, w1.
    firstorder.
    Qed.

    (* How to prove w1_from_w0 without 'firstorder magic'? *)
    (* How to prove w0_implies_w1 without 'firstorder magic'? *)


    Lemma lem_from_w1: w1 -> lem.
  4. methylene created this gist Jan 16, 2013.
    51 changes: 51 additions & 0 deletions peirce_implies_lem.v
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,51 @@
    (*
    https://www.youtube.com/watch?v=7sk8hPWAMSw
    http://en.wikipedia.org/wiki/Law_of_excluded_middle
    http://en.wikipedia.org/wiki/Peirce_law
    *)

    Definition peirce := forall (p q : Prop),
    ((p -> q) -> p) -> p.

    Definition lem := forall p, p\/ ~ p.

    Theorem peirce_implies_lem: peirce -> lem.

    Proof.
    unfold peirce, lem.
    intros.
    apply H with (q := ~ (p \/ ~ p)).
    firstorder.
    Qed.


    (* Not so fast please.
    Can we break the last two steps down a bit? *)

    Definition w0 := forall (p : Prop),
    ((p -> ~ (p \/ ~ p) ) -> p) -> p.

    Definition w1 := forall (p : Prop),
    (p \/ ~ p -> ~ (p \/ ~ p)) -> p \/ ~ p.


    Lemma w1_from_w0: w0 -> w1.

    Proof.
    unfold w0, w1.
    firstorder.
    Qed.

    (* How to prove w1_from_w0 without 'firstorder magic'? *)


    Lemma lem_from_w1: w1 -> lem.

    Proof.
    unfold w1, lem.
    intro.
    intro.

    (* How do I prove theorem? *)