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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Wed, 8 Jun 2016 04:16:39 -0700 (PDT)

Reading the explanations of Stephan Merz in the thread "pvs, temporal logic and stacks",

it comes to my mind it was the first time I was understanding how the Peano.tla file is made.

it comes to my mind it was the first time I was understanding how the Peano.tla file is made.

Obviously with the CHOOSE construction and an assumption that guarantees the existence

of Nat, Succ and Zero you can achieve what you want.

(It means at least that sometimes a piece of explanation in the spirit of literate programming can help.)

Some more remarks however.

Here is the definition of the natural numbers in Metamath (the definition is close to TLA+ definition except it is defined

as a subset of the real numbers here).

There is an intersection at the beginning to remove the garbage implied by induction definition.

I suppose

> \A S \in SUBSET N : (Z \in S) /\ (\A n \in S : Sc[n] \in S) => (S = N)

has the same role in Peano.tla?

Peano postulates are:

4 implies that suc is an injection. I'm not sure that this is the case in the TLA+ formalization.

Wikipedia also requires suc is an injection.

Final remark. What Peano.tla is good for? Because it seems that TLAPS

relies on SMT solvers every time aritmetics are involved.

--

FL

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

- Prev by Date:
**Re: [tlaplus] specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface** - Next by Date:
**Re: [tlaplus] Peano.tla** - Previous by thread:
**Re: [tlaplus] Cannot select an Behaviour Spec for TLC-Model-Checker** - Next by thread:
**Re: [tlaplus] Peano.tla** - Index(es):