[Top] [All Lists]

Re: [ontolog-forum] First-Order Semantics

To: Kathryn Blackmond Laskey <klaskey@xxxxxxx>
Cc: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Pat Hayes <phayes@xxxxxxx>
Date: Wed, 13 Jun 2007 10:35:50 -0500
Message-id: <p06230910c295badfbea2@[]>
>  >[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)

>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)

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