Dear Daniel de Rauglaudre, dear List Members, A mechanized proof (i.e., verified in the R0 implementation) of (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) avoiding any appeal to the Axiom of Choice is now available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_proof_of_K8033.pdf
Instead of the Axiom of Choice, the (much weaker) Axiom of Descriptions is used. The Axiom of Descriptions for R0 is available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (p. 351 f.) The required theorem was theorem 5311 [cf. Andrews, 2002, p. 235] (which in turn requires the Axiom of Descriptions), not theorem 5312. Kind regards, Ken Kubota References Kubota, Ken (2015c), Proof of K8033. Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_proof_of_K8033.pdf (September 12, 2016). SHA-512: 5864427d033e7135c17f3a5c88fefc70 4faa3a24c9e03ab2f6a5889b5012542e b83d7db208238bddce7344378afac81d 1f4cc3313b9e58f6009eae943a2d98b0. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 > Anfang der weitergeleiteten Nachricht: > > Von: Ken Kubota <m...@kenkubota.de> > Betreff: Aw: [Coq-Club] is the axiom of choice... ? > Datum: 11. September 2016 um 18:50:17 MESZ > An: coq-c...@inria.fr > Kopie: hol-info@lists.sourceforge.net, "Prof. Peter B. Andrews" > <andr...@cmu.edu> > Antwort an: coq-c...@inria.fr > > Dear Daniel de Rauglaudre, > dear List Members, > > The proposition > (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) > you want to prove is very similar to an exercise in the main work of Andrews > [cf. Andrews, 2002, p. 237 (X5308)], > AC^b → (∀ x, ∃ y, P x y) = ∃ f, ∀ x, P x (f x) > where it is the consequent of an implication, but using the (weaker) > existential quantifier > instead of the uniqueness quantifier, and an equivalence instead of the > implication, > and the antecedent of the implication is (an instantiation of) the Axiom of > Choice. > > The two major logistic systems based on Church's simple theory of types [cf. > Church, 1940] > are Mike Gordon's HOL and Peter B. Andrews' Q0, which differ in the treatment > of the Axiom of Choice. > Mike Gordon's HOL implements the epsilon operator which requires the Axiom of > Choice, > whereas Peter B. Andrews' Q0 implements the description operator, such that > the Axiom of Choice can be avoided. > It should be noted that already Gordon himself wrote that "the > [epsilon]-operator looks rather suspicious". > Details are discussed at > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September/msg00014.html > > Information on Mike Gordon's HOL is available in [Gordon/Melham, 1993] and at > https://hol-theorem-prover.org > which is a polymorphic version of Church's simple theory of types. > Descendants are Larry Paulson's Isabelle/HOL and John Harrison's HOL Light. > > Information on Peter B. Andrews' Q0 is available in [Andrews, 2002, pp. > 210-215] and at > http://plato.stanford.edu/entries/type-theory-church/#ForBasEqu > which is, like Church's original theory, a simple type theory. > A descendant is R0, a dependent type theory (and an implementation), to be > announced at > http://dx.doi.org/10.4444/100.10 > > Since you use a stronger hypothesis (involving the uniqueness quantifier), > I believe there is a possibility of proving your proposition without using > the Axiom of Choice, > but requiring the Axiom of Descriptions only. The Axiom of Descriptions allows > one to extract the single element from a singleton (unit set). > At the very first glance, your proposition might be derivable from theorem > 5312 > [cf. Andrews, 2002, p. 235]. > > > Kind regards, > > Ken Kubota > > > > References > > Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9 > (Hardcover). ISBN 0-12-058536-7 (Paperback). > > Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: > Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: > 10.1007/978-94-015-9934-4. > > Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia > of > Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at > http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July > 2, > 2016). > > Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: > Journal of Symbolic Logic 5, pp. 56-68. > > Gordon, Michael J. C., and Melham, Thomas F., eds. (1993), Introduction to > HOL: > A theorem proving environment for higher order logic, Cambridge: Cambridge > University Press. ISBN 0-521-44189-7. > > Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, > 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 > 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 > 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: > http://dx.doi.org/10.4444/100.10 > > Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (p. 1, pp. 356-364, pp. > 411-420, and pp. 754-755). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > > (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c > 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 > 3d1047d1831bc357eb57b263b44c885b. > > Kubota, Ken (2015b), Excerpt from [Kubota, 2015] (p. 1, pp. 165-174, and pp. > 350-352). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf > > (August 13, 2016). SHA-512: 8702d932d50f2e1f6b592dc03b6f283e > 64ba18f881150b4ae32e4b915249d241 3db34ba4c3dcf0e0cdef25b679d9615f > 424adb1803a179e578087ded31b573b9. > > ____________________ > > Ken Kubota > doi: 10.4444/100 > http://dx.doi.org/10.4444/100 > > > >> Am 11.09.2016 um 11:09 schrieb Daniel de Rauglaudre >> <daniel.de_rauglau...@inria.fr>: >> >> Hi all, >> >> Is the axiom of choice required if all sets have one only element ? >> If not, how to prove it ? >> >> Russel said that if all sets contain a pair of socks, we need the axiom >> of choice to select a sock in each pair but that if they are shoes, >> we don't need it, because the choice function can be : "take the left >> shoe". >> >> But for sets of one only element ? >> >> Namely, I want to prove : >> (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x) >> >> Is is possible, or do I need the […] axiom of choice ? >> >> Thanks. >> >> -- >> Daniel de Rauglaudre >> http://pauillac.inria.fr/~ddr/ > ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info