|
|
yuyang08@xxxxxxxxx wrote:
> Hello, everyone,
>
> May be this is another silly question. Please don't laugh. I am
> really an igorant in logic. I found some documents that describe
> high-order logic with type systems. Is it nesscessary for us to
> desribe higher-order logic with types? How shall we describe
> them without types?
I am not aware of any documented logic which is called higher-order and
is not typed.
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, but there are also a number of systems
which are called "illative combinatory logics" and whose aim is pretty
much to do the kinds of thing you do in higher order logic but without
the type system. These are based on the pure (untyped) lambda calculus
in a manner similar to that in which higher order logic can be based on
the typed lambda calculus.
Roger Jones
|
|