Re: Infinite cardinalities

>Ken may have pointed out a problem with the KIF axiomatization for
>DAML+OIL.

Yes. The issue of finite models is a delicate one for KIF itself, in 
fact. 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. (It uses 
sequence quantifiers, which Richard Fikes was careful to avoid in his 
axioms.)

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.  With unrestricted 
usage of sequence quantification, KIF is a sublanguage of Lw1w, so is 
not first-order. In the meantime, one should probably think of 
'lists' in the KIF axioms as referring to entities defined by a 
first-order theory, which therefore might include infinite lists (in 
fact, lists of any cardinality.)

>However, even if we make the condition that properties have some local
>finiteness built into them (and I'm not even sure if this does follow from
>the KIF axiomatization, and it is certainly not in the model-theoretic
>semantics), this does not mean that the entire domain is finite, nor does
>it mean that a property (taken as a whole) need have a finite extension.

Indeed. This issue is local to the definition of lists. Since these 
usages in the axiomatic spec. are restricted to data-structures, an 
alternative interpretation would assume that they are defined in the 
usual way as fixedpoints of recursive specifications, and that this 
specification is external to the model theory of the KIF axioms.

Pat Hayes

---------------------------------------------------------------------
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 Monday, 2 April 2001 17:04:33 UTC