Re: [tlaplus] Curious oddity

Dear Frédéric,

On 03 Sep 2016, at 19:53, 'fl' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

Thus, your formula is valid if x and y are declared as CONSTANTS, but not if at least one of them is a VARIABLE.

But in a system independant of TLAPLUS? For example if LTL is built upon FOL, the individual variables declared by FOL and that can
be quantified are what: state variables or something else?

in classical logic, atomic propositions (in propositional logic) are either true or false and constants (in first-order logic) take fixed values, assigned once and for all by the interpretation. In modal (and in particular, temporal) logic, the interpretations of these symbols are different from one "world" (state, in the temporal interpretation) to another. In a first-order setting, one still uses ordinary ("rigid") variables so that one can compare values of variables at different states. [1]

In order to interpret a formula of temporal logic, you have to know which symbols are flexible (assigned values by states) and which are rigid (assigned values by the underlying first-order interpretation, independently of states). That's why in TLA+ you declare every parameter to be either a CONSTANT or a VARIABLE.

If this bothers you, you are not alone, but people seem to prefer writing, say,

[](x > 0)

where x is a state variable rather than

\A t \in Nat : x(t) > 0

as you would have to do if you expressed temporal properties in a purely first-order language.

As for quantification, many modal logics only have quantification over rigid variables, such that you can write, for example,

\A n \in Nat : []<>(x = n)

but in TLA there is also quantification over state variables (\AA and \EE), used in particular in connection with refinement. In quantifier contexts, the kind of the bound symbol is indicated by the quantifier.

Regards,

Stephan

[1] In theory, rigid variables can be avoided in TLA+: if all variables are assumed to be flexible, one can express that a particular variable x is rigid by writing [][FALSE]_x. However, including such a formula in every statement would be exceedingly clumsy.