Hay un algoritmo que cuando se da un conjunto de axiomas, generará una declaración independiente de los axiomas?

Question

Es allí cualquier mecanismo o algoritmo donde se pueden generar los enunciados matemáticos/problemas que se indecidible, yo.su prueba es independiente, a partir de un determinado conjunto de axiomas?

Answer 1

Gödel original de la prueba, en efecto, ofrece tan sólo una receta para una teoría de la $T$ que es recursivamente axiomatized, contiene (o puede implementar) al menos la cantidad mínima aritmética de aritmética para el teorema de la incompletitud de aplicar, y es (omega) consistentes. Por supuesto que hay completa de las teorías a las que el teorema de Gödel no se aplica (y algunos de ellos son no triviales) Pero, dejando a un lado la incoherencia de los casos -- estos excepcionales teorías habrá que cualquiera de las teorías que no pueden ser efectivamente axiomatized o teorías que se sabe (casi) nada acerca de la aritmética o algo equivalente.

Pero suponiendo que se trata con el tipo adecuado de la teoría, la construcción de un Gödel frase va en dos etapas. Primero seleccionamos algunos de una manera sensata de "arithmetizing" la sintaxis de $T$ (es decir, la codificación de wffs, y pruebas por números). [Hay una gran cantidad de libertad de elección aquí, y diferentes opciones de conducirán a diferentes penas no demostrable en $T$: para esta fase no es determinista algorítmica.]

A continuación, Gödel nos dice cómo realmente un wff $Gdl_T(x, y)$ $T$ que representa la relación "$x$ códigos de una prueba de la wff que resulta de poner el número de $y$ para la variable libre en un wff con número de código de la $y$" [los detalles de este wff dependerá tanto $T$ y el esquema de codificación elegido, pero nos puede dar una receta para la producción de la wff]. A continuación, se muestra cómo construir, muy simplemente, un indecidible sentencia de Gödel $G_T$ para la teoría de la $T$$Gdl_T(x, y)$.

El procedimiento de "elegir un esquema de codificación, a continuación, aplicar la receta para la formación de una sentencia de Gödel" se aplica bastante en general (como Gödel subraya en su original de 1931 papel), para la construcción de un indecidible frase para un determinado $T$ de los (muy general) tipo correcto. Si usted quiere más de los detalles escabrosos, cualquier texto estándar le dirá cómo el truco está hecho. O mirar el Episodio 9 de línea de mis notas de Gödel Sin Lágrimas

Answer 2

Depende del conjunto de axiomas.

Algunas teorías se completa, lo que significa que cada una de las declaraciones (en el lenguaje) puede ser probada o refutada a partir de ellos. Por ejemplo, la teoría de la algebraicamente cerrado campos de caracteres"$0$.

Algunas teorías son tan complicados que tal algoritmo tendrá que hacer apelaciones a los oráculos, que puede acceder a las informaciones no podemos calcular por nuestra cuenta. Por ejemplo, las consecuencias de $\sf PA$ no es un decidable teoría, así que no tenemos un algoritmo para calcular.

Los teoremas de incompletitud nos dan unos requisitos muy específicos. La teoría de la $T$ debe ser:

1. Recursivamente enumerable.
2. Lo suficientemente fuerte como para interpretar verdad básica sobre la teoría de números.
3. En consonancia.

En cuyo caso el teorema de la incompletitud[s] nos da un mecanismo para escribir una declaración en la que es independiente de la teoría de la $T$. Si la teoría no cumplir con estos requisitos puede ser completa, o podría ser incompatible, o de que no podría haber un algoritmo (que no apelen a la oráculos).