The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

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/