Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Some facts and definitions about classical logic

Table of contents:

1. Propositional degeneracy = excluded-middle + propositional extensionality

2. Classical logic and proof-irrelevance

2.1. CC |- prop. ext. + A inhabited -> (A = A->A) -> A has fixpoint

2.2. CC |- prop. ext. + dep elim on bool -> proof-irrelevance

2.3. CIC |- prop. ext. -> proof-irrelevance

2.4. CC |- excluded-middle + dep elim on bool -> proof-irrelevance

2.5. CIC |- excluded-middle -> proof-irrelevance

3. Weak classical axioms

3.1. Weak excluded middle

3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction

3 3. Independence of general premises and drinker's paradox

4. Principles equivalent to classical logic

4.1 Classical logic = principle of unrestricted minimization

4.2 Classical logic = choice of representatives in a partition of bool

(************************************************************************)

Prop degeneracy = excluded-middle + prop extensionality

i.e. (∀ A, A=True ∨ A=False) ↔ (∀ A, A\/~A) ∧ (∀ A B, (A↔B) → A=B)

prop_degeneracy (also referred to as propositional completeness) asserts (up to consistency) that there are only two distinct formulas

Definition prop_degeneracy := forall A:Prop, A = True \/ A = False.

prop_extensionality asserts that equivalent formulas are equal

Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B.

excluded_middle asserts that we can reason by case on the truth or falsity of any formula

Definition excluded_middle := forall A:Prop, A \/ ~ A.

We show prop_degeneracy ↔ (prop_extensionality ∧ excluded_middle)

Lemma prop_degen_ext : prop_degeneracy -> prop_extensionality.prop_degeneracy -> prop_extensionality
Proof.prop_degeneracy -> prop_extensionality
  intros H A B [Hab Hba].H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
A = B
  destruct (H A); destruct (H B).H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = False
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
    rewrite H1; exact H0.H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = False
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
    absurd B.H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = False
~ B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = False
B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
      rewrite H1; exact (fun H => H).H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = True
H1:B = False
B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
      apply Hab; rewrite H0; exact I.H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A = B
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
    absurd A.H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
~ A
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
      rewrite H0; exact (fun H => H).H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = True
A
H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
      apply Hba; rewrite H1; exact I.H:prop_degeneracy
A, B:Prop
Hab:A -> B
Hba:B -> A
H0:A = False
H1:B = False
A = B
    rewrite H1; exact H0.
Qed.

Lemma prop_degen_em : prop_degeneracy -> excluded_middle.prop_degeneracy -> excluded_middle
Proof.prop_degeneracy -> excluded_middle
  intros H A.H:prop_degeneracy
A:Prop
A \/ ~ A
  destruct (H A).H:prop_degeneracy
A:Prop
H0:A = True
A \/ ~ A
H:prop_degeneracy
A:Prop
H0:A = False
A \/ ~ A
    left; rewrite H0; exact I.H:prop_degeneracy
A:Prop
H0:A = False
A \/ ~ A
    right; rewrite H0; exact (fun x => x).
Qed.

Lemma prop_ext_em_degen :
  prop_extensionality -> excluded_middle -> prop_degeneracy.prop_extensionality ->
excluded_middle -> prop_degeneracy
Proof.prop_extensionality ->
excluded_middle -> prop_degeneracy
  intros Ext EM A.Ext:prop_extensionality
EM:excluded_middle
A:Prop
A = True \/ A = False
  destruct (EM A).Ext:prop_extensionality
EM:excluded_middle
A:Prop
H:A
A = True \/ A = False
Ext:prop_extensionality
EM:excluded_middle
A:Prop
H:~ A
A = True \/ A = False
    left; apply (Ext A True); split;
     [ exact (fun _ => I) | exact (fun _ => H) ].Ext:prop_extensionality
EM:excluded_middle
A:Prop
H:~ A
A = True \/ A = False
    right; apply (Ext A False); split; [ exact H | apply False_ind ].
Qed.

A weakest form of propositional extensionality: extensionality for provable propositions only

Require Import PropExtensionalityFacts.

Definition provable_prop_extensionality := forall A:Prop, A -> A = True.

Lemma provable_prop_ext :
  prop_extensionality -> provable_prop_extensionality.prop_extensionality -> provable_prop_extensionality
Proof.prop_extensionality -> provable_prop_extensionality
  exact PropExt_imp_ProvPropExt.
Qed.

(************************************************************************)

Classical logic and proof-irrelevance

(************************************************************************)

CC |- prop ext + A inhabited -> (A = A->A) -> A has fixpoint

We successively show that:

prop_extensionality implies equality of A and A→A for inhabited A, which implies the existence of a (trivial) retract from A→A to A (just take the identity), which implies the existence of a fixpoint operator in A (e.g. take the Y combinator of lambda-calculus)

Notation inhabited A := A (only parsing).

Lemma prop_ext_A_eq_A_imp_A :
  prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.prop_extensionality ->
forall A : Prop, A -> (A -> A) = A
Proof.prop_extensionality ->
forall A : Prop, A -> (A -> A) = A
  intros Ext A a.Ext:prop_extensionality
A:Prop
a:A
(A -> A) = A
  apply (Ext (A -> A) A); split; [ exact (fun _ => a) | exact (fun _ _ => a) ].
Qed.

Record retract (A B:Prop) : Prop :=
  {f1 : A -> B; f2 : B -> A; f1_o_f2 : forall x:B, f1 (f2 x) = x}.

Lemma prop_ext_retract_A_A_imp_A :
  prop_extensionality -> forall A:Prop, inhabited A -> retract A (A -> A).prop_extensionality ->
forall A : Prop, A -> retract A (A -> A)
Proof.prop_extensionality ->
forall A : Prop, A -> retract A (A -> A)
  intros Ext A a.Ext:prop_extensionality
A:Prop
a:A
retract A (A -> A)
  rewrite (prop_ext_A_eq_A_imp_A Ext A a).Ext:prop_extensionality
A:Prop
a:A
retract A A
  exists (fun x:A => x) (fun x:A => x).Ext:prop_extensionality
A:Prop
a:A
forall x : A, x = x
  reflexivity.
Qed.

Record has_fixpoint (A:Prop) : Prop :=
  {F : (A -> A) -> A; Fix : forall f:A -> A, F f = f (F f)}.

Lemma ext_prop_fixpoint :
  prop_extensionality -> forall A:Prop, inhabited A -> has_fixpoint A.prop_extensionality ->
forall A : Prop, A -> has_fixpoint A
Proof.prop_extensionality ->
forall A : Prop, A -> has_fixpoint A
  intros Ext A a.Ext:prop_extensionality
A:Prop
a:A
has_fixpoint A
  case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2.Ext:prop_extensionality
A:Prop
a:A
g1:A -> A -> A
g2:(A -> A) -> A
g1_o_g2:forall x : A -> A, g1 (g2 x) = x
has_fixpoint A
  exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))).Ext:prop_extensionality
