One essential ingredient of the solution I have proposed is the remark that, when the logical constants are understood intuitionistically, the formalization (2t) of (RAR) becomes perfectly acceptable. On the other hand, when the logical constants are understood classically, (2) is utterly unacceptable. This situation is far from surprising; on the contrary, it illustrates a general truth reminded above: the classical meaning of the logical constants is deeply different from their intuitionistic meaning. Consider for instance the schema “α or not α”: classically understood (i.e., formalized as α + −α) it expresses the intuitively true principle that every proposition is either true or false, (intuitively true because our common-sense or pre-theoretic intuitions about the world are predominantly realistic) whereas intuitionistically understood

(i.e. formalized as α ∨ ¬α) it expresses the intuitively false principle that every proposition is decidable in the sense that there is either a proof or a refutation of it.

However, this situation generates a serious problem: the problem whether a rational discussion between a supporter of classical logic and a supporter of intuitionistic logic is possible at all. How is it possible that there is real disagreement or real agreement between them, given that both disagreement and agreement about a principle presuppose that the same meaning is assigned to it by both parties, while, as we have just seen, the meaning of one and the same formula drastically changes across classical and intuitionistic readings?

It seems to me that there are at least two alternative strategies to tackle the problem. The first consists in placing the discussion between the two parties before the formalization of the intuitive notions (as the logical constants, the notion of truth, and so on) into a formal language. The discussion, in this case, concerns questions like the following:

(i) Which intuitive notions should be formalized? For instance: inclusive or exclusive disjunction? Which notion of implication? Which notion of truth?

(ii) Which intuitive notion should be chosen as the key-notion of the theory of meaning, i.e. as the notion in terms of which the meaning of the expressions of the formal language (in particular of the logical constants) is to be characterized? For instance: (bivalent) truth (as the realist claims), or knowability/existence of a proof (as the neo-verificationist claims), or knowledge/actual proof (as the intuitionist claims)?

In this case the problem can be solved, provided that each party accepts the intelligibility of the key-notion adopted by the other party; for only in this case a rational discussion is possible: the same intuitive notions are accessible to both parties, and the disagreement concerns the legitimacy, the adequacy, the fruitfulness, etc. of adopting one notion or another as the key-notion. From this standpoint, Brouwer's idea that such classical notions as bivalent truth or actual infinity are unintelligible is to be abandoned, in favor of a slightly different claim: that those classical notions, precisely because they are intelligible, turn out to be incapable to play the foundational role the classicist gives them. Of course, such a claim should be motivated by a rational argument; which means that a rational discussion would be possible.

The second strategy consists in placing the discussion between the two parties after the formalization of the intuitive notions. In this case the problem of course arises, owing to the fact that the choice of different key-notions for the theory of meaning induces differences in the meaning of the logical constants. However, there may be tactics to solve it.

I hold the first alternative is better, but I have not an a priori argument; I will argue for my thesis by considering what seems a very plausible tactics and explaining why, in my opinion, it is not viable.

The tactics is based on the idea of translating one logic into the other, analogously to the case of the translation of a language into another. As a matter of fact, there are several so-called 'translations', both of classical logic/mathematics into intuitionistic logic/mathematics—the so-called negative translations (by Kolmogorov, Gödel, Gentzen, Kuroda and others); and of intuitionistic logic/mathematics into extensions of classical logic/mathematics (Shapiro, Horsten, Artemov). I shall not enter here into a detailed discussion of this tactics. I want only to stress an obvious fact: that the so-called 'translations' are not translations at all. A translation, in general, must be correct, and it is correct if it is meaning-preserving, i.e. if, for every expression

E of L (the language to be translated), its translation Tr(E ) into L t has the same

meaning as E (whatever meaning is). But there is no reason to believe that the 'translations' mentioned above are meaning-preserving. Consider for instance the BHK clause for implication; Shapiro himself admits that the notion of “transformations of proofs” cannot be captured in the language of Epistemic Arithmetic, and Smoryn´ski has observed that the 'translation' of intuitionistic logic into epistemic logic "does not capture the full flavor of talk about methods" (p. 1497).37 To make another example, Kuroda's negative translation is based on a simple idea: that intuitionistic double negation is a sort of 'equivalent' of classical truth; this is surely true if one aims at a faithful 'immersion' of classical logic into intuitionistic logic (i.e. at a representation preserving theoremhood), but not if one aims at a genuine translation, for the classical truth of α, expressed by its occurrence within any formula, is something very different from the existence of an obstacle in principle to our being able to deny that α, expressed by ¬¬α. Moreover, there seems to be a conceptual reason for the impossibility of a genuine translation of one logic into another: on the one hand, a translation is correct only if it is meaning-preserving; on the other hand, classical logic explains the meaning of the logical constants in terms of a notion (bivalent truth) the intuitionist considers unintelligible or illegitimate, and also the converse is true (the classicist finds mysterious the intuitionistic notion of general method or effective function): so it seems unlikely that one of them finds in his own language an expression with the same meaning of an expression of the other's language.

Found a mistake? Please highlight the word and press Shift + Enter