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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Fri, 4 Dec 2015 07:24:00 -0800 (PST)*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com>

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 higher-order (like Coq)", and so less expressive. Similarly, I've heard people say that things like separation logic require higher-orderness, 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

**Follow-Ups**:**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

**Re: [tlaplus] TLA+ logic***From:*fl

**References**:**TLA+ logic***From:*Ron Pressler

**Re: [tlaplus] TLA+ logic***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLA+ logic** - Next by Date:
**Re: [tlaplus] TLA+ logic** - Previous by thread:
**Re: [tlaplus] TLA+ logic** - Next by thread:
**Re: [tlaplus] TLA+ logic** - Index(es):