Re: Revised Axioms for Cardinality Restrictions

>  > >Add a second argument to relation NoRepeatsList that is the length of
>>  >the list.  Then, the axiom defining NoRepeatsList becomes the following:
>>  >
>>  >(<=> (NoRepeatsList ?l ?n)
>>  >      (or (and (= ?n 0) (= ?l nil))
>>  >          (and (= ?n 1) (exists (?x) (= ?l (listof ?x))))
>>  >          (and (not (item (rest ?l) (first ?l)))
>>  >               (NoRepeatsList (rest ?l) (- ?n 1)))))   [NoRepeatsList
>>  >axiom 1]
>>  >
>>  >Add an axiom stating that NoRepeatsLists exist for any finite collection
>>  >of objects as follows:
>>  >
>>  >(=> (and (Integer ?n)
>>  >          (>= ?n 0)
>>  >          (NoRepeatsList ?l1 ?n)
>>  >          (not (item ?l1 ?x)))
>>  >     (exists (?l2) (and (NoRepeatsList ?l2 (+ ?n 1)) (item ?l2 ?x))))
>>
>>  This seems to assume that (Integer ?n) is true of only finite
>>  objects, though, which begs the question. There is no way to
>>  axiomatize this in FOL which guarantees that all things satisfying
>>  this (or any other) predicate are finite in all models. For example,
>>  suppose that there are infinite lists, say with lengths w+1, w+2,
>>  etc., where w is the first transfinite ordinal, and also that w is an
>>  integer, ie (Integer ?n) is true when '?n' denotes w, w+1, etc.. Then
>>  both your axioms are satisfied, and any first-order version of the
>>  induction axiom for arithmetic can be be satisfied also. (This
>>  follows from the compactness theorem for FOL.) The only way to rule
>>  out models like this is to go beyond first-order logic, eg by using
>>  infinitary logic, as KIF does (implicitly) in the parts that you have
>>  decided, wisely, not to use in your axioms.
>
>Can't we require the second argument of relation NoRepeatsList to be a
>finite (non-negative) integer and still remain in FOL?

Well, yes and no. Yes, you can simply stipulate that Integer is true 
of finite integers as a semantic assumption, outside of the axioms 
themselves, and work on that basis; and everything else is then in 
FOL, and you only draw FOL-valid conclusions from that. The problem 
being, of course, that this stipulation will have consequences that 
are invisible to a formal FOL reasoner working with the axioms. What 
you can't do is write a collection of first-order axioms which 
guarantee that Integer is true only of finite integers. (If you 
could, then you could axiomatize arithmetic, and Goedel's ghost would 
never give you any peace.) So you can't both claim that you are 
working in a purely first-order axiomatic framework, and also claim 
(or legitimately assume) that (Integer ?x) really says that ?x is 
finite.

>   That is, is it
>within FOL to have a relation "Finite-Integer"?

To have, in a sense, but not to have a complete axiomatization of. 
(Shouldn't be too surprising; after all, we often write predicates 
like (Is-Human ?x) without thinking that this is guaranteed to really 
mean 'is human' in *all* models, right? Someone once said that the 
integers are the work of God and all the rest is the work of Man, and 
I think this is what he meant; contrary to what pre-Goedelian 
optimists thought, the integers are more like a piece of the real 
world than most mathematical categories; they are too complicated to 
be fully captured in any set of axioms we can write down. A group is 
anything that satisfies the axioms of group theory, a set anything 
that satisfies the axioms of set theory, etc..  But the integers we 
just have to take on faith.)

>  That is what I had in
>mind regarding both the second argument of NoRepeatsList and the
>relation in the existence axiom that I called "Integer".

Yep, I thought you did. That's what Genesereth had in mind when he 
defined List in KIF as well. :-) Which, to repeat, is fine, as long 
as you don't claim to have axiomatized (exactly) what you have in 
mind.

Pat

PS. BTW, heres why you get stuck, in a nutshell. Suppose you could 
axiomatize Integer somehow so that it was true of exactly the finite 
integers, and consider the infinite disjunction
(or (= ?x 0) (= ?x 1)(= ?x 2).......)
This also is true just of the finite integers, considered as a 
predicate on ?x, so the following:
(iff (Integer ?x)
        (or (= ?x 0) (= ?x 1)(= ?x 2).......))
must be true in all models.  But you are never going to be able to 
write this in any version of FOL.
One way round is fine:
        (implies (or (= ?x 0) (= ?x 1)(= ?x 2).......) (Integer ?x))
turns into an infinite conjunction:
(and (implies (= ?x 0)(Integer ?x))
        (implies (= ?x 1)(Integer ?x))
       (implies (= ?x 2)(Integer ?x))
       .......)
which is really just an infinite collection of regular FOL axioms
(implies (= ?x 0)(Integer ?x))
(implies (= ?x 1)(Integer ?x))
(implies (= ?x 2)(Integer ?x))
.....
which is fine, and could be captured by a schema defined in terms of numerals:
(implies (= ?x [n])(Integer ?x))
which one could do pretty directly in KIF.
But its the other way round that is impossible, since that is
        (implies (Integer ?x)(or (= ?x 0) (= ?x 1)(= ?x 2).......))
which just can't be said in any first-order way.
(If you try to use a schema-like trick you get a skolemization 
problem since (exists ([n])... is inside (forall (?x)...), and how 
are you going to axiomatize the resulting function from finite 
integers to numerals?)
But you would need to be able to say this, or something equivalent to 
it, in order to have a complete theory of finiteness. As things 
stand, you can say only a finite subset of it, which always leaves 
some wiggle room to allow one of the unmentioned numerals to denote 
some transfinite ordinal and still satisfy your axioms.
(Note, this isn't a *proof* that arithmetic can't be described in 
FOL, but it helped me see what is going on.)

-- 
---------------------------------------------------------------------
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 Thursday, 13 September 2001 17:23:35 UTC