Es la frase "Cada primitiva de la función recursiva es total" comprobable en $PA$?

Question

En ciencias de la computación folleto he encontrado en internet (google: funciones recursivas primitivas Prim Rec Fcns Inicial Funciones: N), de la siguiente reclamación:

Cada primitiva de la función recursiva es total.

Es este comprobable en la Aritmética de Peano? Si es así, me gustaría ver la prueba.

Gracias de antemano.

Answer 1

Yo diría que el mayor problema con esta es la simbolización de esta declaración. La Aritmética de Peano no tiene símbolos para expresar esto en ninguna forma directa como $\forall x ((Fun(x) \land PrRec(x)) \rightarrow Total(x))$ ... PA sólo tiene símbolos para muy básicas de la aritmética: $0$, $s$, $+$, y $*$. Estos símbolos son el Lenguaje de la Aritmética o $L_A$.

Ahora, podemos tratar de usar expresiones de $L_A$ a expresar otras cosas. Por ejemplo, para expresar $x < y$ podemos usar $\exists z : y = x + s(z)$, y como tal podemos usar $<$ en PA con el entendimiento de que es la abreviatura de esta expresión.

Pero con el fin de hablar acerca de las funciones, usted realmente necesita un conjunto teórico primitivas: funciones (definidas sobre los números naturales) sería un tipo especial de relaciones, que son conjuntos de grupos irregulares de los números ... pero no tenemos esas conjunto teórico primitivas en PA.

Por otra parte, podemos codificar sillos de números usando solo números, e incluso podemos hacerlo con $L_A$. Esto está lejos de ser trivial, sin embargo, y haciendo las pruebas dentro de una codificación se convertiría en un verdadero dolor de cabeza, pero supongo que sería posible.

Simboliza la 'primitiva recursiva' trae otro problema, sin embargo: decir que las funciones recursivas primitivas son todos y sólo aquellos que son construidos mediante funciones elementales como el cero de la función, la función sucesor (hey, eso lo tenemos: $S$!), función identidad, y las operaciones de composición y la recursividad es ... difícil, por decir lo menos. De hecho, no estoy seguro de si esto es posible incluso que el uso de la PA y de la lógica de primer orden ... tal vez usted tiene que comenzar a usar de segundo orden de la lógica (y, de nuevo, algunos teoría) realmente para definir esto como una clase de objetos que se forma recursiva cerrado bajo las operaciones.

Suponiendo que podemos hacer la simbolización, sin embargo, yo diría que la prueba es completamente trivial: todas las funciones básicas son el total, y el uso de la composición y la recursividad conserva la totalidad, y todo esto sería bastante fácil para mostrar una vez que el expresiva de la maquinaria está en su lugar. Pero se está haciendo el reclamo expresado en un aplicables formato que el principal problema!