Algunas preguntas sobre las implicaciones "profundas" del Teorema de Completitud de Gödel (si las hay)

Question

Estoy tratando de refrescar mis conocimientos sobre lógica matemática y todavía no estoy satisfecho con mi comprensión del Teorema de Completitud de Gödel.

He estudiado la versión de Henkin y creo que la domino. Algunos libros de texto (por ejemplo Ian Chiswell y Wilfrid Hodges , Lógica matemática (2007), introducen la construcción de Henkin con lógica sentencial, creo que para "introducir" al alumno en la construcción "probándola" en un entorno simplificado.

1) ¿Tiene sentido intentar adaptar la prueba original de Gödel al cálculo sentencial para entender los detalles específicos necesarios para demostrarla para la lógica f-o?

Una de las peculiaridades de la prueba de Henkin es que el aspecto de "completitud" (es decir, si $A$ es válida es demostrable) es algo así como un subproducto de la existencia del modelo. Tenemos casos "extremos", como Boolos & Burgess & Jeffrey, Computabilidad y lógica (5ª ed. - 2007), donde la Existencia del Modelo da la compacidad antes de la introducción de cualquier sistema de prueba, y el Teorema de Completitud está "bastante ausente". De este modo, se "maximizan" los aspectos no constructivos del teorema.

Las pruebas de Gödel utilizan números (naturales). Esto es obvio (con perspicacia) hoy que conocemos el realismo filosófico de Gödel.

La construcción de Hankin evita los números pero utiliza la "materia sintáctica" para construir el modelo. Pero esto (según mi entendimiento) no es realmente diferente; para "ejecutar" la construcción necesitamos muchos símbolos contables, y los símbolos son "entidades abstractas" (como los números). Creo que realmente los necesita : no podemos reemplazarlos por marcas de conteo "físicas". Así que mi pregunta :

2) ¿En qué sentido podemos minimizar la importancia "ontológica" del teorema?

En un esfuerzo anterior pedí algunas aclaraciones a un distinguido académico y recibí esta respuesta : "Sobre la prueba de completitud, es un teorema de la matemática ortodoxa, y no pretende ser nominalista."

No he estudiado la lógica intuicionista, pero sé que hay semántica para ella.

3) ¿Existen teoremas de "completitud" (que vinculen la semántica con los sistemas de prueba) para la lógica intuicionista f-o? ¿Qué hay de su no constructivo aspectos (si los hay) ?

¿Cuál es la opinión de constructivista ¿los matemáticos (no necesariamente intuicionistas) sobre la prueba de Gödel o de Henkin, y sobre el resultado correspondiente (si lo hay) para la lógica f-o intuicionista?

Answer 1

En primer lugar, la prueba estándar del teorema de la completitud no es constructiva, y necesariamente lo es. Se sabe que hay conjuntos de axiomas consistentes computables que no tienen modelos computables. Por lo tanto, cualquier prueba de que todo conjunto consistente de axiomas tiene un modelo tendrá que utilizar técnicas que permitan la creación de conjuntos no computables.

La prueba original de Gödel no ayuda en este sentido. De hecho, es algo menos susceptible de una interpretación constructiva, porque se basa en una especie de funciones de Skolem, que nos llevan a tipos superiores, mientras que el método de Henkin no requiere la Skolemización. Hay una buena descripción del argumento original de Gödel en este documento por Jeremy Avigad.

Segundo: existen efectivamente teoremas de completitud para la lógica intuicionista. Pero la semántica es muy diferente en ese entorno, porque las lógicas no son susceptibles de funciones de verdad de 2 valores. De hecho, la situación es más complicada en la lógica no clásica. En la lógica clásica de primer orden, tenemos esencialmente una sola semántica, la que utiliza estructuras de primer orden. Hay variaciones menores, pero todas se reducen a lo mismo. En la lógica intuicionista, hay varias semánticas bastante diferentes: la semántica topológica, los modelos de Kripke y la realizabilidad son tres importantes. Hay algunas conexiones entre ellas, sin duda, pero varían mucho más que diferentes presentaciones de la misma cosa, como en la lógica clásica de primer orden.

También hay un problema con la lógica intuicionista que consiste en que algunos intuicionistas reales (o constructivistas, más generalmente) no aceptan que su razonamiento pueda ser capturado adecuadamente en ningún sistema formal. Se resisten a formalizar su trabajo, por lo que no aceptarían que cualquier teorema de completitud para una lógica intuicionista formalizada sea aplicable a su propio razonamiento.