Peano.tla
97 views
Skip to first unread message
fl
Jun 8, 2016, 7:16:39 AM6/8/16
to tlaplus
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
Stephan Merz
Jun 8, 2016, 8:01:32 AM6/8/16
to tla...@googlegroups.com
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,
Stephan
[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).
--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
fl
Jun 9, 2016, 4:26:10 AM6/9/16
to tlaplus
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
fl
Jun 9, 2016, 6:18:33 AM6/9/16
to tlaplus
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.
Excuse me. I had misread the sentence. We agree. It is missing.
--
FL
Reply all
Reply to author
Forward
0 new messages