1 Wright, Crispin, «A Cogent Argument Against Private Language?», dans Ph. Pettit et J. McDowell, dir, Subject, Thought, and Context, Oxford, Clarendon Press, 1986, p. 252.Google Scholar

2 Dummett, Michael, «Postscriptum» (1972) à l'article «Truth» de 1959, dans Truth and Other Enigmas, Londres, Duckworth, 1978, p. 23–24Google Scholar, trad, franç F. Pataut dans Philosophie de la logique, Paris, Éd. de Minuit, 1991, p. 77.

3 Wright, Crispin, Realism, Meaning, and Truth, Oxford, Blackwell, 1987.Google Scholar

4 Dummett, Michael, Philosophie de la logique, p. 98.Google Scholar

5 Zermelo était un réaliste de cette veine. Il attribuait les résultats d'incompletudé de Gödel à une notion d'assertabilité foncièrement pervertie par le «préjugé finitiste», et il plaidait pour une logique infinitaire, très éloignée des méthodes «imparfaites» et «trompeuses» utilisées par notre entendement fini, et dans laquelle tout énoncé vrai serait également prouvable (Zermelo, Ernst, «Über Stufen der Quantifikation und die Logik des Unendlichen», Jahresbericht der Deutschen Mathematiker-Vereinigung, vol. 41 [1932], p. 85–88).Google Scholar

6 Ceci ne vapas de soi. Selon la plupart des intuitionnistes, une preuve de/A ⊃B c'est-à-dire une construction II transformant toute preuve de A en preuve de B, devrait toujours être ratifiée par une métapreuve établissant quell possède bien la propriètè en question. Cf. sur ce point Sundholm, Göran, «Constructions, Proofs, and the Meaning of Logical Constants», Journal of Philosophical Logic, vol. 12 (1983), p. 151–172.CrossRefGoogle Scholar

7 McGinn, Colin, «Truth and Use», dans Mark Platts, dir., Reference, Truth, and Reality, Londres, Routledge and Kegan Paul, 1980, p. 19–40.Google Scholar

8 Tennant, Neil, Anti-Realism and Logic, Oxford, Clarendon Press, 1987, chap. XIGoogle Scholar. La plupart des formulations de Dummett vont dans le sens de Tennant. Cf. par exemple «What Is a Theory of Meaning? (II)» (1976), dans The Seas of Language, Oxford, Clarendon Press, 1993, p. 70Google Scholar: «Nous comprenons un énoncé donné lorsque nous savons comment reconnaître une preuve de cet énoncé quand on nous en présente une».

9 Cf. Crispin Wright: «La connaissance est […] l'aptitude à reconnaître, lorsque l'on est correctement placé, les circonstances qui répondent […] aux conditions de vérité de l'énoncé» (Realism, Meaning, and Truth, p. 53, les italiques sont de moi).

10 Church, Alonzo, Introduction to Mathematical Logic (1956), Princeton, Princeton University Press, 6^e ed., 1970, p. 53.Google Scholar

11 Dummett, Michael, The Seas of Language, p. 60.Google Scholar

12 Ibid.

13 Même si l'exécution d'une étape ne demandait que le temps mis par la lumière pour traverser un proton, l'ensemble de la procédure exigerait plus de temps que l'âge actuel de l'univers.

14 Wright, Crispin, Wittgenstein on the Foundations of Mathematics, Londres, Duckworth, 1980, p. 127.Google Scholar

15 Dummett, Michael, «Wang's Paradox» (1970), dans Truth and Other Enigmas, p. 248–249.Google Scholar

16 Dummett, Michael, Philosophie de la logique, p. 98.Google Scholar

17 Wright, Crispin, Realism, Meaning, and Truth, p. 124sq.Google Scholar

18 Cette question est régulièrement confondue avec la question qui est en quelque sorte converse, et qui est celle de savoir si tout système matériel peut être considéré, sous au moins l'une de ses descriptions, comme la réalisation d'une machine de Turing. À cette derniére, la réponse est bien sûr affirmative : tout peut être vu comme la machine triviale qui calcule la fonction constante…

