Lógica De Demostrabilidad

Tabla de contenido:

Lógica De Demostrabilidad
Lógica De Demostrabilidad

Vídeo: Lógica De Demostrabilidad

Vídeo: Lógica De Demostrabilidad
Vídeo: inferencias lógicas, Método Directo 2024, Marzo
Anonim

Navegación de entrada

  • Contenido de entrada
  • Bibliografía
  • Herramientas académicas
  • Vista previa de PDF de amigos
  • Información de autor y cita
  • Volver arriba

Lógica de demostrabilidad

Publicado por primera vez el miércoles 2 de abril de 2003; revisión sustantiva mié 5 abr 2017

La lógica de demostrabilidad es una lógica modal que se utiliza para investigar lo que las teorías aritméticas pueden expresar en un lenguaje restringido acerca de sus predicados de demostrabilidad. La lógica se ha inspirado en desarrollos en metamatemáticas como los teoremas de incompletitud de Gödel de 1931 y el teorema de Löb de 1953. Como lógica modal, la lógica de demostrabilidad se ha estudiado desde principios de los años setenta, y ha tenido importantes aplicaciones en los fundamentos de las matemáticas.

Desde un punto de vista filosófico, la lógica de demostrabilidad es interesante porque el concepto de demostrabilidad en una teoría aritmética fija tiene un significado único y no problemático, además de conceptos como la necesidad y el conocimiento estudiados en lógica modal y epistémica. Además, la lógica de demostrabilidad proporciona herramientas para estudiar la noción de autorreferencia.

  • 1. La historia de la lógica de demostrabilidad
  • 2. El sistema de axioma de la lógica de demostrabilidad proposicional

    • 2.1 Axiomas y reglas
    • 2.2 El teorema del punto fijo
  • 3. Posible semántica de mundos y semántica topológica

    • 3.1 Caracterización y solidez modal
    • 3.2 Completitud modal
    • 3.3 Fracaso de la integridad completa
    • 3.4 Semántica topológica para la lógica de demostrabilidad
  • 4. Lógica de demostrabilidad y aritmética de Peano

    • 4.1 Solidez aritmética
    • 4.2 Integridad aritmética
  • 5. El alcance de la lógica de demostrabilidad

    • 5.1 Límites
    • 5.2 Lógica de interpretabilidad
    • 5.3 Cuantificadores proposicionales
    • 5.4 Lógicas de demostrabilidad bimodal y polimodal de Japaridze
    • 5.5 Lógica de demostrabilidad de predicado
    • 5.6 Otras generalizaciones
  • 6. Significado filosófico
  • Bibliografía
  • Herramientas académicas
  • Otros recursos de internet

    • Artículos y presentaciones
    • Otros sitios
  • Entradas relacionadas

1. La historia de la lógica de demostrabilidad

Dos líneas de investigación han llevado al nacimiento de la lógica de demostrabilidad. El primero proviene de un artículo de K. Gödel (1933), donde introduce las traducciones de la lógica proposicional intuicionista a la lógica modal (más precisamente, en el sistema hoy en día llamado S4), y menciona brevemente que la demostrabilidad puede verse como un operador modal. Incluso antes, CI Lewis comenzó el estudio moderno de la lógica modal al introducir una implicación estricta como un tipo de deducibilidad, donde puede haber significado deducibilidad en un sistema formal como Principia Mathematica, pero esto no está claro en sus escritos.

El otro capítulo comienza con la investigación en metamatemáticas: ¿qué pueden decir las teorías matemáticas sobre sí mismos al codificar propiedades interesantes? En 1952, L. Henkin formuló una pregunta engañosamente simple inspirada en los teoremas de incompletitud de Gödel. Para formular la pregunta de Henkin, se necesitan más antecedentes. Como recordatorio, el primer teorema de incompletitud de Gödel establece que, para una teoría formal suficientemente fuerte como la Aritmética de Peano, cualquier oración que afirme su propia imposibilidad de prueba no es demostrable. Por otro lado, desde "fuera" de la teoría formal, uno puede ver que tal oración es verdadera en el modelo estándar, apuntando a una distinción importante entre verdad y demostrabilidad.

Más formalmente, dejemos que (ulcorner A / urcorner) denote el número de Gödel de fórmula aritmética (A), que es el resultado de asignar un código numérico a (A). Sea (Prov) el predicado de demostrabilidad formalizado para Aritmética de Peano, que tiene la forma (exist p \, / Proof (p, x)). Aquí, (Proof) es el predicado de prueba formalizado de Aritmética de Peano, y (Proof (p, x)) significa "código Gödel (p) una prueba correcta de los axiomas de Aritmética de Peano de la fórmula con el número de Gödel (x) ". (Para una formulación más precisa, ver Smoryński (1985), Davis (1958).) Ahora, supongamos que la Aritmética de Peano demuestra (A / leftrightarrow / neg) (Prov (ulcorner A / urcorner)), luego por el resultado de Gödel, (A) no es demostrable en Aritmética de Peano, y por lo tanto es cierto, porque de hecho la oración autorreferencial (A) dice "No soy demostrable".

Henkin, por otro lado, quería saber si se podía decir algo sobre las oraciones que afirman su propia capacidad de prueba: suponiendo que la Aritmética de Peano demuestra (B / leftrightarrow / Prov (ulcorner B / urcorner)), ¿qué implica esto acerca de (B)? Tres años después, M. Löb asumió el desafío y respondió a la pregunta de Henkin de una manera sorprendente. A pesar de que todas las oraciones demostrables en Peano Arithmetic son verdaderas sobre los números naturales, Löb demostró que la versión formalizada de este hecho, (Prov (ulcorner B / urcorner) rightarrow B), solo se puede probar en Peano Arithmetic en el caso trivial de que la aritmética de Peano ya demuestra (B) en sí misma. Este resultado, ahora llamado teorema de Löb, responde inmediatamente a la pregunta de Henkin. (Para una prueba del teorema de Löb, consulte la Sección 4.) Löb también mostró una versión formalizada de su teorema,a saber, que la aritmética de Peano demuestra

) Prov (ulcorner / Prov (ulcorner B / urcorner) rightarrow B / urcorner) rightarrow / Prov (ulcorner B / urcorner).)

En el mismo artículo, Löb formuló tres condiciones sobre el predicado de demostrabilidad de Peano Aritmética, que forman una modificación útil de las complicadas condiciones que Hilbert y Bernays introdujeron en 1939 para probar el segundo teorema de incompletitud de Gödel. A continuación, la derivabilidad de (A) de la aritmética de Peano se denota por (PA / vdash A):

  1. Si (PA / vdash A), entonces (PA / vdash / Prov (ulcorner A / urcorner));
  2. (PA / vdash / Prov (ulcorner A / rightarrow B / urcorner) rightarrow (Prov (ulcorner A / urcorner) rightarrow / Prov (ulcorner B / urcorner));)
  3. (PA / vdash / Prov (ulcorner A / urcorner) rightarrow / Prov (ulcorner / Prov (ulcorner A / urcorner) urcorner).)

Estas condiciones de Löb, como se las llama hoy en día, parecen pedir una investigación lógica modal, donde la modalidad (Box) representa la probabilidad en AP. Irónicamente, la primera vez que la versión formalizada del teorema de Löb se declaró como el principio modal

) Box (Box A / rightarrow A) rightarrow / Box A)

fue publicado en un artículo de Smiley en 1963 sobre la base lógica de la ética, que no consideraba la aritmética en absoluto. Sin embargo, las investigaciones más relevantes comenzaron seriamente solo veinte años después de la publicación del artículo de Löb. A principios de la década de 1970, se vio el rápido desarrollo de la lógica de demostrabilidad proposicional, donde varios investigadores de diferentes países probaron de forma independiente los resultados más importantes, discutidos en las Secciones 2, 3 y 4. La lógica de demostrabilidad proposicional resultó capturar exactamente lo que muchas teorías formales de la aritmética pueden decir por medios proposicionales acerca de su propio predicado de demostrabilidad. Más recientemente, los investigadores han investigado los límites de este enfoque y han propuesto varias extensiones más interesantes y expresivas de la lógica de demostrabilidad (ver Sección 5).

2. El sistema de axioma de la lógica de demostrabilidad proposicional

El lenguaje lógico de la lógica de comprobabilidad proposicional contiene, además de átomos proposicionales y los operadores habituales de verdad funcional, así como el símbolo de contradicción (bot), un operador modal (Box) con el significado deseado " (T) ", donde (T) es una teoría formal suficientemente fuerte, digamos Aritmética de Peano (ver Sección 4). (Diamond A) es una abreviatura de (neg \, / Box / neg \, A). Por lo tanto, el lenguaje es el mismo que el de los sistemas modales como K y S4 presentados en la lógica modal de entrada.

2.1 Axiomas y reglas

La lógica de demostrabilidad proposicional a menudo se llama GL, después de Gödel y Löb. (Los nombres alternativos encontrados en la literatura para sistemas equivalentes son L, G, KW, K4W y PrL). La lógica GL resulta de agregar el siguiente axioma a la lógica modal básica K:

) tag {GL} Box (Box A / rightarrow A) rightarrow / Box A.)

Como recordatorio, debido a que GL extiende K, contiene todas las fórmulas que tienen la forma de una tautología proposicional. Por la misma razón, GL contiene el

) tag {Axioma de distribución} Box (A / rightarrow B) rightarrow (Box A / rightarrow / Box B).)

Además, está cerrado bajo la Regla Modus Ponens, que permite derivar (B) de (A / rightarrow B) y (A), y la Regla de generalización, que dice que si (A) es un teorema de GL, entonces también lo es (Box A).

La noción (GL / vdash A) denota la probabilidad de una fórmula modal (A) en la lógica de demostrabilidad proposicional. No es difícil ver que el axioma modal (Box A / rightarrow / Box / Box A) (conocido como Axiom 4 de lógica modal) es demostrable en GL. Para probar esto, uno usa la sustitución (A / wedge / Box A) para (A) en el axioma (GL). Luego, al ver que el antecedente de la implicación resultante se deriva de (Box A), se aplica el Axioma de Distribución y la Regla de Generalización, así como cierta lógica proposicional. A menos que se indique explícitamente lo contrario, en la secuela "lógica de demostrabilidad" representa el sistema GL de lógica de demostrabilidad proposicional.

