Gentzen, in his papers for consistency proofs of arithmetic, remarked that one of the aims of his 1935 consistency proof is to give an interpretation for the implications in arithmetic. However, Gentzen eventually replaced each implication A⊃B with the formula ￢(A&￢B) at the beginning of the proof: he treated the implications A⊃B as the formulas of the form ￢(A&￢B). In the present paper, first we note that the implications can be dealt with directly in Gentzen's 1935 consistency proof. Specifically, the reduction steps (Reduktionsschritt) for the implications are made explicit in terms of his method. Second, by using Gentzen's reduction steps extended in this way, we propose an interpretation of the implications, which is stipulated without replacing the implications with other formulas.

投稿論文