A:Prop
a:A
g1:A -> A -> A
g2:(A -> A) -> A
g1_o_g2:forall x : A -> A, g1 (g2 x) = x
forall f : A -> A,
f
  (g1 (g2 (fun x : A => f (g1 x x)))
     (g2 (fun x : A => f (g1 x x)))) =
f
  (f
     (g1 (g2 (fun x : A => f (g1 x x)))
        (g2 (fun x : A => f (g1 x x)))))
  intro f.Ext:prop_extensionality
A:Prop
a:A
g1:A -> A -> A
g2:(A -> A) -> A
g1_o_g2:forall x : A -> A, g1 (g2 x) = x
f:A -> A
f
  (g1 (g2 (fun x : A => f (g1 x x)))
     (g2 (fun x : A => f (g1 x x)))) =
f
  (f
     (g1 (g2 (fun x : A => f (g1 x x)))
        (g2 (fun x : A => f (g1 x x)))))
  pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1.Ext:prop_extensionality
A:Prop
a:A
g1:A -> A -> A
g2:(A -> A) -> A
g1_o_g2:forall x : A -> A, g1 (g2 x) = x
f:A -> A
(fun a0 : A -> A =>
 f (a0 (g2 (fun x : A => f (g1 x x)))) =
 f
   (f
      (g1 (g2 (fun x : A => f (g1 x x)))
         (g2 (fun x : A => f (g1 x x))))))
  (g1 (g2 (fun x : A => f (g1 x x))))
  rewrite (g1_o_g2 (fun x:A => f (g1 x x))).Ext:prop_extensionality
A:Prop
a:A
g1:A -> A -> A
g2:(A -> A) -> A
g1_o_g2:forall x : A -> A, g1 (g2 x) = x
f:A -> A
f
  (f
     (g1 (g2 (fun x : A => f (g1 x x)))
        (g2 (fun x : A => f (g1 x x))))) =
f
  (f
     (g1 (g2 (fun x : A => f (g1 x x)))
        (g2 (fun x : A => f (g1 x x)))))
  reflexivity.
Qed.

Remark: prop_extensionality can be replaced in lemma ext_prop_fixpoint by the weakest property provable_prop_extensionality.

(************************************************************************)

CC |- prop_ext /\ dep elim on bool -> proof-irrelevance

proof_irrelevance asserts equality of all proofs of a given formula

Definition proof_irrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.

Assume that we have booleans with the property that there is at most 2 booleans (which is equivalent to dependent case analysis). Consider the fixpoint of the negation function: it is either true or false by dependent case analysis, but also the opposite by fixpoint. Hence proof-irrelevance.

We then map equality of boolean proofs to proof irrelevance in all propositions.

Section Proof_irrelevance_gen.

  Variable bool : Prop.
  Variable true : bool.
  Variable false : bool.
  Hypothesis bool_elim : forall C:Prop, C -> C -> bool -> C.
  Hypothesis
    bool_elim_redl : forall (C:Prop) (c1 c2:C), c1 = bool_elim C c1 c2 true.
  Hypothesis
    bool_elim_redr : forall (C:Prop) (c1 c2:C), c2 = bool_elim C c1 c2 false.
  Let bool_dep_induction :=
  forall P:bool -> Prop, P true -> P false -> forall b:bool, P b.

  Lemma aux : prop_extensionality -> bool_dep_induction -> true = false.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
prop_extensionality ->
bool_dep_induction -> true = false
  Proof.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
prop_extensionality ->
bool_dep_induction -> true = false
    intros Ext Ind.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
true = false
    case (ext_prop_fixpoint Ext bool true); intros G Gfix.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
true = false
    set (neg := fun b:bool => bool_elim bool false true b).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
true = false
    generalize (eq_refl (G neg)).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
G neg = G neg -> true = false
    pattern (G neg) at 1.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
(fun b : bool => b = G neg -> true = false) (G neg)
    apply Ind with (b := G neg); intro Heq.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:true = G neg
true = false
bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:false = G neg
true = false
    rewrite (bool_elim_redl bool false true).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:true = G neg
true = bool_elim bool false true true
bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:false = G neg
true = false
    change (true = neg true); rewrite Heq; apply Gfix.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:false = G neg
true = false
    rewrite (bool_elim_redr bool false true).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
G:(bool -> bool) -> bool
Gfix:forall f : bool -> bool, G f = f (G f)
neg:=fun b : bool => bool_elim bool false true b:bool -> bool
Heq:false = G neg
bool_elim bool false true false = false
    change (neg false = false); rewrite Heq; symmetry ;
      apply Gfix.
  Qed.

  Lemma ext_prop_dep_proof_irrel_gen :
    prop_extensionality -> bool_dep_induction -> proof_irrelevance.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
prop_extensionality ->
bool_dep_induction -> proof_irrelevance
  Proof.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
prop_extensionality ->
bool_dep_induction -> proof_irrelevance
    intros Ext Ind A a1 a2.bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
a1 = a2
    set (f := fun b:bool => bool_elim A a1 a2 b).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
a1 = a2
    rewrite (bool_elim_redl A a1 a2).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
bool_elim A a1 a2 true = a2
    change (f true = a2).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
f true = a2
    rewrite (bool_elim_redr A a1 a2).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
f true = bool_elim A a1 a2 false
    change (f true = f false).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
f true = f false
    rewrite (aux Ext Ind).bool:Prop
true, false:bool
bool_elim:forall C : Prop, C -> C -> bool -> C
bool_elim_redl:forall (C : Prop) (c1 c2 : C),
c1 = bool_elim C c1 c2 true
bool_elim_redr:forall (C : Prop) (c1 c2 : C),
c2 = bool_elim C c1 c2 false
bool_dep_induction:=forall P : bool -> Prop,
P true ->
P false -> forall b : bool, P b:Prop
Ext:prop_extensionality
Ind:bool_dep_induction
A:Prop
a1, a2:A
f:=fun b : bool => bool_elim A a1 a2 b:bool -> A
f false = f false
    reflexivity.
  Qed.

End Proof_irrelevance_gen.

In the pure Calculus of Constructions, we can define the boolean proposition bool = (C:Prop)C->C->C but we cannot prove that it has at most 2 elements.

Section Proof_irrelevance_Prop_Ext_CC.

  Definition BoolP := forall C:Prop, C -> C -> C.
  Definition TrueP : BoolP := fun C c1 c2 => c1.
  Definition FalseP : BoolP := fun C c1 c2 => c2.
  Definition BoolP_elim C c1 c2 (b:BoolP) := b C c1 c2.
  Definition BoolP_elim_redl (C:Prop) (c1 c2:C) :
    c1 = BoolP_elim C c1 c2 TrueP := eq_refl c1.
  Definition BoolP_elim_redr (C:Prop) (c1 c2:C) :
    c2 = BoolP_elim C c1 c2 FalseP := eq_refl c2.

  Definition BoolP_dep_induction :=
    forall P:BoolP -> Prop, P TrueP -> P FalseP -> forall b:BoolP, P b.

  Lemma ext_prop_dep_proof_irrel_cc :
    prop_extensionality -> BoolP_dep_induction -> proof_irrelevance.prop_extensionality ->
