Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and Arithmetic

摘要

The purpose of this paper is to make clear the difference between Heyting, who was a representative scholar of the intuitionist school and who first introduced the intuitionistic formal logic and arithmetic, and Gentzen, who was a representative scholar of the Hilbertian finitist school, by a close look at their constructive interpretations of logical connectives. We show that although both Gentzen and Heyting proposed very similar constructive interpretations for logical connectives of intuitionistic logic mathematically, their interpretations were based on very different standpoints philosophically: Gentzen used the logical positivist way of verification theory of meaning, while Heyting emphasized the Husserlian phenomeno-logical way of verification theory of meaning. In addition, we shall point out that although both Heyting and Gentzen emphasized similar forms of constructive interpretation for the intuitionistic implication in terms of "proof-construction", the notion of "proof" here was taken very differently by Gentzen and Heyting, resulted in the different attitudes towards the intuitionistic logic.