Table of Contents - 1.5. Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
In this section we introduce four additional schemes ax-10, ax-11,
ax-12, and ax-13 that are not part of Tarski's system but can be proved
(outside of Metamath) as theorem schemes of Tarski's system. These are
needed to give our system the property of "scheme completeness", which
means that we can prove (with Metamath) all possible theorem schemes
expressible in our language of wff metavariables ranging over object-language
wffs, and setvar variables ranging over object-language individual variables.
To show that these schemes are valid metatheorems of Tarski's system S2,
above we proved from Tarski's system theorems ax10w, ax11w, ax12w,
and ax13w, which show that any object-language instance of these schemes
(emulated by having no wff metavariables and requiring all setvar variables
to be mutually distinct) can be proved using only the schemes in Tarski's
system S2.
An open problem is to show that these four additional schemes are mutually
metalogically independent and metalogically independent from Tarski's. So
far, independence of ax-12 from all others has been shown, and
independence of Tarski's ax-6 from all others has been shown; see
items 9a and 11 on https://us.metamath.org/award2003.html.