En cuanto a la teoría de la prueba de la lógica de demostrabilidad, Valentini (1983) demostró que una formulación de cálculo secuencial estándar de GL obedece a la eliminación del corte, lo que significa, aproximadamente formulada, que cada fórmula demostrable a partir de GL en el cálculo secuencial también tiene una prueba secuencial GL sin desvíos”(vea la entrada sobre el desarrollo de la teoría de la prueba para una explicación precisa de la eliminación del corte). En los últimos años, ha habido un renovado interés en la teoría de prueba de GL, ver por ejemplo Goré y Ramanayake (2008). La eliminación de corte conduce a la propiedad de subformula deseable para GL, porque todas las fórmulas que aparecen en una prueba sin corte son subformulas de las fórmulas finales posteriores.

Para investigaciones recientes teóricas de prueba de lógica de demostrabilidad basadas en diferentes cálculos secuenciales sin cortes, ver (Negri 2005, 2014; Poggiolesi 2009). Negri presenta dos cálculos secuenciales etiquetados equivalentes para GL y una prueba sintáctica de eliminación de corte. Incluso si una propiedad de subformula completa no se cumple para estos cálculos debido al etiquetado, se pueden establecer las consecuencias habituales de la propiedad de subformula: El formalismo etiquetado permite una prueba de integridad directa, que se puede utilizar para establecer la capacidad de decisión, así como el modelo finito. propiedad, lo que significa que cualquier fórmula que no sea demostrable tiene un contramodelo finito.

Un nuevo desarrollo teórico de prueba intrigante es la expansión de Shamkanov de sistemas de prueba de estilo secuencial al permitir pruebas circulares (Shamkanov 2014). Considere un sistema secuencial para K4, el sistema modal resultante de GL reemplazando el axioma GL por el axioma más débil (Box A / rightarrow / Box / Box A) (axiom 4). Sin embargo, suponga que se permiten hipótesis abiertas, siempre que la misma secuencia ocurra estrictamente debajo de esa hipótesis en el árbol de prueba. Formulado más técnicamente, uno puede encontrar una derivación circular de un árbol de derivación ordinario al vincular cada una de sus hojas no axiomáticas con un nodo interior idéntico. Shamkanov (2014) demostró que el sistema resultante es consistente y que, además, en general, cada secuenciante tiene una derivación GL si y solo si tiene una derivación K4 circular. Las pruebas circulares también proporcionan un método para demostrar, teóricamente, que el teorema de interpolación de Lyndon es válido para GL. La interpolación estándar para GL ya había sido probada anteriormente por diferentes métodos (Boolos 1979; Smoryński 1978; Rautenberg 1983). (Para obtener más información sobre el teorema de interpolación de Lyndon para la lógica de primer orden, consulte también la teoría del modelo de primer orden de entrada).

2.2 El teorema del punto fijo

El principal resultado "modal" sobre la lógica de demostrabilidad es el teorema del punto fijo, que D. de Jongh y G. Sambin probaron independientemente en 1975 (Sambin 1976). Aunque está formulado y probado por métodos estrictamente modales, el teorema del punto fijo todavía tiene una gran importancia aritmética. Dice esencialmente que la autorreferencia no es realmente necesaria, en el siguiente sentido. Suponga que todas las ocurrencias de la variable proposicional (p) en una fórmula dada (A (p)) están bajo el alcance del operador de probabilidad, por ejemplo (A (p) = / neg / Box p), o (A (p) = / Box (p / rightarrow q)). Luego hay una fórmula (B) en la que (p) no aparece, de modo que todas las variables proposicionales que ocurren en (B) ya aparecen en (A (p)), y tal que

) GL / vdash B / leftrightarrow A (B).)

Esta fórmula (B) se llama un punto fijo de (A (p)). Además, el punto fijo es único, o más exactamente, si hay otra fórmula (C) tal que (GL / vdash C / leftrightarrow A (C)), entonces debemos tener (GL / vdash B / leftrightarrow C). La mayoría de las pruebas en la literatura dan un algoritmo por el cual se puede calcular el punto fijo (ver Smoryński 1985, Boolos 1993, Sambin y Valentini 1982, Lindström 2006). Una prueba particularmente corta y clara, así como un algoritmo muy eficiente para calcular puntos fijos, se pueden encontrar en Reidhaar-Olson (1990).

Por ejemplo, suponga que (A (p) = / neg \, / Box p). Entonces el punto fijo producido por dicho algoritmo es (neg \, / Box / bot), y de hecho uno puede probar que

) GL / vdash / neg \, / Box / bot / leftrightarrow / neg \, / Box (neg \, / Box / bot).)

Si esto se lee aritméticamente, la dirección de izquierda a derecha es solo la versión formalizada del segundo teorema de incompletitud de Gödel: si una teoría formal suficientemente fuerte (T) como Peano Arithmetic no prueba una contradicción, entonces no es demostrable en (T) que (T) no prueba una contradicción. Por lo tanto, las teorías aritméticas consistentes suficientemente fuertes no pueden probar su propia consistencia. Pasaremos a estudiar la relación entre la lógica de demostrabilidad y la aritmética con mayor precisión en la Sección 4, pero para ese fin es necesario proporcionar primero otro aspecto "modal" de GL: la semántica.

3. Posible semántica de mundos y semántica topológica

La lógica de demostrabilidad tiene una semántica de mundos posibles adecuada, al igual que muchas otras lógicas modales. Como recordatorio, un posible modelo de mundos (o modelo de Kripke) es un triple (M = / langle W, R, V / rangle), donde (W) es un conjunto no vacío de mundos posibles, (R) es una relación de accesibilidad binaria en (W), y (V) es una valoración que asigna un valor de verdad a cada variable proposicional para cada mundo en (W). El par (F = / langle W, R / rangle) se llama marco de este modelo. La noción de verdad de una fórmula (A) en un modelo (M) en un mundo (W), notación (M, w / modelos A), se define inductivamente. Repitamos solo la cláusula más interesante, la del operador de demostrabilidad (Box):

[M, w / models / Box A / text {iff para cada} w ', / text {if} wRw', / text {entonces} M, w '\ models A.)

Consulte la lógica modal de entrada para obtener más información sobre la semántica de mundos posibles en general.

3.1 Caracterización y solidez modal

La lógica modal K es válida en todos los modelos Kripke. Sin embargo, su extensión GL no lo es: necesitamos restringir la clase de modelos de mundos posibles a uno más adecuado. Digamos que una fórmula (A) es válida en el marco (F), notación (F / modelos A), iff (A) es verdadera en todos los mundos en los modelos Kripke (M) basado en (F). Resulta que el nuevo axioma (GL) de la lógica de demostrabilidad corresponde a una condición en los cuadros, como sigue:

Para todos los marcos (F = / langle W, R / rangle, F / models / Box (Box p / rightarrow p) rightarrow / Box p) iff (R) es transitivo y, por el contrario, está bien fundado.

Aquí, la transitividad es la propiedad bien conocida que para todos los mundos (w_1), (w_2), (w_3) en (W), if (w_1 Rw_2) y (w_2 Rw_3), luego (w_1 Rw_3). Por el contrario, una relación está bien fundada si no hay secuencias ascendentes infinitas, es decir, secuencias de la forma (w_1 Rw_2 Rw_3 R / ldots). Tenga en cuenta que, a la inversa, los marcos bien fundados también son irreflexivos, ya que si (wRw), esto da lugar a una secuencia ascendente infinita (wRwRwR / ldots).

El resultado de la correspondencia anterior muestra de inmediato que GL es razonablemente sólido con respecto a la clase de modelos de mundos posibles en marcos transitivos inversamente bien fundados, porque todos los axiomas y reglas de GL son válidos en dichos modelos. La pregunta es si la integridad también es válida: por ejemplo, la fórmula (Box A / rightarrow / Box / Box A), que es válida en todos los marcos transitivos, es demostrable en GL, como se mencionó en la Sección 1. Pero ¿todas las fórmulas que son válidas en todos los marcos transitivos inversamente bien fundamentados también son demostrables en GL?

3.2 Completitud modal

Sin darse cuenta de la importancia aritmética de GL, K. Segerberg demostró en 1971 que GL es de hecho completo con respecto a los marcos transitivos inversamente bien fundados; D. de Jongh y S. Kripke también probaron independientemente este resultado. Segerberg demostró que GL está completo incluso con respecto a la clase más restringida de árboles irreflexivos transitivos finitos, un hecho que luego resultó ser muy útil para la prueba de Solovay del teorema de integridad aritmética (ver Sección 4).

Los teoremas de solidez e integridad modal dan lugar inmediatamente a un procedimiento de decisión para verificar cualquier fórmula modal (A) si (A) se sigue de GL o no, mediante la búsqueda en profundidad a través de árboles transitivos irreflexivos de profundidad acotada. Mirando el procedimiento con un poco más de precisión, se puede demostrar que GL es decidible en la clase de complejidad computacional PSPACE, como las conocidas lógicas modales K, T y S4. Esto significa que hay una máquina de Turing que, dada una fórmula (A) como entrada, responde si (A) se sigue de GL o no; El tamaño de la memoria que necesita la máquina de Turing para su cálculo es solo polinomial en la longitud de (A). Se puede demostrar que el problema de decisión para GL (nuevamente, como los problemas de decisión para K, T y S4) es PSPACE- completo,en el sentido de que todos los demás problemas en PSPACE no son más difíciles que decidir si una fórmula dada es un teorema de GL. (Ver Goré y Kelly (2007) para la descripción de un probador de teoremas automatizado para GL).

Para dar más perspectiva sobre la complejidad, la clase P de funciones computables en una cantidad de tiempo polinomial en la longitud de la entrada, se incluye en PSPACE, que a su vez se incluye en la clase EXPTIME de funciones computables en tiempo exponencial (ver el entrada computabilidad y complejidad). Sigue siendo un problema abierto famoso si estas dos inclusiones son estrictas, aunque muchos teóricos de la complejidad creen que lo son. Algunas otras lógicas modales bien conocidas, como la lógica epistémica con conocimiento común, son decidibles en EXPTIME, por lo que pueden ser más complejas que GL, dependiendo de los problemas abiertos.

3.3 Fracaso de la integridad completa

Muchas lógicas modales conocidas (S) no solo están completas con respecto a una clase apropiada de marcos, sino que incluso están muy completas. Para explicar la exhaustividad completa, necesitamos la noción de derivabilidad de un conjunto de supuestos. Una fórmula (A) se deriva del conjunto de supuestos (Gamma) en una lógica modal (S), escrita como (Gamma / vdash A), si (A) está en (Gamma) o (A) se deduce de las fórmulas en (Gamma) y los axiomas de (S) mediante aplicaciones de Modus Ponens y la Regla de generalización. Aquí, la regla de generalización solo se puede aplicar a derivaciones sin supuestos (ver Hakli y Negri 2010).

Ahora una lógica modal (S) está muy completa si para todos los conjuntos (finitos o infinitos) (Gamma) y todas las fórmulas (A):

Si, en los marcos apropiados de (S), (A) es verdadero en todos los mundos en los que todas las fórmulas de (Gamma) son verdaderas, entonces (Gamma / vdash A) en la lógica (S).

Esta condición se cumple para sistemas como K, M, K4, S4 y S5. Si se restringe a conjuntos finitos (Gamma), la condición anterior corresponde a la integridad.

Sin embargo, la integridad completa no es válida para la lógica de demostrabilidad, porque la compactación semántica falla. La compacidad semántica es la propiedad que para cada conjunto infinito (Gamma) de fórmulas, Si cada subconjunto finito (Delta) de (Gamma) tiene un modelo en un marco (S) apropiado, entonces (Gamma) también tiene un modelo en un (S) apropiado -cuadro.

Como contraejemplo, tome el conjunto infinito de fórmulas

) Gamma = { Diamond p_0, / Box (p_0 / rightarrow / Diamond p_1), / Box (p_1 / rightarrow / Diamond p_2), / Box (p_2 / rightarrow / Diamond p_3), / ldots, / Box (p_n / rightarrow / Diamond p_ {n + 1}), / ldots })

