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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 4 Dec 2015 06:44:19 -0800 (PST)*References*: <dbc52c84-b6ce-4326-aeec-a7c17dd257c0@googlegroups.com>

> So the ability to quantify over functions, plus the SUBSET and UNION operators (as well as the analogous

> INTERSECTION operator, easily defined with a set comprehension) “feel” very much second-order.

Don't forget that in ZFC a function is a class of pairs. It is possible to quantify over functions (and relations)

Don't forget that in ZFC a function is a class of pairs. It is possible to quantify over functions (and relations)

as long as they are not proper classes.

If you have doubt about that see Metamath.

If you have doubt about that see Metamath.

http://us2.metamath.org:88/mpegif/mmrecent.html

> I understand that quantifying over functions is formally an “encoding” of operators in ZF, but is there an actual

> I understand that quantifying over functions is formally an “encoding” of operators in ZF, but is there an actual

> difference between the expressivity of TLA+ and second (and higher) -order logic?

TLAPLUS uses a formal system called temporal logic of actions (TLA). It is built over a modal logic called

TLAPLUS uses a formal system called temporal logic of actions (TLA). It is built over a modal logic called

linear temporal logic (ltl). Inside TLA there is a subset of ZFC (not everything expressible in ZFC

And to tell the truth I claim that second-order logic doesn't exist. All the references to it are merely allusive and

contradictory. It's just like for the Yeti. If you are looking for something of higher order that really exists,

with axioms and all what is needed, try higher-order logic.

--

FL

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

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