This discussion of intension and extension may be fine, but I'm
concerned that an engineer reading it might get the idea that
TLA+ has subtle problems and is difficult to understand. So, I
will explain the issue being discussed in simple terms that an
engineer will understand.
TLA+ is a precise, formal mathematical language. As far as I can
tell, mathematicians have no standard way of formalizing the concept
of a definition. Some logicians formalize the definition A == 2 by
saying that it adds the axiom A = 2. I found it simpler to make
definition a syntactic concept in TLA+, so a defined operator is
essentially a macro. This implies that the definition A == 2 means
that one can replace A by 2 or vice versa in any _expression_ without
changing the meaning of that _expression_. Thus,
(1) if A == 2 and B == 2, then A = B is true and any A appearing
in an _expression_ can be changed to B (and vice-versa) without
changing the meaning of the _expression_.
Similarly,
(2) If A(x) == 2*x and B(x) == 2*x, then for any _expression_ exp,
A(exp) can be replaced by B(exp) (and vice versa) in any
_expression_ without changing the meaning of that _expression_.
Note that in (2), I did not write A = B because that's not a legal
TLA+ _expression_. To keep TLA+ as simple as possible, equality of
operators is not expressible in it.
Also, A(x) == 2*x and A(y) == 2*y define the same operator A,
so (2) is true if the definition of A is replaced by A(y) = 2*y.
Note: A TLA+ recursive definition is shorthand for its actual
definition. For example, the recursive function definition
f[n \in Nat] == IF n = 0 THEN 1 ELSE n * f[n-1]
is shorthand for the actual definition
f == CHOOSE f : f = [n \in Nat |-> IF n = 0 THEN 1 ELSE n * f[n-1]]
The actual definition of a recursively defined operator is quite
complicated, but it defines the operator to have the expected meaning
on values of its arguments for which the recursion terminates.
-------
Let me give the name "definitional equivalence" to the general
property of definitions illustrated by (1) and (2). Definitional
equivalence is similar to the property of equality called
"substitutivity". Substitutivity asserts that exp1 = exp2 implies
that replacing exp1 by exp2 (or vice versa) in any _expression_ leaves
the value of the _expression_ unchanged. Definitional equivalence holds
for all definitions and expressions of TLA+. However, substitutivity
holds only for ordinary mathematics, which is formalized by the subset
of TLA+ obtained by eliminating the action operators and temporal
operators in Tables 3 and 4 (page 269) of "Specifying Systems". The
full TLA+ language expresses a temporal logic, and substitutivity does
not hold in temporal logic. This complicates writing proofs of
liveness properties, but it is of no concern to users of TLA+ who
don't write proofs.
Leslie