Luego, para cada subconjunto finito (Delta) de (Gamma), se puede construir un modelo en un marco transitivo, inversamente bien fundado, y un mundo en el modelo donde todas las fórmulas de (Delta) son cierto. Entonces, por solidez modal, GL no prueba (bot) de (Delta) para ningún finito (Delta / subseteq / Gamma), y un GL fortiori no prueba (bot) de (Gamma), ya que cualquier prueba GL es finita. Por otro lado, es fácil ver que no hay un modelo en un marco transitivo, a la inversa, bien fundado, donde en cualquier mundo, se mantengan todas las fórmulas de (Gamma). Por lo tanto, (bot) se sigue semánticamente de (Gamma), pero no es demostrable en GL, lo que contradice la condición de integridad completa.

3.4 Semántica topológica para la lógica de demostrabilidad

Como alternativa a la semántica de mundos posibles, muchas lógicas modales pueden recibir semántica topológica. Claramente, las proposiciones pueden interpretarse como subconjuntos de un espacio topológico. También es fácil ver que el conectivo proposicional (wedge) corresponde a la operación teórica de conjuntos (cap), mientras que (vee) corresponde a (cup), (neg) corresponde al complemento teórico de conjuntos, y (rightarrow) corresponde a (subseteq). Las lógicas modales que contienen el axioma de reflexión (Box A / rightarrow A) también disfrutan de una interpretación particularmente natural de los operadores modales. Para estas lógicas, (Diamond) corresponde al operador de cierre en un espacio topológico, mientras que (Box) corresponde al interior. Para ver por qué estas interpretaciones son apropiadas,Observe que el axioma de reflexión corresponde al hecho de que cada conjunto está incluido en su cierre y cada conjunto incluye su interior.

Sin embargo, la lógica de demostrabilidad no prueba la reflexión, ya que la instanciación (Box / bot / rightarrow / bot) de reflexión conduciría a una contradicción con el axioma (GL).

La lógica de demostrabilidad, por lo tanto, necesita un enfoque diferente. Basado en una sugerencia de J. McKinsey y A. Tarski (1944), L. Esakia (1981, 2003) investigó la interpretación de (Diamond) como el operador de conjunto derivado (d), que mapea un conjunto (B) al conjunto de sus puntos límite (d (B)). Para explicar las consecuencias de esta interpretación de (Diamond), necesitamos dos definiciones más, a saber, los conceptos denso en sí mismo y disperso. Un subconjunto (B) de un espacio topológico se llama denso en sí mismo (B / subseteq d (B)). Un espacio topológico se denomina disperso si no tiene un subconjunto no vacío que sea denso en sí mismo. Los ordinales en su topología de intervalo forman ejemplos de espacios dispersos. Esakia (1981) demostró una correspondencia importante: demostró que un espacio topológico satisface el axioma GL si y solo si el espacio está disperso. Esta correspondencia pronto condujo al resultado, encontrado independientemente por Abashidze (1985) y Blass (1990), de que la lógica de demostrabilidad es completa con respecto a cualquier ordinal (ge / omega ^ / omega).

En los últimos años, la semántica topológica para la lógica de demostrabilidad ha experimentado un verdadero renacimiento, especialmente en el estudio de la lógica de comprobabilidad bimodal GLB de Japaridze, una extensión de GL (Japaridze 1986). La lógica GLB resulta ser modalmente incompleta con respecto a la semántica de sus mundos posibles, en el sentido de que no corresponde a ninguna clase de tramas. Esta característica coloca el GLB bimodal en marcado contraste con el GL unimodal, que corresponde a la clase de árboles finitos transitivos irreflexivos, como se mencionó anteriormente. Beklemishev y col. (2009) mostraron que GLB es, sin embargo, completo con respecto a su semántica topológica (ver también Beklemishev 2009, Icard 2011). Se pueden encontrar reverberaciones intrigantes de la correspondencia de Esakia entre GL y espacios topológicos dispersos en estudios topológicos recientes de lógicas espaciales y epistémicas (ver Aiello et al.2007). (Consulte la Sección 5.4 para obtener más información sobre GLB).

4. Lógica de demostrabilidad y aritmética de Peano

Desde el momento en que se formuló el GL, los investigadores se preguntaron si era adecuado para teorías formales como la Aritmética de Peano (PA): ¿GL prueba todo sobre la noción de demostrabilidad que puede expresarse en un lenguaje modal proposicional y puede probarse en Aritmética de Peano, o ¿Deberían agregarse más principios a GL? Para hacer más precisa esta noción de adecuación, definimos una realización (a veces llamada traducción o interpretación) como una función f que asigna a cada átomo proposicional de lógica modal una oración de aritmética, donde

  • (f (bot) = / bot;)
  • (f) respeta las conexiones lógicas, por ejemplo, (f (B / rightarrow C) = (f (B) rightarrow f (C));) y
  • (Box) se traduce como el predicado de probabilidad (Prov), entonces (f (Box B) = / Prov (ulcorner f (B) urcorner).)

4.1 Solidez aritmética

A principios de la década de 1970, ya estaba claro que GL es aritméticamente sólido con respecto a PA, formalmente:

) text {If} GL / vdash A, / text {entonces para todas las realizaciones} f, / PA / vdash f (A).)

Para dar una idea de la metamatemática, bosquejemos la prueba de solidez.

Bosquejo de prueba de solidez aritmética. De hecho, PA demuestra la realización de tautologías proposicionales, y la demostrabilidad del Axioma de distribución de GL se traduce en

) PA / vdash / Prov (ulcorner A / rightarrow B / urcorner) rightarrow (Prov (ulcorner A / urcorner) rightarrow / Prov (ulcorner B / urcorner)))

para todas las fórmulas A y B, que es solo la segunda condición de derivabilidad de Löb (ver Sección 1). Además, PA obedece a Modus Ponens, así como a la traducción de la Regla de Generalización:

) text {If} PA / vdash A, / text {then} PA / vdash / Prov (ulcorner A / urcorner),)

que es solo la primera condición de derivabilidad de Löb. Finalmente, la traducción del axioma principal (GL) es demostrable en PA:

) PA / vdash / Prov (ulcorner / Prov (ulcorner A / urcorner) rightarrow A / urcorner) rightarrow / Prov (ulcorner A / urcorner).)

Esta es exactamente la versión formalizada del teorema de Löb mencionado en la Sección 1.

Demos un bosquejo de la prueba del teorema de Löb en sí mismo a partir de sus condiciones de derivabilidad (la prueba de la versión formalizada es similar). La prueba se basa en el lema de diagonalización de Gödel, que dice que para cualquier fórmula aritmética (C (x)) hay una fórmula aritmética (B) tal que

) PA / vdash B / leftrightarrow C (ulcorner B / urcorner).)

En palabras, la fórmula (B) dice "Tengo propiedad (C)".

Prueba de Löb Es teorema:. Supongamos que (PA / vdash / Prov (ulcorner A / urcorner) rightarrow A); necesitamos mostrar que (PA / vdash A). Por el lema de diagonalización, hay una fórmula (B) tal que

) PA / vdash B / leftrightarrow (Prov (ulcorner B / urcorner) rightarrow A).)

De esto se desprende de las condiciones de derivabilidad primera y segunda de Löb más algún razonamiento proposicional que

) PA / vdash / Prov (ulcorner B / urcorner) leftrightarrow / Prov (ulcorner / Prov (ulcorner B / urcorner) rightarrow A / urcorner).)

Así, nuevamente por la segunda condición de Löb,) PA / vdash / Prov (ulcorner B / urcorner) rightarrow (Prov (ulcorner / Prov (ulcorner B / urcorner) urcorner) rightarrow / Prov (ulcorner A / urcorner)).)

Por otro lado, la tercera condición de Löb da

) PA / vdash / Prov (ulcorner B / urcorner) rightarrow / Prov (ulcorner / Prov (ulcorner B / urcorner) urcorner),)

así

) PA / vdash / Prov (ulcorner B / urcorner) rightarrow / Prov (ulcorner A / urcorner).)

Junto con la suposición de que (PA / vdash / Prov (ulcorner A / urcorner) rightarrow A), esto da

) PA / vdash / Prov (ulcorner B / urcorner) rightarrow A.)

