>[JS] ...what creates problems
>in traditional higer-order logic is *not* the syntax, but the semantics.
>With Quine's construction, the apply operator, or the CL syntax, the
>crucial feature that keeps the logic within the realm of FOL is the
>semantics -- i.e., that there is a single domain D over which all the
>What makes HOL complicated is the assumption of a hierarchy of domains:
> 1. Ordinary variables range over a set D0 of individuals.
> 2. Variables that represent first-order predicates range over D1,
> whose cardinality is 2^card(D0).
> 3. Variables that represent second-order predicates range over D2,
> whose cardinality is 2^card(D1).
>Notice that the cardinality of these domains grows exponentially
>(and if the starting domain is countably infinite, the Ds grow
>very fast indeed).
>If you just assume a single domain D, in which everything of interest
>is a member, you never go beyond FOL. (01)
[KBL] A typed logic has quantifiers for each type, ranging over
entities of that type. Typed logics can have first-order semantics.
CL is untyped, but can represent typed logics. I can use CL to
reason about predicates or functions, and write quantified CL
expressions in which the variables range only over the predicates
and/or functions. (02)
The key assumption, as I understand it, is that in first-order
semantics, the domain D is a set, and not a proper class. We can
create syntactic conventions that restrict variable substitutions in
quantified expressions to subsets of D, but the restricted ranges are
subsets of a set, not subclasses of a proper class. This simplifies
the semantics. (03)
Is that right? (04)
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (06)