BoolP_dep_induction -> proof_irrelevance
  Proof.prop_extensionality ->
BoolP_dep_induction -> proof_irrelevance
    exact (ext_prop_dep_proof_irrel_gen BoolP TrueP FalseP BoolP_elim BoolP_elim_redl
      BoolP_elim_redr).
  Qed.

End Proof_irrelevance_Prop_Ext_CC.

Remark: prop_extensionality can be replaced in lemma ext_prop_dep_proof_irrel_gen by the weakest property provable_prop_extensionality.

(************************************************************************)

CIC |- prop. ext. -> proof-irrelevance

In the Calculus of Inductive Constructions, inductively defined booleans enjoy dependent case analysis, hence directly proof-irrelevance from propositional extensionality.

Section Proof_irrelevance_CIC.

  Inductive boolP : Prop :=
    | trueP : boolP
    | falseP : boolP.
  Definition boolP_elim_redl (C:Prop) (c1 c2:C) :
    c1 = boolP_ind C c1 c2 trueP := eq_refl c1.
  Definition boolP_elim_redr (C:Prop) (c1 c2:C) :
    c2 = boolP_ind C c1 c2 falseP := eq_refl c2.
  Scheme boolP_indd := Induction for boolP Sort Prop.

  Lemma ext_prop_dep_proof_irrel_cic : prop_extensionality -> proof_irrelevance.prop_extensionality -> proof_irrelevance
  Proof.prop_extensionality -> proof_irrelevance
    exact (fun pe =>
      ext_prop_dep_proof_irrel_gen boolP trueP falseP boolP_ind boolP_elim_redl
      boolP_elim_redr pe boolP_indd).
  Qed.

End Proof_irrelevance_CIC.

Can we state proof irrelevance from propositional degeneracy (i.e. propositional extensionality + excluded middle) without dependent case analysis ?

Berardi [Berardi90] built a model of CC interpreting inhabited types by the set of all untyped lambda-terms. This model satisfies propositional degeneracy without satisfying proof-irrelevance (nor dependent case analysis). This implies that the previous results cannot be refined.

[Berardi90] Stefano Berardi, "Type dependence and constructive mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990.

(************************************************************************)

CC |- excluded-middle + dep elim on bool -> proof-irrelevance

This is a proof in the pure Calculus of Construction that classical logic in Prop + dependent elimination of disjunction entails proof-irrelevance.

Reference:

[Coquand90] T. Coquand, "Metamathematical Investigations of a Calculus of Constructions", Proceedings of Logic in Computer Science (LICS'90), 1990.

Proof skeleton: classical logic + dependent elimination of disjunction + discrimination of proofs implies the existence of a retract from Prop into bool, hence inconsistency by encoding any paradox of system U- (e.g. Hurkens' paradox).

Require Import Hurkens.

Section Proof_irrelevance_EM_CC.

  Variable or : Prop -> Prop -> Prop.
  Variable or_introl : forall A B:Prop, A -> or A B.
  Variable or_intror : forall A B:Prop, B -> or A B.
  Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
  Hypothesis
    or_elim_redl :
    forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
      f a = or_elim A B C f g (or_introl A B a).
  Hypothesis
    or_elim_redr :
    forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
      g b = or_elim A B C f g (or_intror A B b).
  Hypothesis
    or_dep_elim :
    forall (A B:Prop) (P:or A B -> Prop),
      (forall a:A, P (or_introl A B a)) ->
      (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.

  Hypothesis em : forall A:Prop, or A (~ A).
  Variable B : Prop.
  Variables b1 b2 : B.

p2b and b2p form a retract if ¬b1=b2

  Let p2b A := or_elim A (~ A) B (fun _ => b1) (fun _ => b2) (em A).
  Let b2p b := b1 = b.

  Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
forall A : Prop, A -> b2p (p2b A)
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
forall A : Prop, A -> b2p (p2b A)
    unfold p2b; intro A; apply or_dep_elim with (b := em A);
      unfold b2p; intros.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a0 : A0),
f a0 =
or_elim A0 B0 C f g
  (or_introl A0 B0 a0)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a0 : A0, P (or_introl A0 B0 a0)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
A:Prop
a, H:A
b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) (or_introl A (~ A) a)
or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
A:Prop
b:~ A
H:A
b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (or_intror A (~ A) b)
    apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
A:Prop
b:~ A
H:A
b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) (or_intror A (~ A) b)
    destruct (b H).
  Qed.

  Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
b1 <> b2 -> forall A : Prop, b2p (p2b A) -> A
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
b1 <> b2 -> forall A : Prop, b2p (p2b A) -> A
    intro not_eq_b1_b2.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
not_eq_b1_b2:b1 <> b2
forall A : Prop, b2p (p2b A) -> A
    unfold p2b; intro A; apply or_dep_elim with (b := em A);
      unfold b2p; intros.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a0 : A0),
f a0 =
or_elim A0 B0 C f g
  (or_introl A0 B0 a0)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a0 : A0, P (or_introl A0 B0 a0)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
not_eq_b1_b2:b1 <> b2
A:Prop
a:A
H:b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (or_introl A (~ A) a)
A
or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
not_eq_b1_b2:b1 <> b2
A:Prop
b:~ A
H:b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (or_intror A (~ A) b)
A
    assumption.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
not_eq_b1_b2:b1 <> b2
A:Prop
b:~ A
H:b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (or_intror A (~ A) b)
A
    destruct not_eq_b1_b2.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
A:Prop
b:~ A
H:b1 =
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (or_intror A (~ A) b)
b1 = b2
    rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b0 : B0),
g b0 =
or_elim A0 B0 C f g
  (or_intror A0 B0 b0)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b0 : B0, P (or_intror A0 B0 b0)) ->