Finalmente, la ecuación producida por el lema de diagonalización implica que (PA / vdash B), entonces (PA / vdash / Prov (ulcorner B / urcorner)), así

) PA / vdash A,)

como se desee.

Tenga en cuenta que sustituyendo (bot) por (A) en el teorema de Löb, derivamos que (PA / vdash / neg \, / Prov (ulcorner / bot / urcorner)) implica (PA / vdash / bot), que es solo la contraposición del segundo teorema de incompletitud de Gödel.

4.2 Integridad aritmética

El resultado histórico en la lógica de demostrabilidad es el teorema de integridad aritmética de R. Solovay de 1976, que muestra que GL es realmente adecuado para la aritmética de Peano:

) GL / vdash A / text {si y solo si para todas las realizaciones} f, / PA / vdash f (A).)

Este teorema dice esencialmente que la lógica modal GL captura todo lo que la aritmética de Peano puede decir sinceramente en términos modales sobre su propio predicado de demostrabilidad. La dirección de izquierda a derecha, la solidez aritmética de GL, se discutió anteriormente. Solovay se propuso probar la otra dirección, mucho más difícil, por contraposición. Su prueba se basa en intrincadas técnicas autorreferenciales, y aquí solo se puede dar un pequeño vistazo.

El teorema de integridad modal de Segerberg fue un primer paso importante en la prueba de Solovay de la integridad aritmética de GL con respecto a la aritmética de Peano. Suponga que GL no prueba la fórmula modal (A). Luego, por completitud modal, hay un árbol finito transitivo irreflexivo tal que (A) es falso en la raíz de ese árbol. Ahora Solovay ideó una forma ingeniosa de simular un árbol tan finito en el lenguaje de la aritmética de Peano. Así encontró una realización (f) de fórmulas modales a oraciones de aritmética, de modo que la Aritmética de Peano no prueba (f (A)).

El teorema de integridad de Solovay proporciona una forma alternativa de construir muchas oraciones aritméticas que no son demostrables en la aritmética de Peano. Por ejemplo, es fácil hacer un posible modelo de mundos para mostrar que GL no prueba (Box p / vee / Box / neg \, p), por lo que según el teorema de Solovay, hay una oración aritmética (f (p)) tal que la aritmética de Peano no pruebe (Prov (ulcorner f (p) urcorner) vee / Prov (ulcorner / neg \, f (p) urcorner)). En particular, esto implica que ni (f (p)) ni (neg \, f (p)) es demostrable en Aritmética de Peano; Supongamos, por el contrario, que (PA / vdash f (p)), luego por la primera condición y lógica proposicional de Löb, (PA / vdash / Prov (ulcorner f (p) urcorner) vee / Prov (ulcorner / neg \, f (p) urcorner)), lo que lleva a una contradicción, y de manera similar si se supone que (PA / vdash / neg \, f (p)).

El teorema de Solovay es tan significativo porque muestra que un fragmento interesante de una teoría formal indecidible como la Aritmética de Peano, es decir, aquella que la aritmética puede expresar en términos proposicionales sobre su propio predicado de demostrabilidad, puede estudiarse por medio de una lógica modal decidible, GL, con una semántica visible de mundos posibles.

5. El alcance de la lógica de demostrabilidad

En esta sección, se discuten algunas tendencias recientes en la investigación sobre la lógica de demostrabilidad. Un aspecto importante se refiere a los límites en el alcance de GL, donde la pregunta principal es, ¿para qué teorías formales, además de la aritmética de Peano, es GL la lógica de demostrabilidad proposicional apropiada? A continuación, discutimos algunas generalizaciones de la lógica de demostrabilidad proposicional en lenguajes modales más expresivos.

5.1 Límites

En los últimos años, los lógicos han investigado muchos otros sistemas de aritmética que son más débiles que la aritmética de Peano. A menudo, estos lógicos se inspiraron en los problemas de computabilidad, por ejemplo, el estudio de funciones computables en tiempo polinómico. Han dado una respuesta parcial a la pregunta: "¿Para qué teorías de la aritmética sigue siendo válido el teorema de integridad aritmética de Solovay (con respecto al predicado de demostrabilidad apropiado)?" Para discutir esta pregunta, se necesitan dos conceptos. (Delta_0): las fórmulas son fórmulas aritméticas en las que todos los cuantificadores están limitados por un término, por ejemplo

) forall y / le / bs / bs 0 \: / forall z / le y \: / forall x / le y + z \: (x + y / le (y + (y + z))),)

donde (bs) es el operador sucesor ("(+ 1)"). La teoría aritmética (I / Delta_0) (donde significa "inducción"), es similar a la Aritmética de Peano, excepto que permite menos inducción: el esquema de inducción

[A (0) wedge / forall x \, (A (x) rightarrow A (bs x)) rightarrow / forall x \, A (x))

está restringido a (Delta_0) - fórmulas (A).

Como señalaron De Jongh y otros (1991), la integridad aritmética ciertamente es válida para las teorías (T) que satisfacen las siguientes dos condiciones:

  1. (T) prueba la inducción para (Delta_0) - fórmulas, y (T) prueba EXP, la fórmula que expresa que para todo (x), su poder (2 ^ x) existe. En notación más estándar: (T) extiende (I / Delta_0) + EXP;
  2. (T) no prueba ninguna oración falsa de la forma (exist x \, A (x)), con (A (x)) a (Delta_0) - fórmula.

Para tales teorías, la solidez aritmética y la integridad de GL Hold, siempre que (Box) se traduzca en (Prov_T), un predicado de demostrabilidad natural con respecto a una axiomatización suficientemente simple de (T). Así, para las oraciones modales (A):

) GL / vdash A / text {si y solo si para todas las realizaciones} f, T / vdash f (A).)

Todavía no está claro si la Condición 1 otorga un límite inferior en el alcance de la lógica de demostrabilidad. Por ejemplo, todavía es una pregunta abierta si GL es la lógica de demostrabilidad de (I / Delta_0 + / Omega_1), una teoría que es algo más débil que (I / Delta_0) + EXP en ese (Omega_1) es el axioma que afirma que para todo (x), su poder (x ^ { log (x)}) existe. La lógica de probabilidad GL es aritméticamente sólida con respecto a (I / Delta_0 + / Omega_1), pero a excepción de algunos resultados parciales de Berarducci y Verbrugge (1993), proporcionando realizaciones aritméticas consistentes con (I / Delta_0 + / Omega_1) para un clase de oraciones consistentes con GL, la pregunta permanece abierta. Su respuesta puede depender de problemas abiertos en la teoría de la complejidad computacional.

El resultado anterior de De Jongh et al. muestra una fuerte característica de la lógica de demostrabilidad: para muchas teorías aritméticas diferentes, GL captura exactamente lo que esas teorías dicen sobre sus propios predicados de demostrabilidad. Al mismo tiempo, esto es una debilidad. Por ejemplo, la lógica de comprobabilidad proposicional no apunta a ninguna diferencia entre esas teorías que son finitamente axiomatizables y las que no lo son.

5.2 Lógica de interpretabilidad

Para poder hablar en un lenguaje modal sobre distinciones importantes entre teorías, los investigadores han extendido la lógica de demostrabilidad de muchas maneras diferentes. Mencionemos algunos. Una extensión es agregar una modalidad binaria (interprets), donde para una teoría aritmética dada (T), la oración modal (A / interpreta B) significa (T + B) es interpretable en (T + A)”(Švejdar, 1983). De Jongh y Veltman (1990) investigaron la semántica modal para varias lógicas de interpretabilidad, mientras que De Jongh y Visser (1991) demostraron la propiedad explícita de punto fijo para las más importantes. Visser caracterizó la lógica de interpretabilidad de las teorías axiomatizadas finitamente más comunes, y Berarducci y Shavrukov caracterizaron independientemente la de PA, que no es axiomatizable finitamente. Parece que de hecho,La lógica de interpretabilidad de las teorías finitamente axiomatizables es diferente de la lógica de interpretabilidad de Peano Arithmetic (véase Montagna 1987; Visser 1990, 1998; Berarducci 1990, Shavrukov 1988; Joosten y Visser 2000).

5.3 Cuantificadores proposicionales

Otra forma de extender el marco de la lógica de demostrabilidad proposicional es agregar cuantificadores proposicionales, para que uno pueda expresar principios como el de Goldfarb:

) forall p \, / forall q \, / exist r \: / Box ((Box p / vee / Box q) leftrightarrow / Box r),)

diciendo que para cualquiera de las dos oraciones hay una tercera oración que es demostrable si y solo si cualquiera de las dos primeras oraciones es demostrable. Este principio es demostrable en la aritmética de Peano (ver, por ejemplo, Artemov y Beklemishev 1993). El conjunto de oraciones de GL con cuantificadores proposicionales que es válido aritméticamente resulta indecidible (Shavrukov 1997).

5.4 Lógicas de demostrabilidad bimodal y polimodal de Japaridze

La lógica bimodal GLB de Japaridze (1988) tiene dos operadores de demostrabilidad similares a (Box), denotados por ([0]) y ([1]), con sus operadores duales (Diamond) (langle 0 / rangle) y (langle 1 / rangle), respectivamente. En la interpretación de Japaridze, uno puede pensar que ([0]) representa el predicado de demostrabilidad estándar en Aritmética de Peano. Por otro lado, ([1]) corresponde a un predicado de demostrabilidad más fuerte, a saber, (omega) - provabilidad.

Definamos los conceptos que se necesitan para comprender esta interpretación prevista de GLB. Una teoría aritmética (T) se define como (omega) - consistente si y solo si para todas las fórmulas A con variable libre (x), (T / vdash / neg \, A (I_n)) para todos (n) implica que (T / not / vdash / exist x x, A (x)); aquí, (I_n) es el número de (n), es decir, el término (bs / bs / ldots / bs 0) con (n) ocurrencias del operador sucesor (bs) La aritmética de Peano (PA) es el ejemplo más conocido de una teoría consistente de (omega) (véanse también los teoremas de incompletitud de Gödel). Ahora dejemos que PA (^ +) sea la teoría aritmética cuyos axiomas son los de PA junto con todas las oraciones (forall x \, / neg \, A (x)) tal que para cada (n), PA (vdash / neg \, A (I_n)). Ahora (omega) - la demostrabilidad es simplemente la demostrabilidad en PA (^ +),entonces es el doble de (omega) - consistencia.

