Lógica de probabilidad - Provability logic

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

Ejemplos de

Hay una serie de lógicas de demostrabilidad, algunas de las cuales se tratan en la literatura mencionada en § Referencias . El sistema básico generalmente se denomina GL (para Gödel - Löb ) o L o K4W . Se puede obtener agregando la versión modal del teorema de Löb a la lógica K (o K4 ).

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

  • Axioma de distribución : □ ( pq ) → (□ p → □ q );
  • Axioma de Löb : □ (□ pp ) → □ p .

Y las reglas de inferencia son:

  • Modus ponens : De p q y p concluyen q ;
  • Necesidad : De p concluir p .

Historia

El modelo GL fue iniciado por Robert M. Solovay en 1976. Desde entonces, hasta su muerte en 1996, el principal inspirador del 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 contribuciones significativas al campo .

Generalizaciones

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

Ver también

Referencias