 As we noted above, Gentzen had already begun in 1931 to be concerned with the consistency of full elementary number theory. As the logical framework he used, what we now call, natural deduction calculi. They evolved from an axiomatic calculus that had been used by Hilbert and Bernays since 1922 and introduced an important modification of the calculus for sentential logic. The connectives \(\land \) and \(\lor\) are incorporated, and the axioms for these connectives are as follows: 