La lógica de comprobabilidad bimodal de Japaridze GLB puede ser axiomatizada por los axiomas y las reglas de GL (ver Sección 2), formulados por separado para [0] y [1]. Además, GLB tiene dos axiomas mixtos, a saber:) tag {Monotonicity} [0] A / rightarrow [1] A)) tag {(Pi ^ 0_1) - completeness} langle 0 / rangle A / rightarrow [1] langle 0 / rangle A) La lógica de Japaridze es decidible y tiene una semántica razonable de Kripke, y es aritméticamente sólida y completa con respecto a la Aritmética de Peano (Japaridze 1988, Boolos 1993).

Un análogo polimodal del GLB de Japaridze, llamado GLP, ha recibido mucha atención en los últimos años. GLP tiene infinitos operadores de probabilidad como (Box), indicados por cajas ([n]) para cada número natural (n), con sus operadores / \ / \ Diamond / como duales / langle n / rangle). Nuevamente, uno puede pensar que ([0]) representa el predicado de demostrabilidad estándar en Aritmética de Peano, (langle 1 / rangle) para (omega) - demostrabilidad, etcétera. GLP se ha axiomatizado a partir de los axiomas y las reglas de GL (ver Sección 2), formulados por separado para cada ([n]). Además, GLP tiene tres esquemas de axiomas mixtos, a saber, según lo formulado por Beklemishev (2010): [m] A / rightarrow [n] A, / mbox {for} m / leq n)) langle k / rangle A / rightarrow [n] langle k / rangle A, / mbox {for} k / lt n) [m] A / rightarrow [n] [m] A, / mbox {for} m / leq n)

Recientemente, GLP ha sido dotado de una semántica de Kripke con respecto a la cual está completo, y también se ha demostrado que es aritméticamente completo con respecto a la Aritmética de Peano (ver Beklemishev 2010a, 2011a). Al igual que para GL, el problema de decisión para GLP es PSPACE-complete (Shapirovsky 2008), mientras que su fragmento cerrado es decidible en tiempo polinómico (Pakhomov 2014).

En los últimos años, se han demostrado una serie de resultados sobre el GLP de la lógica polimodal de predicados de demostrabilidad fuertes. Aquí siguen algunos temas particularmente fructíferos:

  • el fragmento cerrado de BPL (ver Ignatiev 1993; Beklemishev, Joosten y Vervoort 2005);
  • GLP y ordinales teóricos de prueba (Beklemishev 2004);
  • Teoremas de interpolación para GLP (ver Beklemishev 2010b, Shamkanov 2011);
  • La relación entre la semántica topológica y la teoría de conjuntos, entre otros axiomas cardinales grandes particulares y la reflexión estacionaria (ver Beklemishev 2011b; Beklemishev y Gabelaia 2013, 2014; Fernández-Duque 2014).

5.5 Lógica de demostrabilidad de predicado

Finalmente, uno puede, por supuesto, estudiar la lógica de demostrabilidad de predicados. El lenguaje es el de la lógica de predicados sin símbolos de función, junto con el operador (Box). Aquí, la situación se vuelve mucho más compleja que en el caso de la lógica de demostrabilidad proposicional. Para empezar, la versión cuantificada directa de GL no tiene la propiedad de punto fijo, no está completa con respecto a ninguna clase de marcos de Kripke, y no está completa aritméticamente con respecto a la aritmética de Peano (Montagna, 1984). Entonces surge la pregunta: ¿Existe alguna lógica de demostrabilidad de predicado bien axiomatizada que sea adecuada, que demuestre exactamente los principios válidos de demostrabilidad? La respuesta es, lamentablemente, un rotundo no:Vardanyan (1986) ha demostrado sobre la base de las ideas de Artemov (1985a) que el conjunto de oraciones de lógica de demostrabilidad de predicados, cuyas realizaciones son demostrables en PA, ni siquiera es recursivamente enumerable sino (Pi ^ 0_2) - completo, entonces no tiene axiomatización razonable. Visser y De Jonge (2006) mostraron que no hay escapatoria del teorema de Vardanyan al demostrar una generalización: para una amplia gama de teorías aritméticas (T), el conjunto de oraciones de lógica de demostrabilidad de predicados, cuyas realizaciones son demostrables en (T) resulta ser (Pi ^ 0_2) - completo también. Para una amplia gama de teorías aritméticas (T), el conjunto de oraciones de lógica de demostrabilidad de predicados cuyas realizaciones son demostrables en (T) resulta ser (Pi ^ 0_2) - completo también. Para una amplia gama de teorías aritméticas (T), el conjunto de oraciones de lógica de demostrabilidad de predicados cuyas realizaciones son demostrables en (T) resulta ser (Pi ^ 0_2) - completo también.

5.6 Otras generalizaciones

Quedan fuera de la discusión anterior hay muchas otras líneas importantes de investigación en lógica de demostrabilidad y sus extensiones. El lector interesado señala las siguientes áreas:

  • la lógica de demostrabilidad de la aritmética intuicionista (ver Troelstra 1973; Visser 1982, 1999; Iemhoff 2000, 2001, 2003; Visser 2002, 2008);
  • clasificación de las lógicas de demostrabilidad (ver Visser 1980, Artemov 1985b, Beklemishev 1989, Beklemishev et al. 1999);
  • Pedidos de Rosser y aceleración de pruebas (ver Guaspari y Solovay 1979, Švejdar 1983, Montagna 1992);
  • varios tipos de lógicas de comprobabilidad bimodal con operadores de demostrabilidad para diferentes teorías (ver Carlson 1986; Smoryński 1985; Beklemishev 1994, 1996);
  • lógicas de comprobabilidad para la comprobabilidad estándar combinada con predicados de probabilidad inusuales que enumeran externamente PA, como los predicados de probabilidad de Feferman y Parikh y los predicados de probabilidad lenta (ver Montagna 1978; Visser 1989; Shavrukov 1994; Lindström 1994, 2006; Henk y Pakhomov 2016 (Otros recursos de Internet));
  • la lógica de las pruebas explícitas (ver Artemov 1994, 2001; Artemov y Montagna 1994; Artemov e Iemhoff 2007);
  • aplicaciones de la lógica de demostrabilidad en la teoría de la prueba (ver Beklemishev 1999, 2004, 2005, 2006);
  • lógica de demostrabilidad positiva y cálculo de reflexión (ver Beklemishev 2012, 2014; Dashkov 2012);
  • generalizaciones de la lógica de comprobabilidad polimodal GLP, a saber, lógicas de comprobabilidad con muchas modalidades de manera transfinita (ver Beklemishev et al. 2014; Fernández-Duque y Joosten 2013a, 2013b, 2013 (Otros recursos de Internet), 2014);
  • relaciones entre la lógica de demostrabilidad y el cálculo de (mu) (véase van Benthem 2006, Visser 2005, Alberucci y Facchini 2009); y
  • álgebras de probabilidad, también llamadas álgebras diagonalizables o álgebras de Magari (ver Magari 1975a, 1975b; Montagna 1979, 1980a, 1980b; Shavrukov 1993a, 1993b, 1997; Zambella 1994; para resultados recientes sobre sus teorías elementales, ver Pakhomov 2012, 2014 (Other Internet Recursos), 2015 (Otros recursos de Internet)).

Para el lector que quisiera contribuir al área de la lógica de demostrabilidad y sus generalizaciones, Beklemishev y Visser (2006) han propuesto una lista anotada de intrigantes problemas abiertos.

6. Significado filosófico

Aunque la lógica de demostrabilidad proposicional es una lógica modal con una especie de operador de "necesidad", resiste la crítica controvertida de Quine (1976) de las nociones modales como ininteligibles, ya debido a su interpretación aritmética clara e inequívoca. Por ejemplo, a diferencia de muchas otras lógicas modales, las fórmulas con modalidades anidadas como (Box / Diamond p / rightarrow / Box / bot) no son problemáticas, ni existen disputas sobre cuáles deberían ser tautologías. De hecho, la lógica de demostrabilidad incorpora todos los desiderata que Quine (1953) estableció para los tratamientos sintácticos de modalidad.

Las flechas principales de Quine apuntaban hacia lógicas de predicados modales, especialmente la construcción de oraciones que contienen operadores modales bajo el alcance de cuantificadores ("cuantificación en"). Sin embargo, en la lógica de demostrabilidad de predicados, donde los cuantificadores varían sobre los números naturales, tanto las modalidades de dicto como las de re tienen interpretaciones directas, al contrario del caso de otras lógicas modales (ver la nota sobre la distinción de dicto / de re). Por ejemplo, fórmulas como

) forall x \, / Box \, / exist y \, (y = x))

no son para nada problemáticos. Si el número (n) se asigna a (x), entonces (Box \, / exist y \, (y = x)) es verdadero con respecto a esta asignación si la oración (existe y \, (y = I_n)) es demostrable en Aritmética de Peano; aquí, (I_n) es el número de (n), es decir, el término (bs / bs / ldots / bs 0) con (n) ocurrencias del operador sucesor (bs) Esta oración es verdadera para todos (n) en el modelo estándar de los números naturales, y (forall x \, / Box \, / exist y \, (y = x)) es incluso demostrable en Aritmética de Peano.

Por cierto, la fórmula de Barcan

) forall x \, / Box \, A (x) rightarrow / Box \, / forall x \, A (x))

no es cierto para los enteros, y mucho menos demostrable (por ejemplo, tome para (A (x)) la fórmula "(x) no codifica una prueba de (bot)"). Es inverso

) Box \, / forall x \, A (x) rightarrow / forall x \, / Box \, A (x))

Por otro lado, es demostrable en Peano Aritmética para cualquier fórmula (A).