forall b0 : or A0 B0, P b0
em:forall A0 : Prop, or A0 (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : Prop =>
or_elim A0 (~ A0) B (fun _ : A0 => b1)
  (fun _ : ~ A0 => b2) 
  (em A0):Prop -> B
b2p:=fun b0 : B => b1 = b0:B -> Prop
A:Prop
b:~ A
H:b1 = b2
b1 = b2
    assumption.
  Qed.

Using excluded-middle a second time, we get proof-irrelevance

  Theorem proof_irrelevance_cc : b1 = b2.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
b1 = b2
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
b1 = b2
    refine (or_elim _ _ _ _ _ (em (b1 = b2))); intro H.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
H:b1 = b2
b1 = b2
or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
H:b1 <> b2
b1 = b2
    trivial.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
em:forall A : Prop, or A (~ A)
B:Prop
b1, b2:B
p2b:=fun A : Prop =>
or_elim A (~ A) B (fun _ : A => b1)
  (fun _ : ~ A => b2) 
  (em A):Prop -> B
b2p:=fun b : B => b1 = b:B -> Prop
H:b1 <> b2
b1 = b2
    apply (NoRetractFromSmallPropositionToProp.paradox B p2b b2p (p2p2 H) p2p1).
  Qed.

End Proof_irrelevance_EM_CC.

Hurkens' paradox still holds with a retract from the negative fragment of Prop into bool, hence weak classical logic, i.e. ∀ A, ¬A\/~~A, is enough for deriving a weak version of proof-irrelevance. This is enough to derive a contradiction from a Set-bound weak excluded middle with an impredicative Set universe.

Section Proof_irrelevance_WEM_CC.

  Variable or : Prop -> Prop -> Prop.
  Variable or_introl : forall A B:Prop, A -> or A B.
  Variable or_intror : forall A B:Prop, B -> or A B.
  Hypothesis or_elim : forall A B C:Prop, (A -> C) -> (B -> C) -> or A B -> C.
  Hypothesis
    or_elim_redl :
    forall (A B C:Prop) (f:A -> C) (g:B -> C) (a:A),
      f a = or_elim A B C f g (or_introl A B a).
  Hypothesis
    or_elim_redr :
    forall (A B C:Prop) (f:A -> C) (g:B -> C) (b:B),
      g b = or_elim A B C f g (or_intror A B b).
  Hypothesis
    or_dep_elim :
    forall (A B:Prop) (P:or A B -> Prop),
      (forall a:A, P (or_introl A B a)) ->
      (forall b:B, P (or_intror A B b)) -> forall b:or A B, P b.

  Hypothesis wem : forall A:Prop, or (~~A) (~ A).

  Notation NProp := NoRetractToNegativeProp.NProp.
  Notation El := NoRetractToNegativeProp.El.
  
  Variable B : Prop.
  Variables b1 b2 : B.

p2b and b2p form a retract if ¬b1=b2

  Let p2b (A:NProp) := or_elim (~~El A) (~El A) B (fun _ => b1) (fun _ => b2) (wem (El A)).
  Let b2p b : NProp := exist (fun P=>~~P -> P) (~~(b1 = b)) (fun h x => h (fun k => k x)).

  Lemma wp2p1 : forall A:NProp, El A -> El (b2p (p2b A)).or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
forall A : NProp, El A -> El (b2p (p2b A))
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
forall A : NProp, El A -> El (b2p (p2b A))
    intros A.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
El A -> El (b2p (p2b A)) unfold p2b.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
El A ->
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2) (wem (El A))))
    apply or_dep_elim with  (b := wem (El A)).or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
forall a : ~ ~ El A,
El A ->
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_introl (~ ~ El A) (~ El A) a)))
or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
forall b : ~ El A,
El A ->
El
  (b2p
     (or_elim (~ ~ El A) 
        (~ El A) B (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) b)))
    +or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
forall a : ~ ~ El A,
El A ->
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_introl (~ ~ El A) (~ El A) a))) intros nna a.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a0 : A0),
f a0 =
or_elim A0 B0 C f g
  (or_introl A0 B0 a0)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a0 : A0, P (or_introl A0 B0 a0)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
nna:~ ~ El A
a:El A
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_introl (~ ~ El A) (~ El A) nna)))
      rewrite <- or_elim_redl.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a0 : A0),
f a0 =
or_elim A0 B0 C f g
  (or_introl A0 B0 a0)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a0 : A0, P (or_introl A0 B0 a0)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
nna:~ ~ El A
a:El A
El (b2p b1)
      cbn.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a0 : A0),
f a0 =
or_elim A0 B0 C f g
  (or_introl A0 B0 a0)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a0 : A0, P (or_introl A0 B0 a0)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
nna:~ ~ El A
a:El A
~ b1 <> b1 auto.
    +or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
A:NProp
forall b : ~ El A,
El A ->
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) b))) intros n x.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x0 : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x0)):B -> NProp
A:NProp
n:~ El A
x:El A
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) n)))
      destruct (n x).
  Qed.

  Lemma wp2p2 : b1 <> b2 -> forall A:NProp, El (b2p (p2b A)) -> El A.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
b1 <> b2 -> forall A : NProp, El (b2p (p2b A)) -> El A
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
b1 <> b2 -> forall A : NProp, El (b2p (p2b A)) -> El A
    intro not_eq_b1_b2.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
forall A : NProp, El (b2p (p2b A)) -> El A
    intros A.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
El (b2p (p2b A)) -> El A unfold p2b.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2) (wem (El A)))) -> El A
    apply or_dep_elim with  (b := wem (El A)).or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
forall a : ~ ~ El A,
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_introl (~ ~ El A) (~ El A) a))) -> El A
or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
forall b : ~ El A,
El
  (b2p
     (or_elim (~ ~ El A) 
        (~ El A) B (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) b))) -> 
El A
    +or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
forall a : ~ ~ El A,
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_introl (~ ~ El A) (~ El A) a))) -> El A cbn.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
forall a : ~ ~ El A,
~
b1 <>
or_elim (~ ~ El A) (~ El A) B (fun _ : ~ ~ El A => b1)
  (fun _ : ~ El A => b2)
  (or_introl (~ ~ El A) (~ El A) a) -> El A
      intros x _.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x0 : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x0)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
x:~ ~ El A
El A
      destruct A.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x1 : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x1)):B -> NProp
not_eq_b1_b2:b1 <> b2
x0:Prop
p:~ ~ x0 -> x0
x:~ ~ El (exist (fun P : Prop => ~ ~ P -> P) x0 p)
El (exist (fun P : Prop => ~ ~ P -> P) x0 p) cbn in x |- *.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x1 : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x1)):B -> NProp
not_eq_b1_b2:b1 <> b2
x0:Prop
p:~ ~ x0 -> x0
x:~ ~ x0
x0
      auto.
    +or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
forall b : ~ El A,
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) b))) -> El A intros na.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
na:~ El A
El
  (b2p
     (or_elim (~ ~ El A) (~ El A) B
        (fun _ : ~ ~ El A => b1)
        (fun _ : ~ El A => b2)
        (or_intror (~ ~ El A) (~ El A) na))) -> El A
      rewrite <- or_elim_redr.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
na:~ El A
El (b2p b2) -> El A cbn.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
na:~ El A
~ b1 <> b2 -> El A
      intros h.or:Prop -> Prop -> Prop
