Yes, the theory underlying TLA+ is a variant of ZFC. In most presentations that I am aware of, it is written "Zermelo-Fraenkel set theory" (sometimes "... with choice"), avoiding the more technical abbreviations ZF and ZFC.
Thanks,
Stephan
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.
-- FL
-- FL
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|