diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 74 |
2 files changed, 75 insertions, 1 deletions
@@ -535,7 +535,7 @@ LOGICVO=theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo\ theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo \ - theories/Logic/ClassicalFacts.vo \ + theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo \ theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo \ theories/Logic/Decidable.vo theories/Logic/JMeq.vo diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v new file mode 100644 index 0000000000..2a501eca0c --- /dev/null +++ b/theories/Logic/ChoiceFacts.v @@ -0,0 +1,74 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(* We show that the functional formulation of the axiom of Choice + (usual formulation in type theory) is equivalent to its relational + formulation (only formulation of set theory) + the axiom of + (parametric) finite description (aka as axiom of unique choice) *) + +(* This shows that the axiom of choice can be assumed (under its + relational formulation) without known inconsistency with classical logic, + though finite description conflicts with classical logic *) + +Definition RelationalChoice := + (A:Type;B:Set;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) + -> (EXT R':A->B->Prop | + ((x:A)(EX y:B|(R x y)/\(R' x y)/\ ((y':B) (R' x y') -> y=y')))). + +Definition FunctionalChoice := + (A:Type;B:Set;R: A->B->Prop) + ((x:A)(EX y:B|(R x y))) -> (EX f:A->B | (x:A)(R x (f x))). + +Definition ParamFiniteDescription := + (A:Type;B:Set;R: A->B->Prop) + ((x:A)(EX y:B|(R x y)/\ ((y':B)(R x y') -> y=y'))) + -> (EX f:A->B | (x:A)(R x (f x))). + +Lemma lem1 : ParamFiniteDescription->RelationalChoice->FunctionalChoice. +Intros Descr RelCh. +Red; Intros A B R H. +NewDestruct (RelCh A B R H) as [R' H0]. +NewDestruct (Descr A B R') as [f H1]. +Intro x. +Elim (H0 x); Intros y [H2 [H3 H4]]; Exists y; Split; [Exact H3 | Exact H4]. +Exists f; Intro x. +Elim (H0 x); Intros y [H2 [H3 H4]]. +Rewrite <- (H4 (f x) (H1 x)). +Exact H2. +Qed. + +Lemma lem2 : FunctionalChoice->RelationalChoice. +Intros FunCh. +Red; Intros A B R H. +NewDestruct (FunCh A B R H) as [f H0]. +Exists [x,y]y=(f x). +Intro x; Exists (f x); +Split; [Apply H0| Split;[Reflexivity| Intros y H1; Symmetry; Exact H1]]. +Qed. + +Lemma lem3 : FunctionalChoice->ParamFiniteDescription. +Intros FunCh. +Red; Intros A B R H. +NewDestruct (FunCh A B R) as [f H0]. +(* 1 *) +Intro x. +Elim (H x); Intros y [H0 H1]. +Exists y; Exact H0. +(* 2 *) +Exists f; Exact H0. +Qed. + +Theorem FunChoice_Equiv_RelChoice_and_ParamFinDescr : + FunctionalChoice <-> RelationalChoice /\ ParamFiniteDescription. +Split. +Intro H; Split; [Exact (lem2 H) | Exact (lem3 H)]. +Intros [H H0]; Exact (lem1 H0 H). +Qed. |