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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 2 Jun 2017 05:39:36 -0700 (PDT)*References*: <e94e6084-b49c-4a75-93dd-cbd941bb2d5b@googlegroups.com> <bbb39abb-6686-4feb-9719-21a706334762@googlegroups.com> <0f2ac112-68b2-4766-9311-f8191a5a2a6a@googlegroups.com>

Said like that it's wrong. In FOL +ZFC a variable *can* represent a set.

I suppose that to explain the problem with FOL, we must inform the reader that there exists two kinds of variables. One of them represents

the so-called individuals. The second represents propositions. In FOL only the variables that represent individuals can be quantified.

Regarding the types introduced by Russel, I suppose one must say his main issue was to remove the paradox discovered by him

regarding some previous works by Frege. According to Frege a variable representing any collection can be quantified. That can't work. With

types you constrain what can be quantified. The second way to solve the paradox is to make a distinction between the classes and the

sets. A class represents any collection. Sets are a sub-collection of classes. Axioms determinate what classes are sets. This is the

solution used in set theory, also called ZFC (Zermelo Fraenkel with choice after its inventors).

But the logic used by TLA+ is a subset of FOL + ZFC. And it uses a Gentzen style of proof with the natural deduction axioms

available. And there are some oddities like the construct of a function. But it is due to the fact that it is algorithm oriented and according to

Leslie, few mathematics are needed to speak of algorithms (that doesn't mean simple mathematics, a look at Knuth's books will demonstrate

the opposite). So anyway no type, no higher-order language.

--

FL

**Follow-Ups**:

**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

- Prev by Date:
**Re: [tlaplus] Seq({"xxx"}) is not enumerable** - Next by Date:
**Re: [tlaplus] Seq({"xxx"}) is not enumerable** - Previous by thread:
**Re: TLA+ theory blog post series + new subreddit** - Next by thread:
**Re: TLA+ theory blog post series + new subreddit** - Index(es):