Home Philosophy Advances in ProofTheoretic Semantics


An Intuitionistic SolutionThe first step towards an intuitionistic solution is the remark that the formalizations of (K) and (RAR) by (1) and (2), respectively, acquire a meaning very different from the intuitive one if the logical constants occurring in them are understood according to the BHKexplanation, i.e. the explanation of their intuitionistic meaning given by Brouwer, Heyting and Kolmogorov, and that the intuitionistic formulas corresponding to (1) and (2), namely (1t) (2t) α → ♦ K α α → K α, 6As it will become evident below, the argument stated in this paper in no way relies on Dummett's opinion (for which see for instance [4], p. XXII) that also an antirealist should explain meaning in terms of truthconditions. are valid, independently from there being a ChurchFitch argument (whose last step is not intuitionistically valid). (21) is intuitionistically validIntuitionists do not agree with Dummett and other neoverificationists that meaning is to be explained in any case in terms of truthconditions. According to them, "The notion of truth makes no sense […] in intuitionistic mathematics"7; the key notion of the theory of meaning is the notion of proof, and understanding α (knowing its meaning) is to be explained as being capable to recognize the proofs of α. The content of a mathematical statement α (what Frege would have called the thought expressed by α) is characterized by Heyting as the expectation of a proof of α. What a proof of α is, is explained by recursion on the logical complexity of α, under the assumption that we have an intuitive understanding of what is a proof of an atomic statement. This is the BHKexplanation. I think a revision of this explanation is necessary concerning disjunction and existential quantification.8 According to Heyting, a proof of α ∨ β is either a proof of α or a proof of β; however, even the intuitionists consider, for instance, “Prime(n) ∨¬ Prime(n)”, where n is some very large number, as assertible even if neither “Prime(n)” nor “¬ Prime(n)” is; I propose therefore to revise the BHKexplanation in the following way: A proof of α ∨ β is a procedure such that its execution yields,9 after a finite time, either a proof of α or a proof of β.10 An analogous modification of the clause for ∃x α can be similarly motivated. Summing up, the revised version of the BHKexplanation I will make reference to is the following: 
< Prev  CONTENTS  Next > 

Related topics 