19 Si Ton veut, l'effectuabilité explicite est à l'effectivité ce qu'est la calculabilité par automates linéaires bornés à la calculabilité au sens de Turing, les functions ALB-calculables étant définies comme celles des fonctions Turing-calculables dont le calcul peut être effectué sans occuper trop de place sur le ruban (précisément: le calcul de la valeur ne doit pas occuper plus de place que l'argument lui-même). Cf. Hopcroft, John E. et Ullman, Jeffrey D., Introduction to Automata Theory, Languages, and Computation, Reading, MA, Addison-Wesley, 1979, p 225.Google Scholar

La littérature courante en intelligence artificielle fournit à foison des exemples de régies explicitement effectuables. On peut se reporter, à titre d'illustration, à Kurt Konolige (A Deduction Model of Belief, Los Altos, CA, Morgan Kaufmann Publ., 1986), qui propose de ne tenir pour déductibles que les énoncés qui se déduisent en au plus n applications du modus ponens. Cette stipulation, pour ne rien dire de l'aspect logique de la chose, se heurte évidemment à la difficulté de déterminer un entier n adéquat: nous sommes certainement capables de conduire jusqu'a son terme une déduction d'une seule ligne, et nos ressourcescognitives sont suffisamment elastiques (ou suffisamment imprécises dans leurs contours) pour que nous soyons capables d'effectuer n + 1 inferences si nous sommes capables d'en effectuer n …

20 Church, Alonzo, Introduction to Mathematical Logic, p. 53, n. 121.Google Scholar

21 Dummett, Michael, Philosophic de la logique, p. 67.Google Scholar

22 Cf. Prawitz, Dag, «Ideas and Results in Proof Theory», dans Jens Erik Fenstad, dir., Proceedings of the Second Scandinavian Logic Symposium, Amsterdam, North-Holland Publications, 1975, §2.1.1, p. 244–245.Google Scholar

23 Cf. pourtant la note 6 ci-dessus.

24 Brouwer, Luitzen E. J., «De onbetrouwbaarheid der logische principes», 1908, trad, franç. Jacques Bouveresse, «Les principes logiques ne sont pas sûrs», dans François Rivenc et Philippe de Rouilhan, dir., Logique et fondements des mathématiques. Anthologie (1850–1914), Paris, Éd. Payot, 1992, p. 379–392.Google Scholar

25 En vérité, et comme le montre Michael Detlefsen («Brouwerian Intuitionism», dans Michael Detlefsen, dir., Proof and Knowledge in Mathematics, Londres-New York, Routledge, 1992, p. 239) l'affirmation vaut cum grano salis, puisqu'un effort supplemental peut etre requis pour apparier les deux justifications.

26 Prawitz, Dag, Natural Deduction: A Proof-Theoretical Study, Stockholm, Almqvist & Wiksell (Acta Stockholmiensis, Stockholm Studies in Philosophy, vol.3), 1965, p. 22–23.Google Scholar

27 Gentzen, Gerhard, «Die Widerspruchsfreiheit der reinen Zahlentheorie», Mathematische Annalen, vol. 112 (1936), p. 493–565CrossRefGoogle Scholar, trad. angl. dans M. E. Szabo, dir., The Collected Papers of Gerhard Gentzen, Amsterdam, North-Holland Publications, 1969, p. 152.

28 Au reste, la tradition intuitionniste a souvent hésité à accepter certains principes, qui ont fini par être vaille que vaille intégrés à la Vulgate, mais qui ont souleve chez certains Pères Fondateurs des réticences d'inspiration nettement «pertinentiste». On songera, par exemple, à la loi ⊥/A (ex falso quodlibet), sanctifiée par Dag Prawitz (Natural Deduction: A Proof-Theoretical Study, p. 20), mais dont Kolmogorov estimait en 1925 qu'elle n'avait et ne pouvait avoir aucun fondement intuitif, puisqu'elle demande «que nous acceptions B si le jugement vrai A est considéré comme faux» (Andrei Nikolaevich Kolmogorov, «On the Principle of Excluded Middle», dans Jean van Heijenoort, dir., From Frege to Gödel 2^eéd., Cambridge, Harvard University Press, 1971, p. 421).

29 Girard, Jean-Yves, «Linear Logic», Theoretical Computer Science, vol. 50 (1987), p. 1–102.CrossRefGoogle Scholar