sci.logic
[Top] [All Lists]

Re: Must higher-order logic be typed?

Subject: Re: Must higher-order logic be typed?
From: "xilog"
Date: 27 Aug 2006 09:01:59 -0700
Newsgroups: sci.logic
Newberry wrote:
> >
> > However, if you ask "what is a higher order logic?" then one reasonable
> > answer to that might be "a logic in which it is possible to quantify
> > over sets or functions or predicates (not just over individuals)" and
> > there are many logical systems in which this can be done but which are
> > not typed (though they are not normally called higher order logics).
> > The best known is set theory
>
> This is what confuses me. Is set theory a multi-order logic done in a
> first order logic?

Its a bit like that, but the ontology is more liberal.
All the entities which exist in w-order logic at any type exist also in
the domain of Zermelo set theory.
However, there also exist additional sets whose elements do not all
have the same type.
Since the domain of set theory is not separated into types, you run the
risk of your set theory being inconsistent, and this is what lead to
the infamous "Russell's Paradox".
Russell's "Theory of Types", the precursor of modern higher order
logics, and Zermelo's axiomatisation of set theory, were both published
in 1908 and supplied two different ways of resolving the paradoxes, the
first based on types, the second based on the restriction of
comprehension to separation.

Roger Jones


<Prev in Thread] Current Thread [Next in Thread>
Privacy Policy