Each of set theory, higherorder logic (in the tradition of Church's Simple Type Theory, implemented in HOL or Isabelle), and strong type theories as Coq's calculus of inductive constructions has a very different "look and feel".
Looking at just expressiveness (as in flexibility), set theory is certainly stronger than HOL and I believe also than Coq. For example, HOL or Coq do not admit a set like {1, {2,3}}. In fact, the original motivations for type theory were to tame the expressiveness of set theory because it led to paradoxes.
Whether you need that power in practice is a different question. I have rarely felt bothered by the discipline that HOL imposes, and it helps proof automation. At any rate, TLA+ is more expressive than what you might ever need for specifying algorithms.
Stephan
Thank you both Stephan and FL. That Math Exchange link was particularly useful.
So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set (I've read the definition in Specifying Systems). In practice, however, it seems like this can always be avoided, and rather trivially. I have heard people dismiss TLA+ as "not even higherorder (like Coq)", and so less expressive. Similarly, I've heard people say that things like separation logic require higherorderness, but from what little I've seen of it (which is very little), it also seems to be rather trivially expressed in TLA+. Is there an actual difference in expressiveness or just a formal one?
Ron

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
