7 votos

¿Existe un enfoque constructivo que sustituya a la construcción de Henkin?

Prueba de Henkin para el teorema de completitud de Goedel que se basa en la construcción de Henkin utilizando modelos de términos construidos por constantes no es constructiva.

Mi pregunta es si existe algún enfoque constructivo que sustituya a la construcción de Henkin. Si no es así, ¿es posible demostrar que no existe tal prueba constructiva en absoluto?

6voto

JoshL Puntos 290

Por el lado de la computabilidad pura, clásicamente, sabemos que hay teorías efectivas que son consistentes pero no tienen un modelo computable. Por ejemplo, no hay modelos computables no estándar de PA, pero hay una axiomatización efectiva de PA + " $c$ es un número no estándar".

Así que no podemos esperar, en general, tener un modelo computable para cada teoría efectiva. Por otro lado, si hubiera una demostración totalmente constructiva del teorema de completitud, entonces esperaríamos que el teorema de completitud fuera "computablemente verdadero", porque es imposible en la mayoría de los sistemas de matemáticas constructivas demostrar la existencia de un subconjunto de $\mathbb{N}$ sin que ese subconjunto sea computable (esto es una consecuencia de la técnica de "realizabilidad" en la teoría de la prueba).

Podemos pedir lo incalculable que es los modelos construidos por el teorema de la completitud tienen que ser, si no tienen que ser computables. En general, el conjunto de modelos contables de una teoría efectiva es siempre un $\Pi^0_1$ y así el teorema de la base baja muestra que si una teoría efectiva es consistente entonces tiene un modelo $X$ tal que el salto de Turing de $X$ es $\emptyset'$ , que es lo más pequeño que puede ser el salto.

En general, un grado de Turing se llama Grado de AP si es capaz de computar un elemento de cada no vacío $\Pi^0_1$ clase. Equivalentemente, y de forma no obvia, son los grados que pueden computar la teoría de una extensión completa de la aritmética de Peano. Así que resulta que el problema de poder encontrar un modelo de cada teoría efectiva constante no es peor que el problema de poder encontrar una terminación de la aritmética de Peano.

En el contexto de la Matemática Inversa en la aritmética de segundo orden, la existencia de un completamiento de PA, y el teorema de completitud para las teorías de primer orden contables, son ambos equivalentes a $\textsf{WKL}_0$ en $\textsf{RCA}_0$ . Sin embargo, esto no es más que un reflejo de los hechos de la teoría de la computabilidad mencionados anteriormente.

4voto

DanV Puntos 281

Como el teorema de completitud para la lógica de primer orden, en su generalidad, es equivalente al teorema del ideal primo booleano, y este último no es demostrable sin el axioma de elección... la respuesta es no.

En ese caso no hay forma de escribir completamente un algoritmo constructivo.

0 votos

Es muy decepcionante. ¿No es así? :-(

1 votos

¿Qué pasa con las teorías axiomáticas computables?

0 votos

Quiero decir que cuando uno observa el enfoque de Henkins en esta (y otras construcciones similares) no constructivas, realmente siente que podría haber muchas otras formas constructivas de resolver el problema, pero de repente comprende que no hay ninguna y que la cuestión quedará sin resolver para siempre. Lo peor del problema es que la elección juega un papel fundamental.

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X