Re: Infinite cardinalities

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