Lógica demostrativa
La lógica demostrativa es una lógica modal, en la que el operador caja (o "necesidad") es interpretado significando 'debe ser demostrado que'. El aspecto que se desea capturar es la noción de un predicado de demostración de una teoría formal razonablemente rica, tal como la aritmética de Peano.
Existen varias lógicas demostrativas, algunas de las cuales están tratadas en la literatura en la sección de referencias. El sistema básico es generalmente llamado GL (por Gödel-Löb) o L o K4W. El mismo se puede obtener agregando la versión modal del teorema de Löb a la lógica K (o K4). El tema fue desarrollado por Robert M. Solovay en 1976. Desde entonces el principal investigador del tema ha sido George Boolos. Los siguientes especialistas han realizado contribuciones significativas al tema: Sergei Artemov, Lev Beklemishev, Giorgi Japaridze, Dick de Jongh, Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser entre otros. Las lógicas de interpretabilidad constituyen extensiones naturales de la lógica demostrativa.
Referencias
- George Boolos, The Logic of Provability. Cambridge University Press, 1993.
- Giorgi Japaridze and Dick de Jongh, The logic of provability. In: Handbook of Proof Theory, S. Buss, ed. Elsevier, 1998, pp. 475-546.
- Sergei Artemov and Lev Beklemishev, Provability logic. In: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, eds., vol. 13, 2nd ed., pp. 229-403. Kluwer, Dordrecht, 2004.
- Per Lindström, Provability logic - a short introduction. Theoria 62 (1996), pp. 19-61.
- Craig Smoryński, Self-reference and modal logic. Springer, Berlín, 1985.
- Robert M. Solovay, ``Provability Interpretations of Modal Logic``, Israel Journal of Mathematics, Vol. 25 (1976): 287-304.
- Provability logic, from the Stanford Encyclopedia of Philosophy.
