Here are the (necessarily incomplete) rules, in addition to those for PTL, that we use in our book: A(t) => \E x : A(x) if t is substitutable for x [1] (next \E x : A) => \E x : next A A => next A if A is rigid (i.e., does not contain any state variable) x = x x = y => (A(x) => A(y)) A => B |- (\E x : A) => B if there is no free occurrence of x in B Most of these are standard from classical first-order logic (modulo the additional proviso in the first axiom). The second and third axiom bring in an aspect of temporal logic, expressing that quantification (over rigid variables, i.e. constants in TLA jargon) and temporal operators commute (similar laws for [], <>, and the "until" operator are then derivable), and that the interpretation of all symbols except state variables is the same in all states. For TLA, you'll need additional rules governing flexible quantification (the \EE operator). Stephan [1] The term t is called substitutable for x in formula A(x) if A(t) has no new occurrences of state variables in the scope of a temporal operator as compared with A(x). For example, consider the formula A == (x=0) /\ <>(x # 0) and a state variable v. Then v is not substitutable for x because the substitution would introduce an additional occurrence of state variable v in the scope of the <> operator. And indeed, the instance v=0 /\ <>(v # 0) => \E x : (x=0) /\ <>(x # 0) would be unsound, as the right-hand formula is equivalent to false (remember that x is a rigid variable) whereas the left-hand formula may be true in some execution. |