or_introl:forall A0 B0 : Prop, A0 -> or A0 B0
or_intror:forall A0 B0 : Prop, B0 -> or A0 B0
or_elim:forall A0 B0 C : Prop,
(A0 -> C) -> (B0 -> C) -> or A0 B0 -> C
or_elim_redl:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (a : A0),
f a =
or_elim A0 B0 C f g (or_introl A0 B0 a)
or_elim_redr:forall (A0 B0 C : Prop) 
  (f : A0 -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A0 B0 C f g (or_intror A0 B0 b)
or_dep_elim:forall (A0 B0 : Prop)
  (P : or A0 B0 -> Prop),
(forall a : A0, P (or_introl A0 B0 a)) ->
(forall b : B0, P (or_intror A0 B0 b)) ->
forall b : or A0 B0, P b
wem:forall A0 : Prop, or (~ ~ A0) (~ A0)
B:Prop
b1, b2:B
p2b:=fun A0 : NProp =>
or_elim (~ ~ El A0) (~ El A0) B
  (fun _ : ~ ~ El A0 => b1)
  (fun _ : ~ El A0 => b2) 
  (wem (El A0)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
not_eq_b1_b2:b1 <> b2
A:NProp
na:~ El A
h:~ b1 <> b2
El A destruct (h not_eq_b1_b2).
  Qed.

By Hurkens's paradox, we get a weak form of proof irrelevance.

  Theorem wproof_irrelevance_cc : ~~(b1 = b2).or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
~ b1 <> b2
  Proof.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h (fun k : ~ b1 <> b => k x)):B -> NProp
~ b1 <> b2
    intros h.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
False
    unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)).or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
~ ~ B -> B
or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B ?Goal:{P : Prop | ~ ~ P -> P}
False
    {or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
~ ~ B -> B exact (fun _ => b1). }or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
False
    pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox.or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
paradox:forall B0 : NProp, El B0
False
    unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)).or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
paradox:forall B0 : NProp, El B0
~ ~ False -> False
or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
paradox:forall B0 : NProp, El B0
F:=exist (fun P : Prop => ~ ~ P -> P) False ?Goal:{P : Prop | ~ ~ P -> P}
False
    {or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
paradox:forall B0 : NProp, El B0
~ ~ False -> False auto. }or:Prop -> Prop -> Prop
or_introl:forall A B0 : Prop, A -> or A B0
or_intror:forall A B0 : Prop, B0 -> or A B0
or_elim:forall A B0 C : Prop,
(A -> C) -> (B0 -> C) -> or A B0 -> C
or_elim_redl:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (a : A),
f a =
or_elim A B0 C f g (or_introl A B0 a)
or_elim_redr:forall (A B0 C : Prop) 
  (f : A -> C) (g : B0 -> C) 
  (b : B0),
g b =
or_elim A B0 C f g (or_intror A B0 b)
or_dep_elim:forall (A B0 : Prop)
  (P : or A B0 -> Prop),
(forall a : A, P (or_introl A B0 a)) ->
(forall b : B0, P (or_intror A B0 b)) ->
forall b : or A B0, P b
wem:forall A : Prop, or (~ ~ A) (~ A)
B:Prop
b1, b2:B
p2b:=fun A : NProp =>
or_elim (~ ~ El A) (~ El A) B
  (fun _ : ~ ~ El A => b1) 
  (fun _ : ~ El A => b2) 
  (wem (El A)):NProp -> B
b2p:=fun b : B =>
exist (fun P : Prop => ~ ~ P -> P) 
  (~ b1 <> b)
  (fun (h0 : ~ ~ ~ b1 <> b) (x : b1 <> b) =>
   h0 (fun k : ~ b1 <> b => k x)):B -> NProp
h:b1 <> b2
NB:=exist (fun P : Prop => ~ ~ P -> P) B
  (fun _ : ~ ~ B => b1):{P : Prop | ~ ~ P -> P}
paradox:forall B0 : NProp, El B0
F:=exist (fun P : Prop => ~ ~ P -> P) False
  (fun H : ~ ~ False => H (fun H0 : False => H0)):{P : Prop | ~ ~ P -> P}
False
    exact (paradox F).
  Qed.

End Proof_irrelevance_WEM_CC.

(************************************************************************)

CIC |- excluded-middle -> proof-irrelevance

Since, dependent elimination is derivable in the Calculus of Inductive Constructions (CCI), we get proof-irrelevance from classical logic in the CCI.

Section Proof_irrelevance_CCI.

  Hypothesis em : forall A:Prop, A \/ ~ A.

  Definition or_elim_redl (A B C:Prop) (f:A -> C) (g:B -> C)
    (a:A) : f a = or_ind f g (or_introl B a) := eq_refl (f a).
  Definition or_elim_redr (A B C:Prop) (f:A -> C) (g:B -> C)
    (b:B) : g b = or_ind f g (or_intror A b) := eq_refl (g b).
  Scheme or_indd := Induction for or Sort Prop.

  Theorem proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), b1 = b2.em:forall A : Prop, A \/ ~ A
forall (B : Prop) (b1 b2 : B), b1 = b2
  Proof.em:forall A : Prop, A \/ ~ A
forall (B : Prop) (b1 b2 : B), b1 = b2
    exact (proof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
      or_elim_redr or_indd em).
  Qed.

End Proof_irrelevance_CCI.

The same holds with weak excluded middle. The proof is a little more involved, however.

Section Weak_proof_irrelevance_CCI.

  Hypothesis wem : forall A:Prop, ~~A \/ ~ A.

  Theorem wem_proof_irrelevance_cci : forall (B:Prop) (b1 b2:B), ~~b1 = b2.wem:forall A : Prop, ~ ~ A \/ ~ A
forall (B : Prop) (b1 b2 : B), ~ b1 <> b2
  Proof.wem:forall A : Prop, ~ ~ A \/ ~ A
forall (B : Prop) (b1 b2 : B), ~ b1 <> b2
    exact (wproof_irrelevance_cc or or_introl or_intror or_ind or_elim_redl
      or_elim_redr or_indd wem).
  Qed.

End Weak_proof_irrelevance_CCI.

Remark: in the Set-impredicative CCI, Hurkens' paradox still holds with bool in Set and since ¬true=false for true and false in bool from Set, we get the inconsistency of em : ∀ A:Prop, {A}+{~A} in the Set-impredicative CCI.

Weak classical axioms

We show the following increasing in the strength of axioms:

weak excluded-middle
right distributivity of implication over disjunction and Gödel-Dummett axiom
independence of general premises and drinker's paradox
excluded-middle

Weak excluded-middle

The weak classical logic based on ~~A ∨ ¬A is referred to with name KC in [ChagrovZakharyaschev97]

[ChagrovZakharyaschev97] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997.

Definition weak_excluded_middle :=
  forall A:Prop, ~~A \/ ~A.

The interest in the equivalent variant weak_generalized_excluded_middle is that it holds even in logic without a primitive False connective (like Gödel-Dummett axiom)

