[FOM] Question about Set Theory as a formal basis for mathematics

[Arnon Avron]

On Mon, Feb 27, 2006 at 02:41:28PM -0800, John McCarthy wrote:
> >From the point of view of artificial intelligence, it is important to
> have an axiom system for set theory, e.g. ZFC, that admits short
> proofs within logic.  The axiom systems in the texts are designed to
> make it convenient to prove informally metatheorems about the
> existence of proofs.  The use of recursively defined functions is
> justified by the axiom of infinity, but the number of steps is large.
> 
> Has anyone proposed what I would call a heavy duty set of axioms for
> set theory?

Concerning this may I mention my paper:

Formalizing Set Theory  as It Is Actually Used
In Proceedings of Mathematical Knowledge Management (MKM 2004)
(A. Asperti, G. Banecerek, and A. Trybulec, eds.),
pp. 32-43, LNCS 3119, Springer, 2004.

It presents formalizations of ZF which are (I believe) easier
for use and for mechanization than those that are found in 
the usual textbooks.

Arnon Avron

School of Computer Science
Tel-Aviv University
email: aa at math.tau.ac.il
homepage: http://www.cs.tau.ac.il/~aa/

Arnon Avron