Hello, as Leslie implies, most working mathematicians apply the distinction intuitively, and it is only when you try to make things precise or look at foundations that you realize that you have to be careful in order to avoid the paradoxes of naive set theory. Also, the terminology is not universally accepted. Operators are often called "class functions" in standard expositions of formal set theory. Functions are objects that exist within the universe of set theory, i.e. they are themselves sets. In standard constructions of set theory they are sets of pairs (argument, result) – although TLA+ does not commit to any specific representation for functions but has dedicated syntax for functions. An operator such as \in is "too big" to be a set: its domain would have to include the collection of all sets, which is not a set itself. A classic introduction to the subject is Halmos' "Naive Set Theory" (http://www.amazon.com/Naive-Set-Theory-Paul-Halmos/dp/1614271313); it is more accessible than real formal presentations such as those by Suppes (http://www.amazon.com/Axiomatic-Theory-Dover-Books-Mathematics/dp/0486616304) or Shoenfield's chapter in the Handbook of Mathematical Logic (http://www.amazon.com/Handbook-Mathematical-Studies-Foundations-Mathematics/dp/0444863885) that go into more detail on the axiomatic systems. I find Paulson's Formath paper available at http://www.cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf a very well written, careful introduction: see e.g., the distinction between \lambda for defining operators and Lambda(_,_) for defining functions in section 2.2. However, it insists a lot on how things are encoded in the Isabelle logical framework and then describes techniques for automatic reasoning that are not relevant for understanding the basics, so your mileage may vary. In higher-order logic (aka Church's Simple Theory of Types), there is not one universe of values, but the latter are classified by types, and in particular a function does not live in the same type as its arguments or results. In this way, the paradoxes of naive set theory are avoided, and operators are just (polymorphic) functions. For example, \in has type "'a set => bool", which can be read as saying that there is a collection of functions (one per type 'a) from sets over 'a to Booleans. Similarly, the SUBSET (powerset) operator of TLA+ has type "'a set => 'a set set". Regards, Stephan
|