The "scheme completeness theorem", Theorem 9.7 of [Megill] p. 448 (called the "metalogical completeness theorem" there), uses a different but (logically and metalogically) equivalent set of axiom schemes for its proof. In order to show that our axiomatization is also metalogically complete, we derive the axiom schemes of that paper in this section (or mention where they are derived, if they have already been derived as theorems above). Additionally, we rederive our axiomatization from the one in the paper, showing that the two systems are equivalent.
The 14 predicate calculus axioms used by the paper are ax-c4, ax-c5, ax-11, ax-c7, ax-7, ax-c9, ax-c10, ax-c11, ax-8, ax-9, ax-c14, ax-c15, ax-c16, and ax-5. Like ours, it includes the rule of generalization (ax-gen).
The ones we need to prove from our axioms are ax-c4, ax-c5, ax-c7, ax-c9, ax-c10, ax-c11, ax-c14, ax-c15, and ax-c16. The theorems showing the derivations of those axioms, which have all been proved earlier, are axc4, axc5 (also called sp), axc7, axc9, axc10, axc11, axc14, axc15, axc16, and axc11n. In addition, ax-c11n was an intermediate axiom we adopted at one time, and we show its proof in this section as axc11nfromc11.
This section also includes a few miscellaneous legacy theorems such as hbequid use the older axioms.
Note: The axioms and theorems in this section should not be used outside of this section. Inside this section, we may use the external axioms ax-gen, ax-5, ax-7, ax-6, ax-8, and ax-9 since they are common to both our current and the older axiomatizations. (These are the ones that were never revised.)
The following newer axioms may NOT be used in this section until we have proved them from the older axioms: ax-4, ax-10, ax-6, ax-12, and ax-13. However, once we have rederived an axiom (e.g., theorem ax4fromc4 for axiom ax-4), we may make use of theorems outside of this section that make use of the rederived axiom (e.g., we may use theorem alimi, which uses ax-4, after proving ax4fromc4).