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
