In TLA+, tuples and sequences are functions. However, unlike in conventional presentations of ZF set theory, functions are not defined as relations (sets of pairs) but are primitive values, axiomatized by
IsAFcn(f) == f = [x \in DOMAIN f |-> f[x]]
See also Section 16.1.7 of "Specifying Systems".
In particular, << >> = { } is not provable in TLA+, nor is its negation.
Unconventional indeed. But what is defined here is the predicate IsAFcn not
the concept of function nor the operator [ x \in A |-> B ].
But what can we conclude from that ? That the theory
behind TLA+ is not ZFC but a theory (unspecified) less powerful than ZFC, or
that the definition of a function is not the definition we are accustomed to ?
As a rule I'm embarassed when a theory is defined by its semantic and not by axioms.
I think it's less clear.
But I suppose it would be too demanding.
Thank you for this answer.
--
FL