¿Cómo funciona una definición recursiva de encajar en una prueba formal?

Question

Entiendo que una prueba como una serie de instrucciones que son los axiomas o seguir a partir de declaraciones anteriores por un pequeño conjunto de reglas de inferencia.

Entiendo que una definición recursiva a ser algo así como ($\phi$ es la adición):

$$ \phi(x, 0) = x $$ $$ \phi(x, y+1) = \phi(x,y)+1,$$

donde formalmente sería utilizar una función sucesor $s(x) = x+1$ en lugar de escribir "+1" en una fórmula.

Lo que me gustaría entender es cómo esta función ajusta a una prueba formal.

Para el fondo, estoy tratando de comprender de Gödel original de la incompletitud de la prueba. Estoy teniendo problemas para entender cómo muchos de sus funciones recursivas/relaciones se expresa formalmente, ya que son símbolos definidos.

Answer 1

De hecho, hay un problema que hay que resolver aquí -- y Gödel resuelve, pero mucho más tarde, en su 1931 el papel que uno tiende a esperar si uno se acerca, armados con el conocimiento de los modernos paráfrasis.

Estamos buscando en la sección 2 de Über formal unentscheidbare Sätze. Gödel [p 176-180] se describe una prueba formal del sistema P para la teoría de los números (simplificado de Principia Mathematica). Entonces [p 179-181] se define brevemente el concepto de "funciones recursivas" (que son lo que hoy llamamos "primitivas recursivas") y, a continuación, [182ff] inmediatamente se lanza a una larga lista de funciones recursivas que arithmetize el sistema formal.

Pero espera! el lector moderno gritos. No está del todo claro cómo todas estas funciones recursivas puede decirse que existen dentro del sistema de P. Y de hecho no, en este punto en el desarrollo de Gödel trata de las funciones recursivas como existentes completamente fuera del sistema formal; aparecen en el nivel meta.

(Creo que esto es lo que él quiere decir cuando se les describe como "número de la teoría de funciones". Hoy en día, que probablemente iba a estar dispuesto a comprender el "número de la teoría de la función", implica que la función puede ser definida en un determinado sistema formal, tales como la aritmética de Peano, pero esto es en gran medida debido a Gödel del propio trabajo. Antes de eso, "número teórico" debe de haber evocado la idea de "que tipo de matemáticas que no necesita para descansar en la axiomática de desarrollo, porque es intuitivamente obvio cómo funciona".)

Inmediatamente después de la lista de lavandería, las funciones recursivas son finalmente conectado al sistema formal de la Proposición V, que dice que cada recursiva relación corresponde a una fórmula de sistema de P. La cosa extraña es que la Proposición V no es realmente demostró -- Gödel sólo las ondas de sus manos un poco y se deja como ejercicio para el lector. Esto es muy desconcertante para un lector que se utiliza para ver Gödel del argumento desarrollado por algo como la aritmética de Peano. En ese caso, la Proposición V no es en absoluto evidente, pero lo que tendemos a olvidar es que el sistema P es un orden superior sistema donde uno puede cuantificar sobre todas las funciones y así sucesivamente. Algo así como el conjunto habitual de la teoría de la argumentación de que una definición recursiva en realidad define algo (como se indica en la respuesta de David) puede ser llevado a cabo directamente en el sistema de P.

Más adelante en el documento, en la sección 3 que es casi un recuerdo, Gödel muestra como la Proposición VII que una relación recursiva puede también ser representado como un primer orden de la fórmula que contiene sólo la adición, la multiplicación y la cuantificación sobre los números naturales. Aquí es donde nos encontramos con algo de fama $\beta$ función de la construcción, y es este el argumento de que en la mayoría de los modernos narraciones tomar el lugar de Gödel de la propia Proposición V.

Answer 2

Yo también solía tener un montón de problemas para la comprensión de este. Déjame ver si la siguiente ayuda.

Supongo que estamos trabajando en algunas versiones de la teoría de conjuntos y que ya he definido los pares ordenados, números enteros no negativos, y las anotaciones $+$$\times$. Voy a escribir $\mathbb{N}$ para el conjunto de todos los números enteros no negativos. Supongamos que ahora tenemos que definir la función de $n \mapsto 2^n$ $\mathbb{N}$ a sí mismo, y voy a hacerlo de forma recursiva.

Aquí es lo que yo debería probar:

Teorema: Existe un único subconjunto $F$ $\mathbb{N} \times \mathbb{N}$ tal que

