Re: [tlaplus] The Naturals module

[Stephan Merz <stephan.merz@xxxxxxxxx>]

I don’t know why that module was changed in the distribution [1] with respect to the presentation in Specifying Systems, but anyway the original definitions were not usable for the model checker and had to be overridden anyway.

For TLAPS, the situation depends on the backend:

- The SMT backend relies on an injection of the native SMT integers into the universal sort used for representing TLA+ values in the SMT encoding in order to make use of the built-in reasoning capabilities of SMT solvers on integers.

- The Isabelle backend takes the definitions from Specifying Systems and derives standard lemmas on integers / natural numbers. In particular, this requires showing that there exists a structure satisfying the Peano axioms in order to make sure that the CHOOSE expressions involved in defining natural numbers yield a structure with the expected properties.

Stephan

[1] https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/Naturals.tla

On 9 Oct 2025, at 21:31, 'Ugur Yavuz' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

In Specifying Systems, the Naturals module defines natural numbers as an arbitrary set with a constant zero and a successor function satisfying the usual Peano axioms. This is done across a number of modules, namely Peano, ProtoReals and then Naturals. 

It seems that this original formulation was later replaced by a Naturals module containing only placeholder definitions, with the expectation that TLA⁺ tools (e.g., TLC, TLAPS) would provide their own implementations of natural number operators.

Could anyone comment on this change? And more generally, how should one think about the Naturals module in TLA⁺ today?

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/07de996d-fc76-40ee-bb40-6ed5b17050c6n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/B60ADA9B-A2CC-444C-AF18-1041D5A6A210%40gmail.com.