Definition weak_generalized_excluded_middle :=
  forall A B:Prop, ((A -> B) -> B) \/ (A -> B).

Gödel-Dummett axiom

(A→B) ∨ (B→A) is studied in [Dummett59] and is based on [Gödel33].

[Dummett59] Michael A. E. Dummett. "A Propositional Calculus with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol 24 No. 2(1959), pp 97-103.

[Gödel33] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38.

Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).

Lemma excluded_middle_Godel_Dummett : excluded_middle -> GodelDummett.excluded_middle -> GodelDummett
Proof.excluded_middle -> GodelDummett
  intros EM A B.EM:excluded_middle
A, B:Prop
(A -> B) \/ (B -> A) destruct (EM B) as [HB|HnotB].EM:excluded_middle
A, B:Prop
HB:B
(A -> B) \/ (B -> A)
EM:excluded_middle
A, B:Prop
HnotB:~ B
(A -> B) \/ (B -> A)
  left; intros _; exact HB.EM:excluded_middle
A, B:Prop
HnotB:~ B
(A -> B) \/ (B -> A)
  right; intros HB; destruct (HnotB HB).
Qed.

(A→B) ∨ (B→A) is equivalent to (C → A∨B) → (C→A) ∨ (C→B) (proof from [Dummett59])

Definition RightDistributivityImplicationOverDisjunction :=
  forall A B C:Prop, (C -> A\/B) -> (C->A) \/ (C->B).

Lemma Godel_Dummett_iff_right_distr_implication_over_disjunction :
  GodelDummett <-> RightDistributivityImplicationOverDisjunction.GodelDummett <->
RightDistributivityImplicationOverDisjunction
Proof.GodelDummett <->
RightDistributivityImplicationOverDisjunction
  split.GodelDummett ->
RightDistributivityImplicationOverDisjunction
RightDistributivityImplicationOverDisjunction ->
GodelDummett
    intros GD A B C HCAB.GD:GodelDummett
A, B, C:Prop
HCAB:C -> A \/ B
(C -> A) \/ (C -> B)
RightDistributivityImplicationOverDisjunction ->
GodelDummett
    destruct (GD B A) as [HBA|HAB]; [left|right]; intro HC;
      destruct (HCAB HC) as [HA|HB]; [ | apply HBA | apply HAB | ]; assumption.RightDistributivityImplicationOverDisjunction ->
GodelDummett
    intros Distr A B.Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
(A -> B) \/ (B -> A)
    destruct (Distr A B (A\/B)) as [HABA|HABB].Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
A \/ B -> A \/ B
Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
HABA:A \/ B -> A
(A -> B) \/ (B -> A)
Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
HABB:A \/ B -> B
(A -> B) \/ (B -> A)
      intro HAB; exact HAB.Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
HABA:A \/ B -> A
(A -> B) \/ (B -> A)
Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
HABB:A \/ B -> B
(A -> B) \/ (B -> A)
      right; intro HB; apply HABA; right; assumption.Distr:RightDistributivityImplicationOverDisjunction
A, B:Prop
HABB:A \/ B -> B
(A -> B) \/ (B -> A)
      left; intro HA; apply HABB; left; assumption.
Qed.

(A→B) ∨ (B→A) is stronger than the weak excluded middle

Lemma Godel_Dummett_weak_excluded_middle :
  GodelDummett -> weak_excluded_middle.GodelDummett -> weak_excluded_middle
Proof.GodelDummett -> weak_excluded_middle
  intros GD A.GD:GodelDummett
A:Prop
~ ~ A \/ ~ A destruct (GD (~A) A) as [HnotAA|HAnotA].GD:GodelDummett
A:Prop
HnotAA:~ A -> A
~ ~ A \/ ~ A
GD:GodelDummett
A:Prop
HAnotA:A -> ~ A
~ ~ A \/ ~ A
    left; intro HnotA; apply (HnotA (HnotAA HnotA)).GD:GodelDummett
A:Prop
HAnotA:A -> ~ A
~ ~ A \/ ~ A
    right; intro HA; apply (HAnotA HA HA).
Qed.

Independence of general premises and drinker's paradox

Independence of general premises is the unconstrained, non constructive, version of the Independence of Premises as considered in [Troelstra73].

It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle [KreiselPutnam57].

[KreiselPutnam57], Georg Kreisel and Hilary Putnam. "Eine Unableitsbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957.

[Troelstra73], Anne Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.

Definition IndependenceOfGeneralPremises :=
  forall (A:Type) (P:A -> Prop) (Q:Prop),
    inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.

Lemma
  independence_general_premises_right_distr_implication_over_disjunction :
  IndependenceOfGeneralPremises -> RightDistributivityImplicationOverDisjunction.IndependenceOfGeneralPremises ->
RightDistributivityImplicationOverDisjunction
Proof.IndependenceOfGeneralPremises ->
RightDistributivityImplicationOverDisjunction
  intros IP A B C HCAB.IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
(C -> A) \/ (C -> B)
  destruct (IP bool (fun b => if b then A else B) C true) as ([|],H).IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
C -> exists x : bool, if x then A else B
IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
H:C -> A
(C -> A) \/ (C -> B)
IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
H:C -> B
(C -> A) \/ (C -> B)
    intro HC; destruct (HCAB HC); [exists true|exists false]; assumption.IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
H:C -> A
(C -> A) \/ (C -> B)
IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
H:C -> B
(C -> A) \/ (C -> B)
    left; assumption.IP:IndependenceOfGeneralPremises
A, B, C:Prop
HCAB:C -> A \/ B
H:C -> B
(C -> A) \/ (C -> B)
    right; assumption.
Qed.

Lemma independence_general_premises_Godel_Dummett :
  IndependenceOfGeneralPremises -> GodelDummett.IndependenceOfGeneralPremises -> GodelDummett
Proof.IndependenceOfGeneralPremises -> GodelDummett
  destruct Godel_Dummett_iff_right_distr_implication_over_disjunction.H:GodelDummett ->
RightDistributivityImplicationOverDisjunction
H0:RightDistributivityImplicationOverDisjunction ->
GodelDummett
IndependenceOfGeneralPremises -> GodelDummett
  auto using independence_general_premises_right_distr_implication_over_disjunction.
Qed.

Independence of general premises is equivalent to the drinker's paradox

Definition DrinkerParadox :=
  forall (A:Type) (P:A -> Prop),
    inhabited A -> exists x, (exists x, P x) -> P x.

Lemma independence_general_premises_drinker :
  IndependenceOfGeneralPremises <-> DrinkerParadox.IndependenceOfGeneralPremises <-> DrinkerParadox
Proof.IndependenceOfGeneralPremises <-> DrinkerParadox
  split.IndependenceOfGeneralPremises -> DrinkerParadox
