[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Thu, 9 Jun 2016 01:26:10 -0700 (PDT)*References*: <883fca44-784f-4645-80da-08e141e2cf2f@googlegroups.com> <CF4B03ED-86D7-4631-A6CC-7135A87E2B50@gmail.com>

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

**Follow-Ups**:**Re: [tlaplus] Peano.tla***From:*fl

**References**:**Peano.tla***From:*fl

**Re: [tlaplus] Peano.tla***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Peano.tla** - Next by Date:
**Re: [tlaplus] Peano.tla** - Previous by thread:
**Re: [tlaplus] Peano.tla** - Next by thread:
**Re: [tlaplus] Peano.tla** - Index(es):