[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.