> >[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
>>quantifiers range.
>>
>>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).
>>
>> 4......
>>
>>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.
>
>[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.
>
>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.
>
>Is that right? (01)
Not really. Even higher-order model theory can
all be described in set theory. What makes FO
really first-order is that it places essentially
no restrictions on the domain. It is required
only to be nonempty (and even the empty case can
be handled, with a rather awkward version of the
logic). The key semantic difference between the
other logics is that they all impose conditions
on the domain, requiring it to contain some
entities as a result of containing others. So for
example, classical second-order logic semantics
requires that the domain is contain all relations
over the base domain. Henkin-style second-order
logic requires that it contain all
lambda-definable relations. These 'comprehension
principles' are reflected in the logics having
inference rules corresponding to
lambda-conversion, or something equally powerful. (02)
My favorite example to make the point is this: given (03)
(P a) (04)
and (05)
(Q b) (06)
does it follow that (07)
(exists (r)(and (r a)(r b) )) (08)
? Ie, do a and b have a property in common? In
both classical and Henkin logic, the answer is
yes, since the relation (09)
(lambda (x)(or (P x)(Q x))) (010)
is true of both a and b, and is lambda-definable.
But in a first-order logic (with or without
sorts), the answer is no; since in a first-order
logic, there is no reason to suppose that this
relation exists. It might, but it also might not:
and in that case, the existential conclusion
would not follow. First-order logic does not
assume that anything exists other than the things
denoted by terms actually occurring in the
language itself. (011)
The mathematical characterization of this
essentially first-order nature is that a logic is
FO when it is compact (if S entails P then a
finite subset of S entails P) and satisfies the
Lowenheim/Skolem theorem (if S is satisfiable
then it is satisfiable in a countable universe).
The first says that proofs are finite, basically:
the second says that there is no way to force the
cardinality of the universe to be larger than
that of the set of actual expressions. (Its
interesting that the characteristic semantic
property of a *decidable* logic is the *finite*
model property: if S is satisfiable then it is
satisfiable in a finite universe.) (012)
Pat (013)
>
>Kathy
>
>_________________________________________________________________
>Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
>Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
>Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
>Shared Files: http://ontolog.cim3.net/file/
>Community Wiki: http://ontolog.cim3.net/wiki/
>To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
> (014)
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 cell
phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes (015)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (016)
|