DrinkerParadox -> IndependenceOfGeneralPremises
    intros IP A P InhA; apply (IP A P (exists x, P x) InhA); intro Hx; exact Hx.DrinkerParadox -> IndependenceOfGeneralPremises
    intros Drinker A P Q InhA H; destruct (Drinker A P InhA) as (x,Hx).Drinker:DrinkerParadox
A:Type
P:A -> Prop
Q:Prop
InhA:A
H:Q -> exists x0 : A, P x0
x:A
Hx:(exists x0 : A, P x0) -> P x
exists x0 : A, Q -> P x0
      exists x; intro HQ; apply (Hx (H HQ)).
Qed.

Independence of general premises is weaker than (generalized) excluded middle

Remark: generalized excluded middle is preferred here to avoid relying on the "ex falso quodlibet" property (i.e. False → ∀ A, A)

Definition generalized_excluded_middle :=
  forall A B:Prop, A \/ (A -> B).

Lemma excluded_middle_independence_general_premises :
  generalized_excluded_middle -> DrinkerParadox.generalized_excluded_middle -> DrinkerParadox
Proof.generalized_excluded_middle -> DrinkerParadox
  intros GEM A P x0.GEM:generalized_excluded_middle
A:Type
P:A -> Prop
x0:A
exists x : A, (exists x1 : A, P x1) -> P x
  destruct (GEM (exists x, P x) (P x0)) as [(x,Hx)|Hnot].GEM:generalized_excluded_middle
A:Type
P:A -> Prop
x0, x:A
Hx:P x
exists x1 : A, (exists x2 : A, P x2) -> P x1
GEM:generalized_excluded_middle
A:Type
P:A -> Prop
x0:A
Hnot:(exists x : A, P x) -> P x0
exists x : A, (exists x1 : A, P x1) -> P x
    exists x; intro; exact Hx.GEM:generalized_excluded_middle
A:Type
P:A -> Prop
x0:A
Hnot:(exists x : A, P x) -> P x0
exists x : A, (exists x1 : A, P x1) -> P x
    exists x0; exact Hnot.
Qed.

Axioms equivalent to classical logic

Principle of unrestricted minimization

Require Import Coq.Arith.PeanoNat.

Definition Minimal (P:nat -> Prop) (n:nat) : Prop :=
  P n /\ forall k, P k -> n<=k.

Definition Minimization_Property (P : nat -> Prop) : Prop :=
  forall n, P n -> exists m, Minimal P m.

Section Unrestricted_minimization_entails_excluded_middle.

  Hypothesis unrestricted_minimization: forall P, Minimization_Property P.

  Theorem unrestricted_minimization_entails_excluded_middle : forall A, A\/~A.unrestricted_minimization:forall P : nat -> Prop,
Minimization_Property P
forall A : Prop, A \/ ~ A
  Proof.unrestricted_minimization:forall P : nat -> Prop,
Minimization_Property P
forall A : Prop, A \/ ~ A
    intros A.unrestricted_minimization:forall P : nat -> Prop,
Minimization_Property P
A:Prop
A \/ ~ A
    pose (P := fun n:nat => n=0/\A \/ n=1).unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
A \/ ~ A
    assert (P 1) as h.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
P 1
unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
A \/ ~ A
    {unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
P 1 unfold P.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
1 = 0 /\ A \/ 1 = 1 intuition. }unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
A \/ ~ A
    assert (P 0 <-> A) as p₀.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
P 0 <-> A
unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
p₀:P 0 <-> A
A \/ ~ A
    {unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
P 0 <-> A split.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
P 0 -> A
unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
A -> P 0
      +unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
P 0 -> A intros [[_ h₀]|[=]].unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
h₀:A
A assumption.
      +unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
A -> P 0 unfold P.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
A -> 0 = 0 /\ A \/ 0 = 1 tauto. }unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
h:P 1
p₀:P 0 <-> A
A \/ ~ A
    apply unrestricted_minimization in h as ([|[|m]] & hm & hmm).unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 0
hmm:forall k : nat, P k -> 0 <= k
p₀:P 0 <-> A
A \/ ~ A
unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 1
hmm:forall k : nat, P k -> 1 <= k
p₀:P 0 <-> A
A \/ ~ A
unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
m:nat
hm:P (S (S m))
hmm:forall k : nat, P k -> S (S m) <= k
p₀:P 0 <-> A
A \/ ~ A
    +unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 0
hmm:forall k : nat, P k -> 0 <= k
p₀:P 0 <-> A
A \/ ~ A intuition.
    +unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 1
hmm:forall k : nat, P k -> 1 <= k
p₀:P 0 <-> A
A \/ ~ A right.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 1
hmm:forall k : nat, P k -> 1 <= k
p₀:P 0 <-> A
~ A
      intros HA.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 1
hmm:forall k : nat, P k -> 1 <= k
p₀:P 0 <-> A
HA:A
False apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA.unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
hm:P 1
hmm:forall k : nat, P k -> 1 <= k
p₀:P 0 <-> A
HA:False
False assumption.
    +unrestricted_minimization:forall P0 : nat -> Prop,
Minimization_Property P0
A:Prop
P:=fun n : nat => n = 0 /\ A \/ n = 1:nat -> Prop
m:nat
hm:P (S (S m))
hmm:forall k : nat, P k -> S (S m) <= k
p₀:P 0 <-> A
A \/ ~ A destruct hm as [([=],_) | [=] ].
  Qed.

End Unrestricted_minimization_entails_excluded_middle.

Require Import Wf_nat.

Section Excluded_middle_entails_unrestricted_minimization.

  Hypothesis em : forall A, A\/~A.

  Theorem excluded_middle_entails_unrestricted_minimization : 
    forall P, Minimization_Property P.em:forall A : Prop, A \/ ~ A
forall P : nat -> Prop, Minimization_Property P
  Proof.em:forall A : Prop, A \/ ~ A
forall P : nat -> Prop, Minimization_Property P
    intros P n HPn.em:forall A : Prop, A \/ ~ A
P:nat -> Prop
n:nat
HPn:P n
exists m : nat, Minimal P m
    assert (dec : forall n, P n \/ ~ P n) by auto using em.em:forall A : Prop, A \/ ~ A
P:nat -> Prop
n:nat
HPn:P n
dec:forall n0 : nat, P n0 \/ ~ P n0
exists m : nat, Minimal P m
    assert (ex : exists n, P n) by (exists n; assumption).em:forall A : Prop, A \/ ~ A
P:nat -> Prop
n:nat
HPn:P n
dec:forall n0 : nat, P n0 \/ ~ P n0
ex:exists n0 : nat, P n0
exists m : nat, Minimal P m
    destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _).em:forall A : Prop, A \/ ~ A
P:nat -> Prop
n:nat
HPn:P n
dec:forall n0 : nat, P n0 \/ ~ P n0
ex:exists n0 : nat, P n0
n':nat
HPn':P n' /\ (forall x' : nat, P x' -> n' <= x')
exists m : nat, Minimal P m
    exists n'.em:forall A : Prop, A \/ ~ A