La lógica de demostrabilidad tiene principios muy diferentes de otras lógicas modales, incluso aquellas con un propósito aparentemente similar. Por ejemplo, mientras que la lógica de la capacidad de prueba captura la capacidad de prueba en las teorías formales de la aritmética, la lógica epistémica se esfuerza por describir el conocimiento, que podría verse como un tipo de capacidad de prueba informal. En muchas versiones de la lógica epistémica, uno de los principios más importantes es el axioma de la verdad (5):

) mbox {S5} vdash / Box A / rightarrow A, (text {si se sabe} A, / text {then} A / text {es verdadero}).)

El principio análogo claramente no es válido para GL: después de todo,) text {if} GL / vdash / Box A / rightarrow A, / text {then} GL / vdash A.)

Por lo tanto, parece equivocado comparar la fuerza de ambas nociones o combinarlas en un sistema modal. Quizás la comprobabilidad formal es, en cierto sentido, una noción más fuerte que la comprobabilidad informal, pero definitivamente esta no es una verdad o validez aritmética, ni es la otra dirección. Las discusiones sobre las consecuencias de los teoremas de incompletitud de Gödel a veces implican confusión en torno a la noción de demostrabilidad, dando lugar a afirmaciones de que los humanos podrían vencer a los sistemas formales en teoremas de "conocimiento" (ver Davis (1990, 1993) para una buena discusión de tales afirmaciones).

Con todo, la demostrabilidad formal es un concepto definido con precisión, mucho más que la verdad y el conocimiento. Por lo tanto, la autorreferencia dentro del alcance de la demostrabilidad no conduce a paradojas semánticas como el Mentiroso. En cambio, ha llevado a algunos de los resultados más importantes sobre las matemáticas, como los teoremas de incompletitud de Gödel.

Bibliografía

Referencias generales sobre lógica de demostrabilidad

  • Artemov, SN, 2006, "Modal Logic in Mathematics", en P. Blackburn, et al. (eds.), Handbook of Modal Logic, Amsterdam: Elsevier, págs. 927–970.
  • Artemov, SN y LD Beklemishev, 2004, "Provability Logic", en Handbook of Philosophical Logic, Segunda edición, D. Gabbay y F. Guenthner, eds., Volumen 13, Dordrecht: Kluwer, págs. 229–403.
  • Boolos, G., 1979, The Unprovability of Consistency: An Essay in Modal Logic, Cambridge: Cambridge University Press.
  • –––, 1993, The Logic of Provability, Nueva York y Cambridge: Cambridge University Press.
  • de Jongh, DHJ y G. Japaridze, 1998, "The Logic of Provability", en Handbook of Proof Theory, Buss, SR (ed.), Amsterdam: North-Holland, pp. 475-546.
  • Lindström, P., 1996, "Provability Logic-A Short Introduction", Theoria, 52 (1–2): 19–61.
  • Segerberg, K., 1971, An Essay in Classical Modal Logic, Uppsala: Filosofiska Föreningen och Filosofiska Institutionen vid Uppsala Universitet.
  • Švejdar, V., 2000, “Sobre la lógica de la comprobabilidad”, Nordic Journal of Philosophy, 4: 95–116.
  • Smoryński, C., 1985, Self-Reference and Modal Logic, Nueva York: Springer-Verlag.
  • Verbrugge, R. 1996, "Provability" en The Encyclopedia of Philosophy (Supplement), DM Borchert (ed.), Nueva York: Simon and Schuster MacMillan, pp. 476–478.
  • Visser, A., 1998, "Provability Logic", en Routledge Encyclopedia of Philosophy, W. Craig (ed.), Londres: Routledge, pp. 793–797.

Historia

  • van Benthem, JFAK, 1978, "Cuatro paradojas", Journal of Philosophical Logic, 7 (1): 49–72.
  • Boolos, G. y G. Sambin, 1991, "Probabilidad: el surgimiento de una modalidad matemática", Studia Logica, 50 (1): 1–23.
  • Gödel, K., 1933, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines Mathematischen Kolloquiums, 4: 39–40; traducción "Una interpretación del cálculo proposicional intuitivo", en K. Gödel, Collected Works, S. Feferman et al. (eds.), Oxford y Nueva York: Oxford University Press, Volumen 1, 1986, pp. 300–302.
  • –––, 1931, “Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38: 173–198.
  • Halbach, V. y A. Visser, 2014, "The Henkin Sentence", en M. Mazano, I. Sain y E. Alonso (eds.), The Life and Work of Leon Henkin: Ensayos sobre sus contribuciones, Dordrecht: Springer International Publishing, págs. 249–263.
  • Henkin, L., 1952, "Un problema relacionado con la posibilidad de prueba", Journal of Symbolic Logic, 17: 160.
  • –––., 1954, “Review of G. Kreisel: On a Problem of Leon Henkin's”, Journal of Symbolic Logic, 19 (3): 219–220.
  • Hilbert, D. y P. Bernays, 1939, Grundlagen der Mathematik, volumen 2, Berlín / Heidelberg / Nueva York: Springer-Verlag.
  • Kreisel, G., 1953, "Sobre un problema de Leon Henkin", Indagationes Mathematicae, 15: 405–406.
  • Lewis, CI, 1912, "Implicación y el álgebra de la lógica", Mind, 21: 522–531.
  • Löb, MH, 1955, "Solución de un problema de Leon Henkin", Journal of Symbolic Logic, 20: 115-118.
  • Macintyre, AJ y H. Simmons, 1973, "Técnica de Diagonalización de Gödel y propiedades relacionadas de las teorías", Colloquium Mathematicum, 28: 165–180.
  • Magari, R., 1975a, "The Diagonalizable Algebras", Bollettino della Unione Mathematica Italiana, 12: 117–125.
  • –––, 1975b, “Representación y teoría de la dualidad para álgebras diagonalizables”, Studia Logica, 34 (4): 305–313.
  • Smiley, TJ, 1963, "La base lógica de la ética", Acta Philosophica Fennica, 16: 237–246.
  • Smoryński, C., 1991, "The Development of Self-reference: Löb's Theorem", en T. Drucker (ed.), Perspectives on the History of Mathematical Logic, Basilea: Birkhäuser, pp. 110-133.

Eliminación de corte para lógica de demostrabilidad

  • Goré, R. y R. Ramanayake, 2008, "Valentini's Cut-Elimination for Provability Logic Resolved", en Advances in Modal Logic Volume 7, C. Areces y R. Goldblatt (eds.), Londres: Publicaciones universitarias, págs. 67 -86.
  • Negri, S., 2005, "Proof Analysis in Modal Logic", Journal of Philosophical Logic, 50: 507–544.
  • Negri, S., 2014, “Pruebas y contramodelos en lógica no clásica”, Logica Universalis, 8 (1): 25–60.
  • Poggiolesi, F., 2009, "Un cálculo secuencial puramente sintáctico y sin cortes para la lógica modal de demostrabilidad", The Review of Symbolic Logic, 2 (4): 593–611.
  • Rautenberg, W., 1983, "Modal Tableau Calculi and Interpolation", Journal of Philosophical Logic, 12 (4): 403-423.
  • Sambin, G. y S. Valentini, 1982, “La lógica modal de la comprobabilidad. El enfoque secuencial”, Journal of Philosophical Logic, 11 (3): 311–342.
  • Shamkanov, DS, 2011, "Propiedades de interpolación para las lógicas de demostrabilidad GL y GLP", Actas del Instituto Steklov de Matemáticas, 274 (1): 303–316.
  • –––, 2014, “Pruebas circulares para la lógica de demostrabilidad de Gödel-Löb”, Mathematical Notes, 96 (4): 575–585.
  • Smoryński, C., 1978, "Teorema de Beth y oraciones autorreferenciales", Studies in Logic and the Foundations of Mathematics, 96: 253–261.
  • Valentini, S., 1983, "La lógica modal de comprobabilidad: eliminación de cortes", Journal of Philosophical Logic, 12: 471–476.

El teorema del punto fijo

  • de Jongh, DHJ y F. Montagna, 1988, “Puntos fijos comprobables”, Mathematical Logic Quarterly, 34 (3): 229–250.
  • Lindström, P., 2006, "Nota sobre algunas construcciones de puntos fijos en la lógica de demostrabilidad", Journal of Philosophical Logic, 35 (3): 225–230.
  • Reidhaar-Olson, L., 1990, "Una nueva prueba del teorema de punto fijo de la lógica de demostrabilidad", Notre Dame Journal of Formal Logic, 31 (1): 37–43.
  • Sambin, G., 1976, "Un teorema efectivo de punto fijo en álgebras intuitivas y diagonales (La algebraización de las teorías que expresan Theor, IX)", Studia Logica 35: 345-361.
  • Sambin, G. y S. Valentini, 1982, “La lógica modal de la comprobabilidad. El enfoque secuencial”, Journal of Philosophical Logic, 11 (3): 311–342.

Posible semántica de mundos y semántica topológica

  • Abashidze, M., 1985, "Ordinal Completeness of the Gödel-Löb Modal System" (en ruso) en Intensional Logics and the Logical Structure of Theories, Tbilisi: Metsniereba, págs. 49-73.
  • Aiello, M., I. Pratt-Hartmann y J. van Benthem (eds.), 2007, Handbook of Spatial Logics, Berlín: Springer-Verlag.
  • Beklemishev, LD 2009, “Completitud ordinal de la lógica de comprobabilidad bimodal GLB”, en el Simposio internacional de Tbilisi sobre lógica, lenguaje y computación, Berlín: Springer-Verlag, págs. 1–15.
  • Beklemishev, LD, G. Bezhanishvili y T. Icard, 2009, "On Topological Models of GLP", en R. Schindler (ed.), Formas de la teoría de la prueba (Ontos Mathematical Logic: Volumen 2), Frankfurt: Ontos Verlag, pp. 133-153.
  • Blass, A., 1990, "Infinitary Combinatorics and Modal Logic", Journal of Symbolic Logic, 55 (2): 761-778.
  • Esakia, L., 1981, "Construcciones diagonales, fórmula de Löb y espacios dispersos de Cantor" (en ruso), en Studies in Logic and Semantics, Z. Mikeladze (ed.), Tbilisi: Metsniereba, págs. 128–143.
  • –––, 2003, “Lógica intuitiva y modalidad vía topología”, Annals of Pure and Applied Logic, 127: 155–170.
  • Goré, R., 2009, "Teoría de la prueba de comprobación de máquinas: una aplicación de la lógica a la lógica", en ICLA '09: Actas de la 3a Conferencia india sobre lógica y sus aplicaciones, Berlín: Springer-Verlag, págs. 23–35.
  • Goré, R. y J. Kelly, 2007, "Búsqueda de pruebas automatizada en la lógica de probabilidad de Gödel-Löb", British Logic Colloquium 2007, disponible en https://www.dcs.bbk.ac.uk/~roman/blc/.
  • Hakli, R. y S. Negri, 2012, "¿Falla el teorema de la deducción para la lógica modal?" Synthese 187 (3): 849–867.
  • Icard, TF III, 2011, "Un estudio topológico del fragmento cerrado de BPL", Journal of Logic and Computation, 21 (4): 683-696; publicado por primera vez en línea en 2009, doi: 10.1093 / logcom / exp043
  • Japaridze, GK, 1986, Los medios lógicos modales de investigación de demostrabilidad, Tesis en filosofía (en ruso), Moscú.
  • McKinsey, JCC y A. Tarski, 1944, "El álgebra de la topología", Annals of Mathematics, 45: 141–191.

