Le mercredi 8 juin 2016 14:01:32 UTC+2, Stephan Merz a écrit :
- I believe the requirement that successor be injective is missing in the Peano axioms as they are given in Specifying Systems, and I added it to the definition of natural numbers that underlies the Isabelle backend of TLAPS.
The problem is that N = { 0 , 1 , 2 }, Z = 0 and Sc = 0 :> 1 @@ 1 :> 2 @@ :> 1 satisfies those axioms.
It's not what you want.
- On the other hand, the existence of a structure satisfying these axioms is proved, not assumed, in Isabelle/TLA+, from the ZFC axioms, via a fixed-point construction. This shows that the assumption is in fact unnecessary.
Sure that the existence can be proved in ZFC and the assumption can be removed. I just wanted
to say that one needs to add in a comment what you explained in the thread: we need to prove the existence
of such a structure before using CHOOSE.
--
FL