ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] First-Order Semantics

 To: Kathryn Blackmond Laskey "[ontolog-forum] " Pat Hayes Wed, 13 Jun 2007 10:35:50 -0500
 ```> >[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) ```
 Current Thread Re: [ontolog-forum] First-Order Semantics, Kathryn Blackmond Laskey Re: [ontolog-forum] First-Order Semantics, Pat Hayes <= Re: [ontolog-forum] First-Order Semantics, John F. Sowa Re: [ontolog-forum] First-Order Semantics, Pat Hayes Re: [ontolog-forum] First-Order Semantics, Christopher Menzel Re: [ontolog-forum] First-Order Semantics, Waclaw Kusnierczyk Re: [ontolog-forum] First-Order Semantics, Christopher Menzel Re: [ontolog-forum] First-Order Semantics, Waclaw Kusnierczyk Re: [ontolog-forum] First-Order Semantics, John F. Sowa Re: [ontolog-forum] First-Order Semantics, Christopher Menzel Re: [ontolog-forum] First-Order Semantics, Christopher Menzel Re: [ontolog-forum] First-Order Semantics, Waclaw Kusnierczyk