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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 4 Dec 2015 07:59:32 -0800 (PST)*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com> <33ED3621-4D95-4167-9232-9404968DD8E7@gmail.com> <02b4212f-9e09-4759-96a6-d73e7ae0881f@googlegroups.com>

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 think you need to think that TLA+ only implements a part of ZFC and doesn't allow you to quantify over

variables that you will use to "operate" over something.

When you are in doubt with a formal system, look at the formal definition of its syntax and at its system

of axioms and inference rules.

--

FL

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

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

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

**Re: [tlaplus] TLA+ logic***From:*Ron Pressler

- 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):