P:nat -> Prop
n:nat
HPn:P n
dec:forall n0 : nat, P n0 \/ ~ P n0
ex:exists n0 : nat, P n0
n':nat
HPn':P n' /\ (forall x' : nat, P x' -> n' <= x')
Minimal P n' assumption.
  Qed.

End Excluded_middle_entails_unrestricted_minimization.

However, minimization for a given predicate does not necessarily imply decidability of this predicate

Section Example_of_undecidable_predicate_with_the_minimization_property.

  Variable s : nat -> bool.

  Let P n := exists k, n<=k /\ s k = true.

  Example undecidable_predicate_with_the_minimization_property : 
    Minimization_Property P.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
Minimization_Property P
  Proof.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
Minimization_Property P
    unfold Minimization_Property.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
forall n : nat, P n -> exists m : nat, Minimal P m
    intros h hn.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
exists m : nat, Minimal P m
    exists 0.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
Minimal P 0 split.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
P 0
s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
forall k : nat, P k -> 0 <= k
    +s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
P 0 unfold P in *.s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:exists k : nat, h <= k /\ s k = true
exists k : nat, 0 <= k /\ s k = true destruct hn as (k&hk₁&hk₂).s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
exists k0 : nat, 0 <= k0 /\ s k0 = true
      exists k.s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
0 <= k /\ s k = true split.s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
0 <= k
s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
s k = true
      *s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
0 <= k rewrite <- hk₁.s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
0 <= h
        apply PeanoNat.Nat.le_0_l.
      *s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h, k:nat
hk₁:h <= k
hk₂:s k = true
s k = true assumption.
    +s:nat -> bool
P:=fun n : nat => exists k : nat, n <= k /\ s k = true:nat -> Prop
h:nat
hn:P h
forall k : nat, P k -> 0 <= k intros **.s:nat -> bool
P:=fun n : nat =>
exists k0 : nat, n <= k0 /\ s k0 = true:nat -> Prop
h:nat
hn:P h
k:nat
H:P k
0 <= k apply PeanoNat.Nat.le_0_l.
  Qed.

End Example_of_undecidable_predicate_with_the_minimization_property.

Choice of representatives in a partition of bool

This is similar to Bell's "weak extensional selection principle" in [Bell]

[Bell] John L. Bell, Choice principles in intuitionistic set theory, unpublished.

Require Import RelationClasses.

Notation representative_boolean_partition :=
  (forall R:bool->bool->Prop,
    Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y).

Theorem representative_boolean_partition_imp_excluded_middle :
  representative_boolean_partition -> excluded_middle.representative_boolean_partition -> excluded_middle
Proof.representative_boolean_partition -> excluded_middle
  intros ReprFunChoice P.ReprFunChoice:representative_boolean_partition
P:Prop
P \/ ~ P
  pose (R (b1 b2 : bool) := b1 = b2 \/ P).ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
P \/ ~ P
  assert (Equivalence R).ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Equivalence R
ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
H:Equivalence R
P \/ ~ P
  {ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Equivalence R split.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Reflexive R
ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Symmetric R
ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Transitive R
    -ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Reflexive R now left.
    -ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Symmetric R destruct 1.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
x, y:bool
H:x = y
R y x
ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
x, y:bool
H:P
R y x now left.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
x, y:bool
H:P
R y x now right.
    -ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
Transitive R destruct 1, 1; try now right.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
x, y, z:bool
H:x = y
H0:y = z
R x z left; now transitivity y. }ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
H:Equivalence R
P \/ ~ P
  destruct (ReprFunChoice R H) as (f,Hf).ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
H:Equivalence R
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
P \/ ~ P clear H.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
P \/ ~ P
  destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq].ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Heq:f true = f false
P \/ ~ P
ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
P \/ ~ P
  +ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Heq:f true = f false
P \/ ~ P left.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Heq:f true = f false
P
     destruct (Hf false) as ([Hfalse|HP],_); try easy.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Heq:f true = f false
Hfalse:false = f false
P
     destruct (Hf true) as ([Htrue|HP],_); try easy.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Heq:f true = f false
Hfalse:false = f false
Htrue:true = f true
P
     congruence.
  +ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
P \/ ~ P right.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
~ P intro HP.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
HP:P
False
     destruct (Hf true) as (_,H).ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
HP:P
H:forall y : bool, R true y -> f true = f y
False apply Hneq, H.ReprFunChoice:representative_boolean_partition
P:Prop
R:=fun b1 b2 : bool => b1 = b2 \/ P:bool -> bool -> Prop
f:bool -> bool
Hf:forall x : bool,
R x (f x) /\
(forall y : bool, R x y -> f x = f y)
Hneq:f true <> f false
HP:P
H:forall y : bool, R true y -> f true = f y
R true false now right.
Qed.

Theorem excluded_middle_imp_representative_boolean_partition :
  excluded_middle -> representative_boolean_partition.excluded_middle -> representative_boolean_partition
Proof.excluded_middle -> representative_boolean_partition
  intros EM R H.EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
exists f : bool -> bool,
  forall x : bool,
  R x (f x) /\ (forall y : bool, R x y -> f x = f y)
  destruct (EM (R true false)).EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:R true false
exists f : bool -> bool,
  forall x : bool,
  R x (f x) /\ (forall y : bool, R x y -> f x = f y)
EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
exists f : bool -> bool,
  forall x : bool,
  R x (f x) /\ (forall y : bool, R x y -> f x = f y)
  -EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:R true false
exists f : bool -> bool,
  forall x : bool,
  R x (f x) /\ (forall y : bool, R x y -> f x = f y) exists (fun _ => true).EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:R true false
forall x : bool,
R x true /\ (forall y : bool, R x y -> true = true)
    intros []; firstorder.
  -EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
exists f : bool -> bool,
  forall x : bool,
  R x (f x) /\ (forall y : bool, R x y -> f x = f y) exists (fun b => b).EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
forall x : bool,
R x x /\ (forall y : bool, R x y -> x = y)
    intro b.EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
b:bool
R b b /\ (forall y : bool, R b y -> b = y) split.EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
b:bool
R b b
EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
b:bool
forall y : bool, R b y -> b = y
    +EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
b:bool
R b b reflexivity.
    +EM:excluded_middle
R:bool -> bool -> Prop
H:Equivalence R
H0:~ R true false
b:bool
forall y : bool, R b y -> b = y destruct b, y; intros HR; easy || now symmetry in HR.
Qed.

Theorem excluded_middle_iff_representative_boolean_partition :
  excluded_middle <-> representative_boolean_partition.excluded_middle <-> representative_boolean_partition
Proof.excluded_middle <-> representative_boolean_partition
  split; auto using excluded_middle_imp_representative_boolean_partition,
                    representative_boolean_partition_imp_excluded_middle.
Qed.