Probabilidad y Aritmética de Peano

  • Davis, M., 1958, Computability and Unsolvability, Nueva York, McGraw-Hill; reimpreso con un apéndice adicional, Nueva York, Dover Publications 1983.
  • Feferman, S., 1960, "Aritmetización de la metamatemática en un entorno general", Fundamenta Mathematicae, 49 (1): 35-92.
  • Hájek, P. y P. Pudlák, 1993, Metamathematics of First-Order Arithmetic, Berlín: Springer-Verlag.
  • Solovay, RM, 1976, "Interpretaciones de probabilidad de la lógica modal", Israel Journal of Mathematics, 25: 287–304.

El alcance de la lógica de demostrabilidad: límites

  • Berarducci, A. y R. Verbrugge, 1993, "Sobre la lógica de la comprobabilidad de la aritmética limitada", Annals of Pure and Applied Logic, 61: 75-93.
  • Buss, SR, 1986, Aritmética limitada, Nápoles: Bibliopolis.
  • de Jongh, DHJ, M. Jumelet y F. Montagna, 1991, "A prueba del teorema de Solovay", Studia Logica, 50 (1): 51-70.

Lógica de interpretación

  • Berarducci, A., 1990, "The Interpretability Logic of Peano Arithmetic", Journal of Symbolic Logic, 55: 1059-1089.
  • de Jongh, DHJ y F. Veltman, 1990, "Lógicas de comprobabilidad para la interpretación relativa", en PP Petkov (ed.), Lógica matemática: Actas de la escuela de verano Heyting 1988 en Varna, Bulgaria, Boston: Plenum Press, pp. 31-42.
  • de Jongh, DHJ y A. Visser, 1991, "Puntos fijos explícitos en la lógica de la interpretabilidad", Studia Logica, 50 (1): 39-49.
  • Joosten, JJ y Visser, A., 2000, "La lógica de la interpretabilidad de todas las teorías aritméticas razonables", Erkenntnis, 53 (1-2): 3–26.
  • Montagna, F., 1987, "Provability in Finite Subtheories of PA", Journal of Symbolic Logic, 52 (2): 494–511.
  • Shavrukov, V. Yu., 1988, "La lógica de la interpretabilidad relativa sobre la aritmética de Peano", Informe técnico n. ° 5, Moscú: Steklov Mathematical Institute (en ruso).
  • Švejdar, V., 1983, "Análisis modal de oraciones generalizadas de Rosser", Journal of Symbolic Logic, 48: 986–999.
  • Visser, A., 1990, “Interpretability Logic”, en PP Petkov (ed.), Mathematical Logic: Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, Boston: Plenum Press, pp. 175–209.
  • –––, 1998, “Una visión general de la lógica de la interpretabilidad”, en M. Kracht et al. (eds.), Advances in Modal Logic (Volumen 1), Stanford: CSLI Publications, págs. 307–359.

Cuantificadores proposicionales

  • Artemov, SN y LD Beklemishev, 1993, "Sobre cuantificadores proposicionales en lógica de comprobabilidad", Notre Dame Journal of Formal Logic, 34: 401–419.
  • Shavrukov, V. Yu., 1997, "Undecidability in Diagonalizable Algebras", Journal of Symbolic Logic, 62: 79-116.

Las lógicas de demostrabilidad bimodal y polimodal de Japaridze

  • Beklemishev, LD, 2004, “Álgebras de prueba y ordinales de prueba teórica, I”, Annals of Pure and Applied Logic, 128: 103–123.
  • –––, 2010a, “Kripke Semantics for Provability Logic GLP”, Annals of Pure and Applied Logic, 161 (6): 756–774.
  • –––, 2010b, “Sobre la interpolación de Craig y las propiedades de punto fijo de GLP”, en S. Feferman et al. (eds.), Pruebas, categorías y cálculos (Tributes, 13), Londres: Publicaciones universitarias, págs. 49–60.
  • –––, 2011a, “Una prueba simplificada del teorema de integridad aritmética para la lógica de comprobabilidad GLP”, Proceedings Steklov Institute of Mathematics, 274 (1): 25–33.
  • –––, 2011b, “Completitud ordinal de la lógica de comprobabilidad bimodal GLB”, en N. Bezhanishvili et al. (eds.), Lógica, Lenguaje y Computación, 8º Simposio Internacional de Tbilisi TbiLLC 2009 (Lecture Notes in Computer Science: Volume 6618), Heidelberg: Springer, pp. 1-15.
  • Beklemishev, LD y D. Gabelaia, 2013, "Completitud topológica de la lógica de probabilidad GLP", Annals of Pure and Applied Logic, 164 (12): 1201–1223.
  • –––, 2014, “Interpretaciones topológicas de la lógica de demostrabilidad”, en G. Bezhanishvili (ed.), Leo Esakia sobre la dualidad en la lógica modal e intuitiva (contribuciones destacadas a la lógica: volumen 4), Heidelberg: Springer, págs. 257– 290.
  • Beklemishev, LD, J. Joosten y M. Vervoort, 2005, "Un tratamiento finitario del fragmento cerrado de la lógica de capacidad de prueba de Japaridze", Journal of Logic and Computation, 15 (4): 447–463.
  • Fernández-Duque, D. y JJ Joosten, 2014, "Órdenes del pozo sobre el álgebra transfinita de Japaridze", Diario lógico de la IGPL, 22 (6): 933–963.
  • Ignatiev, KN, 1993, "Sobre predicados de probabilidad fuerte y las lógicas modales asociadas", Journal of Symbolic Logic, 58: 249–290.
  • Japaridze, G., 1988, "La lógica de la comprobabilidad polimodal", en Lógica Intensional y la estructura lógica de las teorías: material del cuarto simposio soviético-finlandés sobre lógica, Telavi, págs. 16–48.
  • Pakhomov, FN, 2014, "Sobre la complejidad del fragmento cerrado de la lógica de capacidad de prueba de Japaridze", Archive for Mathematical Logic, 53 (7-8): 949–967.

Lógica de demostrabilidad de predicado

  • Artemov, SN, 1985a, "La no aritmética de la verdad predica la lógica de la demostrabilidad", Doklady Akademii Nauk SSSR, 284: 270–271 (en ruso); Traducción al inglés en Matemáticas soviéticas Doklady, 32: 403–405.
  • McGee, V. y G. Boolos, 1987, "El grado del conjunto de oraciones de lógica de demostrabilidad de predicado que son verdaderas bajo cada interpretación", Journal of Symbolic Logic, 52: 165-171.
  • Vardanyan, VA, 1986, "Complejidad aritmética de la lógica de la capacidad de prueba y sus fragmentos", Doklady Akademii Nauk SSSR, 288: 11–14 (en ruso); Traducción al inglés en Matemáticas soviéticas Doklady, 33: 569–572.
  • Visser, A. y M. de Jonge, 2006, "No Escape from The Vardanyan's Theorem", Archive of Mathematical Logic, 45 (5): 539–554.

