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

[John McCarthy]

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