The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

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 
> <mail AT kenkubota.de>
> Betreff: Aw: [Coq-Club] is the axiom of choice... ?
> Datum: 11. September 2016 um 18:50:17 MESZ
> An: 
> coq-club AT inria.fr
> Kopie: 
> hol-info AT lists.sourceforge.net,
>  "Prof. Peter B. Andrews" 
> <andrews AT cmu.edu>
> Antwort an: 
> coq-club AT 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_rauglaudre AT 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/
>