# Re: Infinite cardinalities

From: pat hayes <phayes@ai.uwf.edu>
Date: Tue, 3 Apr 2001 12:53:19 -0700
Message-Id: <v04210108b6efd792054f@[130.107.66.237]>
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

This archive was generated by hypermail 2.3.1 : Wednesday, 2 March 2016 11:10:34 UTC