# Re: Revised Axioms for Cardinality Restrictions

From: Pat Hayes <phayes@ai.uwf.edu>
Date: Thu, 13 Sep 2001 16:23:10 -0500
Message-Id: <p05101003b7c6c9606e87@[205.160.76.190]>
To: Richard Fikes <fikes@KSL.Stanford.EDU>

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

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