Hasenjaeger [2] has answered a question raised by Hilbert and Bernays [4] p. 279, by showing that the axiom
which, within lower predicate calculus, is independent of the remaining axioms of the system (B) p. 273, is no longer independent if the axiom 0 ≡ 0 of (B) is replaced by a ≡ a. The axioms from which (Cov) can be proved form the following system (B1) (obtained from (B), of course, by dropping (Cov) and replacing 0 ≡ 0 by a ≡ a):
In what follows we consider (B1) and also the systems (B′) and (B′1) which are obtained from (B) and (B1) respectively by dropping the induction axiom and which clarify the role of the induction axiom.
1. (B1) is equivalent to (B). For (B) can be obtained from (B1) by Hasenjaeger's result. On the other hand, by pp. 263 and 261, the axioms (<1) and (J1) of (B1) can be proved from the axioms (<3) and
which belong to the system (A) p. 263. Therefore (B1) can be obtained from (A) and the induction axiom, and hence from (B).