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
