LEM.v

From Coq Require Import Program.Basics.

Reserved Notation "¬ A" (at level 75, right associativity).

Notation "⊥" := Empty_set.
Notation "¬ A" := (A -> ⊥).

Axiom callcc : forall {A B : Type}, ((A -> B) -> A) -> A.

Definition LEM {P : Type} : P + ¬P :=
  callcc (fun f => inl (callcc (fun p => f (inr p)))).

From Coq Require Import ZArith Znumtheory.

Definition goldbach : Type :=
  forall n, n > 2 -> { ' (p, q) | prime p /\ prime q /\ p + q = n }.

Compute LEM : goldbach + ¬goldbach. (* I did it! *)