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.
Escribe un comentario o lo que quieras sobre Lógica demostrativa (directo, no tienes que registrarte)
Comentarios
(de más nuevos a más antiguos)