Library Coq.Logic.Diaconescu

Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi Diaconescu75. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails Excluded-Middle in Type Theory LacasWerner99.

Three variants of Diaconescu's result in type theory are shown below.

A. A proof that the relational form of the Axiom of Choice + Extensionality for Predicates entails Excluded-Middle (by Hugo Herbelin)

B. A proof that the relational form of the Axiom of Choice + Proof Irrelevance entails Excluded-Middle for Equality Statements (by Benjamin Werner)

C. A proof that extensional Hilbert epsilon's description operator entails excluded-middle (taken from Bell Bell93)

See also Carlström for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle

Diaconescu75 Radu Diaconescu, Axiom of Choice and Complementation, in Proceedings of AMS, vol 51, pp 176-178, 1975.

LacasWerner99 Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999.

Bell93 John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993

Carlström04 Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.

Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle





Section PredExt_RelChoice_imp_EM.

The axiom of extensionality for predicates





Definition PredicateExtensionality :=

  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.

From predicate extensionality we get propositional extensionality hence proof-irrelevance





Require Import ClassicalFacts.




Variable pred_extensionality : PredicateExtensionality.




Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.

Proof.

  intros A B H.

  change ((fun _ => A) true = (fun _ => B) true) in |- *.

  rewrite

   pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).

    reflexivity.

    intros _; exact H.

Qed.




Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.

Proof.

  apply (ext_prop_dep_proof_irrel_cic prop_ext).

Qed.

From proof-irrelevance and relational choice, we get guarded relational choice





Require Import ChoiceFacts.




Variable rel_choice : RelationalChoice.




Lemma guarded_rel_choice : GuardedRelationalChoice.

Proof.

 apply

  (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).

Qed.

The form of choice we need: there is a functional relation which chooses an element in any non empty subset of bool





Require Import Bool.




Lemma AC_bool_subset_to_bool :

  exists R : (bool -> Prop) -> bool -> Prop,

   (forall P:bool -> Prop,

      (exists b : bool, P b) ->

       exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).

Proof.

  destruct (guarded_rel_choice _ _ 

   (fun Q:bool -> Prop =>  exists y : _, Q y)

   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).

    exact (fun _ H => H).

  exists R; intros P HP.

  destruct (HR P HP) as (y,(Hy,Huni)).

  exists y; firstorder.

Qed.

The proof of the excluded middle

Remark: P could have been in Set or Type





Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.

Proof.

intro P.

first we exhibit the choice functional relation R


destruct AC_bool_subset_to_bool as [R H].




set (class_of_true := fun b => b = true \/ P).

set (class_of_false := fun b => b = false \/ P).

the actual "decision": is (R class_of_true) = true or false?


destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].

exists true; left; reflexivity.

destruct H0.

the actual "decision": is (R class_of_false) = true or false?


destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].

exists false; left; reflexivity.

destruct H1.

case where P is false: (R class_of_true)=true /\ (R class_of_false)=false


right.

intro HP.

assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).

intro b; split.

unfold class_of_false in |- *; right; assumption.

unfold class_of_true in |- *; right; assumption.

assert (Heq : class_of_true = class_of_false).

apply pred_extensionality with (1 := Hequiv).

apply diff_true_false.

rewrite <- H0.

rewrite <- H1.

rewrite <- H0''. reflexivity.

rewrite Heq.

assumption.

cases where P is true


left; assumption.

left; assumption.




Qed.




End PredExt_RelChoice_imp_EM.

B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality

This is an adaptation of Diaconescu's paradox exploiting that proof-irrelevance is some form of extensionality





Section ProofIrrel_RelChoice_imp_EqEM.




Variable rel_choice : RelationalChoice.




Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.

Let a1 and a2 be two elements in some type A





Variable A :Type.

Variables a1 a2 : A.

We build the subset A' of A made of a1 and a2





Definition A' := sigT (fun x => x=a1 \/ x=a2).




Definition a1':A'.

exists a1 ; auto.

Defined.




Definition a2':A'.

exists a2 ; auto.

Defined.

By proof-irrelevance, projection is a retraction





Lemma projT1_injective : a1=a2 -> a1'=a2'.

Proof.

  intro Heq ; unfold a1', a2', A'.

  rewrite Heq.

  replace (or_introl (a2=a2) (refl_equal a2)) 

     with (or_intror (a2=a2) (refl_equal a2)).

  reflexivity.

  apply proof_irrelevance.

Qed.

But from the actual proofs of being in A', we can assert in the proof-irrelevant world the existence of relevant boolean witnesses





Lemma decide : forall x:A', exists y:bool ,

  (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).

Proof.

  intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.

Qed.

Thanks to the axiom of choice, the boolean witnesses move from the propositional world to the relevant world





Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.

Proof.

  destruct 

    (rel_choice A' bool 

       (fun x y =>  projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))

    as (R,(HRsub,HR)).

    apply decide.

  destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).

  destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].

  destruct (HR a2') as (b2,(Ha2'b2,Huni2)).

  destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].

    left; symmetry; assumption.

    right; intro H.

    subst b1; subst b2.

    rewrite (projT1_injective H) in Ha1'b1.

    assert (false = true) by auto using Huni2.

    discriminate.

  left; assumption.

Qed.

An alternative more concise proof can be done by directly using the guarded relational choice





Declare Implicit Tactic auto.




Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.

Proof.

  assert (decide: forall x:A, x=a1 \/ x=a2 -> 

                exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).

    intros a [Ha1|Ha2]; [exists true | exists false]; auto.

  assert (guarded_rel_choice := 

          rel_choice_and_proof_irrel_imp_guarded_rel_choice 

          rel_choice 

          proof_irrelevance).

  destruct 

    (guarded_rel_choice A bool 

      (fun x => x=a1 \/ x=a2)

      (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))

      as (R,(HRsub,HR)).

      apply decide.

  destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity.

  destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].

  destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity.

  destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].

    left; symmetry; assumption.

    right; intro H.

    subst b1; subst b2; subst a1.

    assert (false = true) by auto using Huni2, Ha1b1.

    discriminate.

  left; assumption.

Qed.




End ProofIrrel_RelChoice_imp_EqEM.

Extensional Hilbert's epsilon description operator -> Excluded-Middle

Proof sketch from Bell Bell93 (with thanks to P. Castéran)





Notation Local "'inhabited' A" := A (at level 10, only parsing).




Section ExtensionalEpsilon_imp_EM.




Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A.




Hypothesis epsilon_spec : 

  forall (A:Type) (i:inhabited A) (P:A->Prop), 

  (exists x, P x) -> P (epsilon A i P).




Hypothesis epsilon_extensionality :

  forall (A:Type) (i:inhabited A) (P Q:A->Prop),

  (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.




Notation Local eps := (epsilon bool true) (only parsing).




Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.

Proof.

  intro P.

  pose (B := fun y => y=false \/ P).

  pose (C := fun y => y=true  \/ P).

  assert (B (eps B)) as [Hfalse|HP] 

    by (apply epsilon_spec; exists false; left; reflexivity).

  assert (C (eps C)) as [Htrue|HP] 

    by (apply epsilon_spec; exists true; left; reflexivity).

    right; intro HP.

    assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption).

    rewrite epsilon_extensionality with (1:=H) in Hfalse.

    rewrite Htrue in Hfalse.

    discriminate.

  auto.

  auto.

Qed.




End ExtensionalEpsilon_imp_EM.