Ron, the logic of TLA+ is a first-order logic because you cannot quantify over operators, as in \E Op : \A x : Op(x) # x (However, note that operator definitions in TLA+ can have operator arguments.) The fact that in set theory, sets (and functions) are ordinary values and so one may quantify over them is confusing at first. As you say, the language "feels" second-order. Formally, it is not because the interpretation of "\in" is only fixed up to the (Zermelo-Fraenkel) axioms. You may want to look at http://math.stackexchange.com/questions/23799/first-order-logic-vs-second-order-logic and similar references for more in-depth discussions of this. Concerning your concrete example, \E epsilon : \A x : x # {} => epsilon[x] \in x cannot be proved because the function would have to be "too big" to be a set (its domain would have to contain all values, which is not a set but a class). However, it is easy to prove \A S : S # {} => \E epsilon \in [SUBSET S -> S] : \A x \in SUBSET S : x # {} => epsilon[x] \in x by defining the witness eps == [T \in SUBSET S |-> IF T = {} THEN CHOOSE x \in S : TRUE ELSE CHOOSE x \in T : TRUE] (The "THEN" branch is necessary to ensure eps \in [SUBSET S -> S].) Regards, Stephan
|