Re: Infinite cardinalities

>pat hayes wrote:
> >
> > >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.
>
>Would you please elaborate on that?

Chris Menzel and I are writing this up now. Draft available in a few days.

>Are you just saying that the earlier KIF specs goofed,
>or are you saying that there's no way, in first order logic,
>to specify the set of finite lists?

The latter. There is no way to specify finiteness in first-order 
logic. To be precise: there is first-order sentence which has the 
property that it is true only of finite objects in every first-order 
interpretation. That is  a famous theorem about first-order logic. 
(In fact it follows from the completeness theorem.)

KIF (3.0) comes very  close to goofing, but doest quite step over the 
edge. It says that every interpretation must contain all finite lists 
(sequences), but it doesnt say that lists are *restricted* to being 
only the finite ones. People often assume that they must all be 
finite, and write recursive axioms which only work when they are 
finite, and of course they never actually get into any trouble, since 
all the lists anyone actually builds are finite; but the axioms don't 
in fact say what people often think they are saying. (To see the kind 
of thing that could go wrong, imagine building a circular list which 
would set the recursions going for ever, and think of it as a finite 
encoding of an infinite list. That infinite list satisfies all the 
first-order list axioms, so it is in some interpretation somewhere; 
so if the axiomatisations were adequate they should be able to handle 
them. But the axioms are written with one class of models in mind, 
even though they don't in fact capture that class. That is what might 
be called an ontological bug.)

>It sounds very much like a claim you made earlier
>that induction (over, say, natural numbers) isn't
>first order.

Yes, they are closely related. There is no way to write a complete 
arithmetic in first order logic either. You can write useful 
arithmetics in first order logic, but they all have 'nonstandard' 
models which cannot be ruled out by any first-order axiomatization, 
and some of those 'nonstandard' interpretations have things like 
omega-plus-one in them, ie transfinite ordinals which can violate 
induction. If we could state induction as intended, we could rule 
those out. But they can't be ruled out in first order (theorem). 
Ergo, induction isn't first-order.

The same goes for first-order set theories, by the way. (I owe you a 
reply to an earlier message which I havnt had time to finish yet and 
will send soon, which goes into this in more detail.)

>I've been researching that claim for a while, and
>I found some pretty persuasive evidence to the
>contrary; it was pointed out to me that
>
>	(a) natural induction is a theorem in set theory
>	(b) set theory has been axiomatized, finitely,
>	in first order logic
>so
>	(c) natural induction has been axiomatized,
>	finitely, in first order logic.

The problem is that the sets that are in the first-order universes of 
the first-order set theories aren't all the sets there are, so when 
those thoeries say 'for all sets S....;', they are in fact only 
quantifying over some sets (the ones they are able to describe). In 
other words, there are 'nonstandard' models of first-order set theory 
as well.  Note, this doesnt mean these theories are wrong, exactly, 
just kind of under-powered. They still pose an hell of a challenge 
for theorem-provers, though:

>I haven't found the whole argument written up in
>detail, but as to the interesting bit, (b):

>[[[
>Computer Assisted Proofs in Set Theory
>
>Belinfante's interest in computer assisted theorem proving has mainly
>concentrated on obtaining proofs of theorems in set theory using the
>first-order logic resolution-style theorem prover Otter, a powerful
>automated reasoning program developed by William McCune at
>Argonne National Laboratories.
>
>Robert Boyer's idea of using Kurt Gödel's finite axiomatization of set
>theory is the basis for all Otter proofs of theorems in set theory. Art
>Quaife in his remarkable PhD thesis showed how to reduce the
>plethora of Skolem functions that had plagued earlier work, and listed
>several hundred theorems in set theory that he proved.
>
>Belinfante explored the use of Otter for more advanced topics in set
>theory, including theorems about certain standard functions in set
>theory, cross products, ordinal number theory, equipollence, the
>theory of finite sets, partial ordering, transitive closure, and so on.
>]]]

Yes, this is very good work (though see the smartly critical review 
at http://www.maths.utas.edu.au/People/dfs/QuaifeReview.html). But it 
is proving theorems in set theory, not doing higher-order reasoning. 
In fact OTTER is really a very basic (but wonderfully fast) 
first-order resolution engine, and wouldnt be able to handle KIF as 
it stands (eg it couldnt deal with sequence quantifiers). It grinds 
through some amazingly large search spaces to prove some very simple 
things, if you check it out.

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 Tuesday, 3 April 2001 15:38:12 UTC