Logique de la prouvabilité
From Wikipedia, the free encyclopedia
En logique, une logique de la prouvabilité est une logique modale où l'opérateur modal se lit « il est prouvable que ». Il existe plusieurs logiques de la prouvabilité , par exemple, la logique GL (pour Gödel-Löb) obtenue en ajoutant un axiome qui correspond au théorème de Löb à la logique modale K4[1].
Tout a commencé lorsque Gödel, en 1933, propose une traduction de la logique intuitionniste en logique modale (la logique modale utilisée s'appelle désormais la logique S4)[2].
Notes et références
- ↑ Rineke (L.C.) Verbrugge, The Stanford Encyclopedia of Philosophy, Metaphysics Research Lab, Stanford University, (lire en ligne)
- ↑ Martin Davis, « Gödel Kurt. Eine Interpretation des intuitionistischen Aussagenkalküls (1933f). A reprint of 41812. Collected Works, Volume I, Publications 1929– 1936, by Kurt Gödel, edited by Feferman Solomon, Dawson John W. Jr., Kleene Stephen C., Moore Gregory H., Solovay Robert M., and van Heijenoort Jean, Clarendon Press, Oxford University Press, New York and Oxford1986, pp. 300, 302. Gödel Kurt. An interpretation of the intuitionistic propositional calculus (1933f). English translation by John Dawson of the preceding. Collected Works, Volume I, Publications 1929– 1936, by Kurt Gödel, edited by Feferman Solomon, Dawson John W. Jr., Kleene Stephen C., Moore Gregory H., Solovay Robert M., and van Heijenoort Jean, Clarendon Press, Oxford University Press, New York and Oxford1986, pp. 301, 303. Troelstra A. S.. Introductory note to 1933f. Collected Works, Volume I, Publications 1929– 1936, by Kurt Gödel, edited by Feferman Solomon, Dawson John W. Jr., Kleene Stephen C., Moore Gregory H., Solovay Robert M., and van Heijenoort Jean, Clarendon Press, Oxford University Press, New York and Oxford1986, pp. 296– 299. », The Journal of Symbolic Logic, vol. 55, no 1, , p. 346–346 (ISSN 0022-4812 et 1943-5886, DOI 10.2307/2274985, lire en ligne, consulté le )
