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?

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?

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

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.

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

--        Computer Assisted Theorem Proving
http://www.math.gatech.edu/~belinfan/research/autoreas/

"Boyer's idea" refers to:


@misc{ boyer86set,
    author = "R. Boyer and E. Lusk and W. McCune and R. Overbeek and M.
Stickel and L.
      Wos",
    title = "Set Theory in First-Order Logic: Clauses for G¨odel's
Axioms",
    text = "R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and
L. Wos. Set
      Theory in First-Order Logic: Clauses for G¨odel's Axioms. Journal
of Automated
      Reasoning, 2:287 -- 327, 1986.",
    year = "1986"
}

which I haven't found a copy of online yet.

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Monday, 2 April 2001 17:22:50 UTC