[FOM] Question about Set Theory as a formal basis for mathematics
aa at tau.ac.il
Wed Mar 1 18:51:19 EST 2006
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.
School of Computer Science
email: aa at math.tau.ac.il
More information about the FOM