stringtranslate.com

Lógica de demostrabilidad

La lógica de la demostrabilidad es una lógica modal en la que el operador de caja (o de "necesidad") se interpreta como "es demostrable que". El objetivo es captar la noción de un predicado de demostración de una teoría formal razonablemente rica , como la aritmética de Peano .

Ejemplos

Existen varias lógicas de demostrabilidad, algunas de las cuales se tratan en la literatura mencionada en § Referencias. El sistema básico se conoce generalmente como GL (por Gödel – Löb ) o L o K4W ( W significa bien fundado ). Se puede obtener añadiendo la versión modal del teorema de Löb a la lógica K (o K4 ).

Es decir, los axiomas de la GL son todas las tautologías de la lógica proposicional clásica más todas las fórmulas de una de las siguientes formas:

Y las reglas de inferencia son:

Historia

El modelo GL fue desarrollado por Robert M. Solovay en 1976. Desde entonces, hasta su muerte en 1996, el principal inspirador de este campo fue George Boolos . Sergei N. Artemov , Lev Beklemishev, Giorgi Japaridze , Dick de Jongh , Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser y otros han realizado importantes contribuciones al campo .

Generalizaciones

Las lógicas de interpretabilidad y la lógica polimodal de Japaridze presentan extensiones naturales de la lógica de demostrabilidad.

Véase también

Referencias

Enlaces externos