Otras generalizaciones

  • Alberucci, L. y A. Facchini, 2009, "Sobre el Modal μ-Calculus y la lógica de Gödel-Löb", Studia Logica, 91: 145–169.
  • Artemov, SN, 1985b, “Sobre la lógica modal de la capacidad de prueba axiomatizante”, Izvestiya Akadademii Nauk SSSR, Seriya Matematicheskaya, 49 (6): 1123–1154 (en ruso); Traducción al inglés en Matemáticas de la URSS – Izvestiya, 27 (3): 402–429.
  • –––, 1994, “Logic of Proofs”, Annals of Pure and Applied Logic, 67 (2): 29–59.
  • –––, 2001, “Probabilidad explícita y semántica constructiva”, Boletín de lógica simbólica, 7: 1–36.
  • Artemov, SN y R. Iemhoff, 2007, "La lógica intuitiva básica de las pruebas", Journal of Symbolic Logic, 72 (2): 439-451.
  • Artemov, SN y F. Montagna, 1994, "Sobre las teorías de primer orden con operador de demostrabilidad", Journal of Symbolic Logic, 59 (4): 1139-1153.
  • Beklemishev, LD, 1989, "Sobre la clasificación de las lógicas de demostrabilidad proposicional", Izvestiya Akademii Nauk SSSR, Seriya Matematicheskaya., 53 (5): 915–943 (en ruso); Traducción al inglés en Matemáticas de la URSS – Izvestiya, 35 (1990) 247–275.
  • –––, 1994, “Sobre las lógicas bimodales de demostrabilidad”, Annals of Pure and Applic Logic, 68: 115–160.
  • –––, 1996, “Bimodal Logics for Extensions of Arithmetical Theories”, Journal of Symbolic Logic, 61: 91–124.
  • –––, 1999, “Inducción libre de parámetros y funciones computables probables totales”, Teorematic Computer Science, 224: 13–33.
  • –––, 2005, “Principios de reflexión y álgebras de demostrabilidad en aritmética formal”, Uspekhi Matematicheskikh Nauk, 60 (2): 3–78. (en ruso); Traducción al inglés en: Russian Mathematical Surveys, 60 (2) (2005): 197–268.
  • –––, 2006, “The Worm Principle”, en Lecture Notes in Logic 27. Logic Colloquium '02, Z. Chatzidakis, P. Koepke y W. Pohlers (eds.), Natick (MA): AK Peters, pp 75-95.
  • –––, 2012, “Calibrando la lógica de probabilidad: de la lógica modal al cálculo de la reflexión”, en T. Bolander, T. Braüner, S. Ghilardi y L. Moss (eds.), Avances en la lógica modal (Volumen 9), Londres: Publicaciones universitarias, págs. 89–94.
  • –––, 2014, “Lógica de demostrabilidad positiva para principios de reflexión uniformes”, Annals of Pure and Applied Logic, 165 (1): 82–105.
  • Beklemishev, LD, D. Fernández-Duque y JJ Joosten, 2014, “Sobre lógicas de demostrabilidad con modalidades ordenadas linealmente”, Studia Logica, 102 (3): 541–566.
  • Beklemishev, LD, M. Pentus y N. Vereshchagin, 1999, Provability, Complexity, Grammars, American Mathematical Society Translations (Serie 2, Volumen 192).
  • Beklemishev, LD y A. Visser, 2006, "Problemas en la lógica de la comprobabilidad", en DM Gabbay, SS Goncharov y M. Zakharyashev (eds.), Problemas matemáticos de la lógica aplicada I: Lógicas para el siglo XXI (Serie matemática internacional, Volumen 4), Nueva York: Springer, págs. 77–136.
  • van Benthem, J., 2006, "Correspondencias de marco modal y puntos fijos", Studia Logica, 83 (1-3): 133-155.
  • Carlson, T., 1986, "Lógicas modales con varios operadores e interpretaciones de demostrabilidad", Israel Journal of Mathematics, 54 (1): 14–24.
  • Dashkov, EV, 2012, "Sobre el fragmento positivo de la lógica de comprobabilidad polimodal GLP", Mathematical Notes, 91 (3): 318–333.
  • Fernández-Duque, D., 2014, "La lógica de las politopologías de demostrabilidad transfinita", Archive for Mathematical Logic, 53 (3-4): 385–431.
  • Fernández-Duque, D. y JJ Joosten, 2013a, "Hyperations, Veblen Progressions, and Transfinite Iteration of Ordinal Functions", Annals of Pure and Applied Logic 164 (7-8): 785–801, [disponible en línea].
  • Fernández-Duque, D. y JJ Joosten, 2013b, "Modelos de lógica de demostrabilidad transfinita", Journal of Symbolic Logic, 78 (2): 543–561, [disponible en línea].
  • Guaspari, D. y RM Solovay, 1979, "Rosser Sentences", Annals of Mathematical Logic, 16: 81–99.
  • Iemhoff, R., 2000, "Un análisis modal de algunos principios de la lógica de probabilidad de la aritmética de Heyting", en Advances in Modal Logic (Volumen 2), M. Zakharyashev et al. (eds.), Stanford: Publicaciones CSLI, pp. 319–354.
  • –––, 2001, “Sobre las reglas admisibles de la lógica proposicional intuicionista”, Journal of Symbolic Logic, 66: 281–294.
  • –––, 2003, “Lógica de la preservación: un análogo de la lógica de la interpretabilidad para las teorías constructivas”, Lógica matemática trimestral, 49 (3): 1–21.
  • Lindström, P., 1994, "La lógica modal de la comprobabilidad de Parikh", Filosofiska Meddelanden, Gröna Serien, Gotemburgo: Göteborgs Universitetet.
  • Lindström, P., 2006, "Sobre Parikh Provability: An Exercise in Modal Logic", en H. Lagerlund, S. Lindström y R. Sliwinski (eds.), Modality Matters: veinticinco ensayos en honor de Krister Segerberg, Uppsala: Uppsala Philosophical Studies (Volumen 53), págs. 53–287.
  • Montagna, F., 1978, "Sobre la algebraización del predicado de Feferman", Studia Logica, 37 (3): 221–236.
  • –––, 1979, “Sobre el álgebra diagonalizable de la aritmética de peano”, Bollettino della Unione Matematica Italiana, B (5), 16: 795–812.
  • –––, 1980a, “Interpretaciones de la teoría de primer orden de álgebras diagonalizables en aritmética de peano”, Studia Logica, 39: 347–354.
  • –––, 1980b, “Indecidibilidad de la teoría de primer orden de álgebras diagonalizables”, Studia Logica, 39: 355–359.
  • –––, 1984, “The Predicate Modal Logic of Provability”, Notre Dame Journal of Formal Logic, 25 (2): 179–189.
  • –––, 1992, “Pruebas polinomiales y superexponencialmente más cortas en fragmentos de aritmética”, Journal of Symbolic Logic, 57: 844–863.
  • Pakhomov, FN, 2012, "Indecidibilidad de la teoría elemental del semilattice de palabras GLP", Sbornik: Matemáticas, 203 (8): 1211.
  • Shapirovsky, I., 2008, "PSPACE-decidability of Japaridze's Polymodal Logic", Advances in Modal Logic, 7: 289–304.
  • Shavrukov, V. Yu., 1993a, "Una nota sobre las álgebras diagonales de PA y ZF", Annals of Pure and Applied Logic, 61: 161-173.
  • –––, 1993b, “Subálgebras de álgebras diagonalizables de teorías que contienen aritmética”, Dissertationes Mathematicae, 323.
  • –––, 1994, “Un niño inteligente de Peano”, Notre Dame Journal of Formal Logic, 35 (2): 161–185.
  • Troelstra, AS, 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Berlín: Springer-Verlag.
  • Visser, A., 1980, Aspects of Diagonalization and Provability, Ph. D. Tesis, Utrecht: Universidad de Utrecht.
  • –––, 1982, “Sobre el principio de integridad: un estudio de demostrabilidad en la aritmética y las extensiones de Heyting”, Annals of Mathematical Logic, 22 (3): 263–295.
  • –––, 1989, “Peano's Smart Children: A Provability Logical Study of Systems with Built-in Consistency”, Notre Dame Journal of Formal Logic, 30 (2): 161–196.
  • –––, 1999, “Reglas y aritmética”, Notre Dame Journal of Formal Logic, 40 (1): 116–140.
  • –––, 2002, “Sustituciones de (Sigma_1) Oraciones: exploraciones entre lógica proposicional intuitiva y aritmética intuicionista”, Annals of Pure and Applied Logic, 114: 227–271.
  • –––, 2005, "Löb's Logic Meets the μ-Calculus", en A. Middeldorp, V. van Oostrom, F. van Raamsdonk y R. de Vrijer (eds.), Procesos, Términos y Ciclos: Pasos en el camino al infinito, Berlín: Springer, págs. 14-25.
  • –––, 2008, “Fragmentos cerrados de las lógicas de demostrabilidad de las teorías constructivas”, Journal of Symbolic Logic, 73: 1081–1096.
  • Zambella, D., 1994, "Teorema de Shavrukov sobre las subálgebras de álgebras diagonales para teorías que contienen (I / Delta_0 + / exp)", Notre Dame Journal of Formal Logic, 35: 147–157.

Significado filosófico

  • Davis, M., 1990, "Is Mathematical Insight Algorithmic?", Comentario sobre Roger Penrose, The Emperor's New Mind, Behavioral and Brain Sciences, 13: 659–660.
  • –––, 1993, “¿Qué tan sutil es el teorema de Gödel?” (Comentario sobre Roger Penrose, La nueva mente del emperador), Behavioral and Brain Sciences, 16: 611–612.
  • Egré, P., 2005, "La paradoja del conocedor a la luz de las interpretaciones de demostrabilidad de las lógicas modales", Journal of Logic, Language and Information, 14 (1): 13–48.
  • Kaplan, D. y R. Montague, 1960, "Una paradoja recuperada", Notre Dame Journal of Formal Logic, 1 (3): 79-90.
  • Montague, R., 1963, "Tratamientos sintácticos de modalidad, con corolarios sobre principios de reflexión y ansiomatización finita", Acta Philosophica Fennica, 16: 153–67.
  • Quine, WV, 1966, "Verdad necesaria", en Quine, WV, The Ways of Paradox and Other Essays, Nueva York: Random House, págs. 48–56.
  • –––, 1953, “Tres grados de participación modal”, en Actas del 11º Congreso Internacional de Filosofía, Amsterdam: Holanda del Norte, págs. 65-81; reimpreso en WV Quine, The Ways of Paradox and Other Essays, Nueva York: Random House, 1966, pp. 156-174.

Herramientas académicas

icono de hombre sep
icono de hombre sep
Cómo citar esta entrada.
icono de hombre sep
icono de hombre sep
Obtenga una vista previa de la versión PDF de esta entrada en Friends of the SEP Society.
icono inpho
icono inpho
Busque este tema de entrada en el Proyecto de ontología de filosofía de Internet (InPhO).
icono de papeles de phil
icono de papeles de phil
Bibliografía mejorada para esta entrada en PhilPapers, con enlaces a su base de datos.

Otros recursos de internet

Artículos y presentaciones

  • Fernández-Duque, D. y JJ Joosten, 2013, "La interpretación de la regla omega de la lógica de comprobabilidad transfinita", manuscrito en línea en arxiv.org.
  • Henk, P. y Pakhomov, F., 2016, "Probabilidad lenta y ordinaria para la aritmética de Peano", manuscrito en arxiv.org.
  • Pakhomov, F., 2014, "Sobre las teorías elementales de álgebras GLP", manuscrito en arxiv.org.
  • Pakhomov, F., 2015, "Sobre las teorías elementales de los sistemas de notación ordinal basados en los principios de reflexión", manuscrito en arxiv.org.
  • Visser, Albert, Sobre demostrabilidad formal versus demostrabilidad humana (en holandés), manuscrito en línea, Universidad de Utrecht.
  • Verbrugge, Rineke, Diapositivas de presentación sobre lógica de demostrabilidad, diapositivas, Universidad de Groninga

Otros sitios

  • Problemas abiertos en Provability Logic, mantenido por Lev Beklemishev
  • Lista de correo Fundamentos de Matemáticas, Universidad de Nueva York

Recomendado: