- From: pat hayes <phayes@ai.uwf.edu>
- Date: Tue, 3 Apr 2001 12:53:19 -0700
- To: Richard Fikes <fikes@KSL.Stanford.EDU>
- Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, kenb@ccs.neu.edu, www-rdf-logic@w3.org
> > If KIF is taken to be a strict first-order language then there > > is no way to guarantee, on semantic grounds, that all lists are > > finite. The 'definition' of lists (also called 'sequences) in the > > extant KIF literature is a little vague on just this issue. > >Chapter 8 of the "draft proposed American National Standard (dpANS)" of >KIF (at http://logic.stanford.edu/kif/dpans.html) says that a list is a >finite sequence of objects. The formal definition of a list (attached >below) given in that chapter uses a sequence variable, as you say. The >model theoretics document for KIF (at >http://logic.stanford.edu/kif/semantics.tex) says that a variable >assignment maps a sequence variable into a finite sequence of objects. >So, the prose in chapter 8 and the prose in the semantics document are >consistent in saying that lists are finite. It says that 'lists' are finite and that every interpretation must contain them all. What it doesn't say is that they must not contain any infinite lists (ie things that list terms might denote.). Which is just as well, as if it did say that, it would follow from the compactness theorem that there would be no finite axiomatization of KIF. To repeat, there is no way to guarantee that all models of any first-order sentence are finite. I am talking about theorems in metamathematics here: making assertions in standards documents is like howling at the moon. > > A working group is currently revising the KIF standard; the new > > version (a draft of which in the form of a working paper will be > > available soon) addresses this issue and provides a clear and > > unambiguous semantics for sequence quantifiers. > >I expect the new standard document will indeed clarify many such issues. > >Richard > >---------------------------------------------- > > > (defrelation list (?x) := > > (exists (@l) (= ?x (listof @l)))) Quite. Which is not first-order logic, because of the sequence quantifier. Eliminating the sequence quantifier gives an *infinitary* sentence in Lw1w: (defrelation list (?x) := (or (exists (?l1) (= ?x (listof ?l1))) (exists (?l1 ?l2) (= ?x (listof ?l1 ?l2))) (exists (?l1 ?l2 ?l3) (= ?x (listof ?l1 ?l2 ?l3))) ..... )) Now, infinitary logic *is* capable of describing finiteness (see http://plato.stanford.edu/entries/logic-infinitary/), but that is precisely why it isn't what we usually call first-order. So KIF can have it either way: it can claim the right to describe true finiteness of lists, or it can claim to be first-order . It can't have it both ways, however. --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayes
Received on Tuesday, 3 April 2001 15:51:22 UTC