diff options
Diffstat (limited to 'theories/Logic/Diaconescu.v')
| -rw-r--r-- | theories/Logic/Diaconescu.v | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 23af5afc..3317766c 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,16 +1,18 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle - in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + 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]. + Excluded-Middle in Type Theory [[LacasWerner99]]. Three variants of Diaconescu's result in type theory are shown below. @@ -23,23 +25,24 @@ Benjamin Werner) C. A proof that extensional Hilbert epsilon's description operator - entails excluded-middle (taken from Bell [Bell93]) + entails excluded-middle (taken from Bell [[Bell93]]) - See also [Carlström] for a discussion of the connection between the + See also [[Carlström04]] for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle - [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + [[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 + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999. - [Bell93] John L. Bell, Hilbert's epsilon operator and classical + [[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. + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent + to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) +Require ClassicalFacts ChoiceFacts. (**********************************************************************) (** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) @@ -54,7 +57,7 @@ Definition PredicateExtensionality := (** From predicate extensionality we get propositional extensionality hence proof-irrelevance *) -Require Import ClassicalFacts. +Import ClassicalFacts. Variable pred_extensionality : PredicateExtensionality. @@ -76,7 +79,7 @@ Qed. (** From proof-irrelevance and relational choice, we get guarded relational choice *) -Require Import ChoiceFacts. +Import ChoiceFacts. Variable rel_choice : RelationalChoice. @@ -89,7 +92,7 @@ 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. +Import Bool. Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, @@ -161,6 +164,8 @@ End PredExt_RelChoice_imp_EM. Section ProofIrrel_RelChoice_imp_EqEM. +Import ChoiceFacts. + Variable rel_choice : RelationalChoice. Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. @@ -263,7 +268,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) -(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) Local Notation inhabited A := A (only parsing). |