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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Sat, 3 Jun 2017 08:09:07 -0700 (PDT)*References*: <e94e6084-b49c-4a75-93dd-cbd941bb2d5b@googlegroups.com> <bbb39abb-6686-4feb-9719-21a706334762@googlegroups.com> <0f2ac112-68b2-4766-9311-f8191a5a2a6a@googlegroups.com> <52f15909-4904-425b-9356-f34118e155ea@googlegroups.com>

I suppose that to explain the problem with FOL, we must inform the reader that there exists two kinds of variables. One of them representsthe so-called individuals. The second represents propositions. In FOL only the variables that represent individuals can be quantified.

And regarding SOL one must explain there exists also two kinds of variables. But this time both kinds may be quantified.

But by different kinds of quantifiers. (You use two dfifferent kinds of quantifiers then but you don't explain why.)

And that for variables that represent propositions they naturally can be interpreted as sets of individuals or as functions whose

parameter is an individual and that return a boolean (it is maybe what you mean by predicate) but that doesn't prevent an

individual from representing a set anyway.

One must be very clear about the concept of individual.

--

FL

**References**:**TLA+ theory blog post series + new subreddit***From:*Ron Pressler

**Re: TLA+ theory blog post series + new subreddit***From:*Ron Pressler

**Re: TLA+ theory blog post series + new subreddit***From:*fl

**Re: TLA+ theory blog post series + new subreddit***From:*fl

- Prev by Date:
**Re: TLA+ theory blog post series + new subreddit** - Next by Date:
**Proving equivalence of AlternatingBit to ABCorrectness** - Previous by thread:
**Re: TLA+ theory blog post series + new subreddit** - Next by thread:
**Re: TLA+ theory blog post series + new subreddit** - Index(es):