Hello Frédéric,
thanks for your pointers. I beg to disagree when you say that IsAFcn "defines" [x \in A |-> B]. The definition of the operator IsAFcn asserts a relation between the three primitive operators [x \in A |-> e] (functional values), DOMAIN f, and f[e], for values f that satisfy the predicate. You also need to assert the axioms (written as TLA+ sequents)
ASSUME NEW CONSTANT S, NEW CONSTANT e(_)
PROVE /\ DOMAIN [x \in S |-> e(x)] = S
/\ \A y \in S : [x \in S |-> e(x)][y] = e(y)
ASSUME NEW f, NEW g, IsAFcn(f), IsAFcn(g)
PROVE (f = g) <=> /\ DOMAIN f = DOMAIN g
/\ \A x \in DOMAIN f : f[x] = g[x]
that are indicated in the book. The theory of functions in TLAPS (more precisely, in the Isabelle backend of TLAPS, which we consider as the standard), is axiomatized in precisely this way, plus the related definitions of [S -> T] and the EXCEPT construct. I'd therefore object to your assertion that the theory is defined semantically rather than axiomatically.
Maybe one more precision, in case it wasn't obvious: the standard interpretation of functions as functional relations satisfies the TLA+ axioms – that explains why you cannot prove that the empty tuple is different from the empty set – but there could be different interpretations of functional values within the universe of set theory. For example, the theory doesn't specify if IsAFcn({}) holds or what the values of DOMAIN {} and {}[0] are. Personally, I think the question of which presentation you'd prefer boils down to a matter of taste. On one side, one could argue that the standard definition of functions in ZF is an instance of overspecification. On the other side, one can argue that the standard definition is preferable because it needs less axioms (since the concept of functions is a derived one).
As you say, and as far as I know, nobody has ever compared the expressive power of standard ZF and the TLA+ variant. But I'd be surprised if there was a significant difference.
Best,
Stephan
On Friday, April 4, 2014 6:11:17 PM UTC+2, fl wrote:
Excuse me. No what is defined by IsAFcn is the operator [ x \in A |-> B ] not
IsAFcn. I had missed the equality.
For those who are interested, the property used by TLA+ to define a function would be in
a traditional presentation of ZFC:
But even in that case it would be a relation.
--
FL