1. Para cada $x \in \mathbb{N}$, no es precisamente una $y \in \mathbb{N}$ tal que $(x,y) \in F$.
2. $(0,1) \in F$.
3. Si $(x,y) \in F$ $(x+1, 2 \times y) \in F$

Entonces, cada vez que quiero escribir $y=2^{10}$, en lugar de escribir "Vamos a $F$ ser el único subconjunto de $\mathbb{N} \times \mathbb{N}$ ( ... ) y vamos a $y$ ser el único elemento de $\mathbb{N}$ tal que $(10, y) \in F$."

Por supuesto, no he utilizado plenamente lenguaje formal aquí. Declaración 1, explica que "Para todos los $x$ $\mathbb{N}$ existe $y \in \mathbb{N}$ tal que $(x, y) \in F$ y, para todos los $x$, $y_1$ y $y_2$ $\mathbb{N}$ si $(x,y_1) \in F$$(x,y_2) \in F$,$y_1 = y_2$." Una similar desembalaje debe ser realizado con la declaración de que $F$ es único.

Este es un buen momento para hacer una pausa y asegúrese de entender lo que he escrito hasta ahora.

---

Así que, ¿cómo demostrarlo? Voy a bosquejar dos pruebas porque no sé si usted se siente cómodo con la escritura inductivo pruebas formalmente. Así que la primera prueba trata de inducción de manera informal y se supone que se puede llenar los huecos, y la segunda prueba llena esos vacíos para usted.

Prueba de dibujo (informal de inducción): Para $n \in \mathbb{N}$, vamos a $\mathbb{N}_{\leq n}$ el conjunto de números enteros no negativos inferior o igual a $n$. Primero mostramos

Reclamo Para todos los $n\in \mathbb{N}$, no existe un único subconjunto $G$ $\mathbb{N}_{\leq n} \times \mathbb{N}$ tal que

1. Para cada $x \in \mathbb{N_{\leq n}}$, no es precisamente una $y \in \mathbb{N}$ tal que $(x,y) \in G$.
2. $(0,1) \in G$.
3. Si $(x,y) \in G$ $x<n$ $(x+1, 2 \times y) \in G$

Nuestra prueba es por inducción sobre $n$. Si $n=0$, tome $G= \{ (0,1) \}$. Yo se lo dejo a usted para comprobar que esto funciona y que es único.

Para $n>0$, vamos a $G'$ ser el subconjunto de $\mathbb{N}_{\leq n-1} \times \mathbb{N}$ ave construye inductivamente. Deje $y$ ser el único número entero tal que $(n-1, y) \in G'$. Set $G = G' \cup \{ (n, 2 \times y ) \}$. De nuevo, usted debe comprobar que esto funciona y que es único.

Definir $F$ a ser el conjunto de pares ordenados $(x,y)$ $\mathbb{N} \times \mathbb{N}$ tal que para algunos $(n, G)$ como en el anterior, el par ordenado $(x,y)$$G$. El resto de la prueba está a la izquierda. $\square$

Prueba de dibujo (formales de inducción): Voy a suponer que, cuando se construye $\mathbb{N}$, que resultó ser el Bien Principio de orden:

Cualquier subconjunto no vacío de a $\mathbb{N}$ tiene al menos un elemento.

Deje $S$ el conjunto de $n$ que no lo hace no existe un conjunto $G$ como en la Demanda. Si $S=\emptyset$, la demanda sostiene y nos finalizar la prueba anterior.

Al $n=0$, la $\{ (0,1) \}$ satisface la Demanda (los detalles omitidos), por lo $0 \not \in S$. Asumir por el bien de la contradicción que $S$ es no vacío. Entonces, por el Principio de orden, $S$ tiene al menos un elemento de a $n$. Por la primera frase de este párrafo, $n >0$.

Desde $n-1 \not \in S$, hay un conjunto $G'$ que satisface la demanda con respecto a $n-1$. Deje $y$ ser el único número entero tal que $(n-1, y) \in G'$. Set $G = G' \cup \{ (n, 2 \times y ) \}$. A continuación, $G$ satisface la demanda con respecto a $n$ (detalles omitidos). Por lo $n$ no $S$ después de todo, una contradicción. $\square$

Comentario de expertos deliberadamente enunciado de la anterior prueba para evitar el Axioma de Reemplazo. Toda la fuerza de la Recursividad Teorema requiere el Reemplazo, pero pensé que era mejor pedagógicamente para esquivar este problema, mientras que podía.