Hi Ron,
I have two comments.
First, the main reason that specifications that aren't machine closed
are usually bad has nothing to do with provability. It's because they
are usually hard to understand. Moreover, if they are supposed to
describe an algorithm, they are almost certainly wrong. There are
rare cases in which a non-machine closed spec is the best way to
describe what a system is supposed to do (rather than how it does it).
The simplest spec I know of sequential consistency is not machine
closed.
Second, you seem to forget that a TLA+ specification is a mathematical
formula. Mathematics cannot express anything about the syntax in
which a mathematical formula is written. You can model a language
like TLA+ in TLA+ and make all sorts of statements about the TLA+
formulas--for example that the meaning of a certain sequence seq of
characters is the formula F, and that seq is the shortest sequence of
characters whose meeaning is F. However, that's a statement about a
sequences of characters, not about a mathematical formula.
Thus, if Wiles's proof is correct, then the following two formulas A
and B are completely equivalent
A == q = 42
B ==
(\A x, y, z, n \in Nat \ {0} : (n>2) => (x^n + y^n # z^n))
=> (q = 42)
Thus, P(A) = P(B) for any mathematical (or TLA+) operator P. A tool
like TLC may be able to evaluate one and not the other, but that's because
tools operate on strings of characters representing formulas, not on
formulas. The correctness condition that TLC is supposed to satisfy
is that if it can evaluate both P(A) and P(B), then it gets the same
value for both . Mathematics gives no meaning to the concept of evaluation
of a formula.
If you want to distinguish between two TLA+ formulas that are
mathematically equivalent (which I believe is what you mean by
equivalent with respect to behaviors), then you're looking for a tool
not for a logic. We already have one such tool: the TLATeX
pretty-printer. Also, a lot of the output that TLC produces depends
on the particular way a specification is written--even if TLC
produces the same yes or no answer of whether the spec satisfies the
properties that TLC is checking. Perhaps there are others tools that
can tell us something useful about a specification that depends on how
it's written.
Leslie