 Clearly, the axioms correspond directly to the natural deduction rules for these connectives, and one finds here the origin of Gentzen’s natural deduction calculi. Bernays had investigated in his Habilitationsschrift (1918) rule based calculi. However, in the given context, the simplicity of the metamathematical description of calculi seemed paramount, and in Bernays 1927 (p. 17) one finds the programmatic remark: “We want to have as few rules as possible, rather put much into axioms”.