Home Philosophy Advances in Proof-Theoretic Semantics
An Intuitionistic Solution
The 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 BHK-explanation, 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
(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 , p. XXII) that also an anti-realist should explain meaning in terms of truth-conditions.
are valid, independently from there being a Church-Fitch argument (whose last step is not intuitionistically valid).
(21) is intuitionistically valid
Intuitionists do not agree with Dummett and other neo-verificationists that meaning is to be explained in any case in terms of truth-conditions. 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 BHK-explanation. 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 BHK-explanation 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 BHK-explanation I will make reference to is the following:
|< Prev||CONTENTS||Next >|