# Re: [tlaplus] << >> = { }

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]]

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.