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

Re: [tlaplus] Peano.tla

Just a few comments:

- 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.

- 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.

- TLA+ first defines natural numbers; real numbers are defined later as a superset of the natural numbers in module ProtoReals.

- TLAPS indeed mostly relies on the SMT backend for reasoning about arithmetic. This reflects common experience that foundational definitions are rarely a good basis for automated reasoning. The definitions are nevertheless valuable because they can help you understand the logical structure. The Isabelle backend derives many facts of arithmetic from the definitions, even if only few are available for automatic reasoning. Eventually, we aim at certifying SMT proofs using Isabelle/TLA+ (similar to how this is done in Isabelle/HOL [1,2]), and thus the foundational definitions become the ultimate justification of arithmetic proofs, even if the SMT solver does not use them directly for finding the proof.

Best regards,

[1] Sascha Böhme, Tjark Weber: Fast LCF-Style Proof Reconstruction for Z3. Interactive Theorem Proving 2010, LNCS 6172, pp. 179-194 (2010).
[2] Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. J. Autom. Reasoning 51(1): 109-128 (2013).

On 08 Jun 2016, at 13:16, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

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.

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.



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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.