[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Hilbert's epsilon and TLAPLUS
Le lundi 7 avril 2014 18:08:28 UTC+2, fl a écrit :
It is said in TLA+ documentation that the theory underlying the system is ZF. But technically speaking
it is not true because Hilbert's epsilon (the CHOOSE construct) is used and this implies an extra axiom
over ZF or ZFC namely the transfinite axiom.
And moreover if Hilbert's epsilon is used the axiom of choice is a consequence and definitely
the underlying theory is more ZFC than ZF.