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