La lógica polimodal de Japaridze (GLP) es un sistema de lógica de probabilidad con infinitas modalidades de probabilidad . Este sistema ha jugado un papel importante en algunas aplicaciones de las álgebras de probabilidad en la teoría de la demostración y se ha estudiado extensamente desde finales de la década de 1980. Lleva el nombre de Giorgi Japaridze .
Lenguaje y axiomatización
El lenguaje de GLP extiende el lenguaje de la lógica proposicional clásica al incluir las series infinitas [0], [1], [2], ... de operadores de necesidad. Sus operadores de posibilidad dual <0>, <1>, <2>, ... están definidos por < n > p = ¬ [ n ] ¬ p .
Los axiomas de GLP son todas tautologías clásicas y todas fórmulas de una de las siguientes formas:
- [ n ] ( p → q ) → ([ n ] p → [ n ] q )
- [ n ] ([ n ] p → p ) → [ n ] p
- [ n ] p → [ n +1] p
- < n > p → [ n +1] < n > p
Y las reglas de inferencia son:
- De p y p → q concluir q
- De p concluir [0] p
Semántica de probabilidad
Considere una teoría T de primer orden suficientemente sólida como Peano Arithmetic PA . Defina la serie T 0 , T 1 , T 2 , ... de teorías de la siguiente manera:
- T 0 es T
- T n +1 es la extensión de T n a través de los axiomas adicionales ∀ xF ( x ) para cada fórmula F ( x ) de manera que T n prueba todas las fórmulas F (0), F (1), F (2), ...
Para cada n , sea Pr n ( x ) una aritmetización natural del predicado " x es el número de Gödel de una oración demostrable en T n " .
Una realización es una función * que envía cada átomo no lógica una de la lengua de GLP a una pena de un * del lenguaje de la T . Se extiende a todas las fórmulas del lenguaje de GLP al estipular que * conmuta con las conectivas booleanas, y que ([ n ] F ) * es Pr n (' F *') , donde ' F *' representa (el número de ) el número de Gödel de F * .
Una integridad teorema aritmético [1] para GLP establece que una fórmula F es demostrable en GLP si y sólo si, para cada interpretación * , la frase F * es demostrable en T .
La comprensión anterior de la serie T 0 , T 1 , T 2 , ... de teorías no es la única comprensión natural que arroja la solidez y la integridad de las BPL. Por ejemplo, cada teoría T n puede entenderse como T aumentada con todas las oraciones ∏ n verdaderas como axiomas adicionales. George Boolos mostró [2] que el GLP se mantiene sólido y completo con (análisis aritmética de segundo orden ) en el papel de la teoría de base T .
Otra semántica
Se ha demostrado que GLP [1] es incompleto con respecto a cualquier clase de tramas de Kripke .
Una semántica topológica natural de GLP interpreta las modalidades como operadores derivados de un espacio politopológico . Dichos espacios se denominan espacios GLP siempre que satisfacen todos los axiomas de GLP. GLP está completo con respecto a la clase de todos los espacios GLP. [3]
Complejidad computacional
El problema de ser un teorema de GLP es PSPACE completo . Por lo tanto, el mismo problema está restringido solo a fórmulas de GLP sin variables. [4]
Historia
GLP, bajo el nombre GP, fue introducido por Giorgi Japaridze en su tesis doctoral "Medios lógicos modales para investigar la probabilidad" ( Universidad Estatal de Moscú , 1986) y publicado dos años después [1] junto con (a) el teorema de completitud para GLP con con respecto a su interpretación de probabilidad (Beklemishev posteriormente presentó una prueba más simple del mismo teorema [5] ) y (b) una prueba de que los marcos de Kripke para GLP no existen. Beklemishev también realizó un estudio más extenso de los modelos de Kripke para GLP. [6] Beklemishev, Bezhanishvili, Icard y Gabelaia estudiaron modelos topológicos para GLP. [3] [7] La decidibilidad de GLP en el espacio polinómico fue probada por I. Shapirovsky, [8] y la dureza PSPACE de su fragmento libre de variables fue probada por F. Pakhomov. [4] Entre las aplicaciones más notables de GLP se encuentra su uso en el análisis teórico de pruebas de la aritmética de Peano , la elaboración de una forma canónica para recuperar la notación ordinal hasta ɛ 0 del álgebra correspondiente y la construcción de enunciados combinatorios independientes simples (Beklemishev [9] ).
George Boolos, en su libro "The Logic of Provability", hizo un estudio extenso de BPL en el contexto de las lógicas de demostrabilidad en general . [10]
Literatura
- L. Beklemishev, "Álgebras de probabilidad y ordinales de teoría de la prueba, I" . Annals of Pure and Applied Logic 128 (2004), págs. 103-123.
- L. Beklemishev, J. Joosten y M. Vervoort, "Un tratamiento final del fragmento cerrado de la lógica de demostrabilidad de Japaridze" . Journal of Logic and Computation 15 (2005), No 4, págs. 447–463.
- L. Beklemishev, "Semántica de Kripke para la lógica de demostrabilidad GLP" . Annals of Pure and Applied Logic 161, 756–774 (2010).
- L. Beklemishev, G. Bezhanishvili y T. Icar, "Sobre modelos topológicos de GLP". Formas de teoría de la prueba, Ontos Mathematical Logic, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, págs. 133-153.
- L. Beklemishev, "Sobre la interpolación de Craig y las propiedades de punto fijo de GLP". Pruebas, categorías y cálculos. S. Feferman et al., Eds., College Publications 2010. pp. 49–60.
- L. Beklemishev, "Completitud ordinal de la lógica de demostrabilidad bimodal GLB" . Lecture Notes in Computer Science 6618 (2011), págs. 1-15.
- L. Beklemishev, "Una prueba simplificada del teorema de completitud aritmética para la lógica de probabilidad GLP" . Actas del Instituto Steklov de Matemáticas 274 (2011), págs. 25–33.
- L. Beklemishev y D. Gabelaia, " Completitud topológica de la lógica de probabilidad GLP" . Annals of Pure and Applied Logic 164 (2013), págs. 1201–1223.
- G. Boolos, "La completitud analítica de las lógicas polimodales de Japaridze" . Annals of Pure and Applied Logic 61 (1993), págs. 95-111.
- G. Boolos, "La lógica de la demostrabilidad". Prensa de la Universidad de Cambridge, 1993.
- EV Dashkov, "Sobre el fragmento positivo de la lógica de probabilidad polimodal GLP". Notas matemáticas 2012; 91: 318–333.
- D. Fernandez-Duque y J. Joosten, "Well-orders in the transfinite Japaridze álgebra" [ enlace muerto ] . Logic Journal of the IGPL 22 (2014), págs. 933–963.
- G. Japaridze, "La lógica polimodal de demostrabilidad" . Lógica intencional y estructura lógica de las teorías. Metsniereba, Tbilisi, 1988, págs. 16–48 (ruso).
- F. Pakhomov, "Sobre la complejidad del fragmento cerrado de la lógica de demostrabilidad de Japaridze" . Archive for Mathematical Logic 53 (2014), págs. 949–967.
- DS Shamkanov, "Propiedades de interpolación para lógicas de probabilidad GL y GLP" . Actas del Instituto Steklov de Matemáticas 274 (2011), págs. 303–316.
- I. Shapirovsky, "PSPACE-decidibilidad de la lógica polimodal de Japaridze" . Advances in Modal Logic 7 (2008), págs. 289-304.
Referencias
- ^ a b c G. Japaridze, "La lógica polimodal de demostrabilidad" . Lógica intencional y estructura lógica de las teorías. Metsniereba, Tbilisi, 1988, págs. 16–48 (ruso).
- ^ G. Boolos, "La completitud analítica de las lógicas polimodales de Japaridze" . Annals of Pure and Applied Logic 61 (1993), págs. 95-111.
- ^ a b L. Beklemishev y D. Gabelaia, " Completitud topológica de la lógica de probabilidad GLP" . Annals of Pure and Applied Logic 164 (2013), págs. 1201–1223.
- ^ a b F. Pakhomov, "Sobre la complejidad del fragmento cerrado de la lógica de demostrabilidad de Japaridze" . Archive for Mathematical Logic 53 (2014), págs. 949–967.
- ^ L. Beklemishev, "Una prueba simplificada del teorema de completitud aritmética para la lógica de probabilidad GLP" . Actas del Instituto Steklov de Matemáticas 274 (2011), págs. 25–33.
- ^ L. Beklemishev, "Semántica de Kripke para la lógica de probabilidad GLP" . Annals of Pure and Applied Logic 161, 756–774 (2010).
- ^ L. Beklemishev, G. Bezhanishvili y T. Icard, "Sobre modelos topológicos de GLP". Formas de teoría de la prueba, Ontos Mathematical Logic, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, págs. 133-153.
- ^ I. Shapirovsky, "PSPACE-decidibilidad de la lógica polimodal de Japaridze" . Advances in Modal Logic 7 (2008), págs. 289-304.
- ^ L. Beklemishev, "Álgebras de probabilidad y ordinales de la teoría de la prueba, I" . Annals of Pure and Applied Logic 128 (2004), págs. 103-123.
- ^ G. Boolos, "La lógica de la demostrabilidad". Prensa de la Universidad de Cambridge, 1993.