Que número natural predicados pueden ser definidos en la aritmética de Robinson?

Question

Estoy sobre todo pensando sobre el fin de la relación, resta, división y exponenciación aquí:

• $x \leq y \quad \Leftrightarrow \quad \exists u\ y=x+u$
• $z= x-y \quad \Leftrightarrow \quad x=y+z\lor (x\leq y \land z=0)$
• $z=x/y \quad \Leftrightarrow \quad \exists u\ x+u=yz\land Su\leq y$
• $z=x^y \quad \Leftrightarrow \quad E(x,y,z)$

Sé que $E(x,y,z)$ puede ser definido para la aritmética de Peano, pero que cualquier fórmula explícita para $E(x,y,z)$ es ridículamente complicado. Porque la aritmética de Peano y Robinson aritmética de tener el mismo idioma, cualquier fórmula para $E(x,y,z)$ que trabaja para la aritmética de Peano es también una fórmula válida para la aritmética de Robinson.

Estos se parecen válidas las definiciones posibles para el predicados, entonces, ¿dónde está el problema? Estoy bastante seguro de que la exponenciación no puede ser definido en la aritmética de Robinson! Esto significa que no importa cual sea la fórmula para $E(x,y,z)$ que trabaja en la aritmética de Peano que yo uso, no voy a ser capaz de probar $E(x,y,z)\land E(x,y,z')\ \rightarrow\ z=z'$ en la aritmética de Robinson.

No estoy seguro de si hay definiciones para la resta y la división por la que puede ser demostrado (en Robinson aritmética) que las fórmulas correspondientes definir funciones. Estoy buscando un "claro claro" respuesta con respecto a esta "incertidumbre". En realidad no creo que el orden habitual relación puede ser definida en la aritmética de Robinson. El orden habitual relación satisfaga las siguientes fórmulas:

• $x\leq y \land y\leq z\ \rightarrow\ x\leq z$ (transitividad)
• $x\leq y \land y\leq x\ \rightarrow\ x=y$ (antisymmetry)
• $x\leq x$ (reflexividad)
• $x\leq y \lor y\leq x$ (totalidad)

Aclaración Aquí uno se puede preguntar cuál de estas propiedades tienen que ser comprobada antes de que podamos afirmar que hemos definido como "el orden habitual de la relación". Claramente transitividad y reflexividad no se puede renunciar. Yo no quiero renunciar a antisymmetry bien, si se puede evitar, debido a que esta condición es bastante similar a la situación que se muestra que un predicado se define una función. No hay necesidad de probar la totalidad, porque la totalidad no es un "Cuerno de la propiedad", y debido a que la línea tiene que ser dibujado en algún lugar.

Con el fin de mostrar que un predicado $P(x,y,z)$ define una función, al menos en las condiciones $P(x,y,z)\land P(x,y,z')\ \rightarrow\ z=z'$ debe ser comprobable. Sería bueno si $\exists z\ P(x,y,z)$ sería comprobable así, pero porque esto no es un "universal Cuerno de la propiedad" y la línea tiene que ser dibujado en algún lugar, puede ser renunciado. A continuación, sólo tenemos una función parcial en lugar de un total de función, pero por lo menos todavía tenemos una función.

Visión de Asaf y Pedro criar a un punto muy válido, que no me había dado cuenta antes. Por qué criterios puedo decidir que un predicado (dado por una arbitraria de primer orden de la fórmula en la $Q$) corresponde a un cierto número natural predicado? Pedro sugiere una respuesta, que yo sería un poco debilitar tales que también se aplica a los predicados que no se definen las funciones. Para $E(x,y,z)$ mi condición lee

Si $m^n = k$ entonces $Q \vdash E(\overline{m}, \overline{n}, \overline{k})$ y
si $m^n \neq k$ entonces $Q \vdash \lnot E(\overline{m}, \overline{n}, \overline{k})$

donde $\overline{m}$ es $Q$'s formal numeral para $m$.

---

Si resultara que algunos de los "inofensivos" número natural predicados no puede ser definido en Robinson aritmética, entonces sería interesante saber si hay un tratamiento conservador de la extensión (="equiconsistent") de Robinson aritmética donde todos canónica "inofensivo" número natural predicados pueden ser definidos. Exponenciación no es "inofensivo", porque si $x$, $y$ y $z$ son binarios codificados, la longitud de $z=x^y$ será del orden de $|x|y$, que es exponencialmente mayor que $|x|+|y|$.

Answer 1

Cualquier fórmula explícita para $E(x,y,z)$ [en el lenguaje de PA] es ridículamente complicado.

Bueno, en realidad no es que complicado! Es tedioso pero ejercicio fácil, una vez que hayas aprendido cómo utilizar Gödel de la beta-función (la cual puede ser escrito en notación primitiva en la mitad de una línea o así) para escribir un candidato $E$ en primitivo de la notación en un par de líneas.

Exponenciación no puede ser definido en la aritmética de Robinson!

Bueno, depende de lo que quieres decir con definida! Diferentes autores significar diferentes cosas por "definir" (uno de los casos de leve cosas molestas en esta área es que es un poco de coherencia a través de los libros de texto aquí).

Sin duda, el siguiente tiene por $Q$ (Robinson Aritmética): hay una fórmula $E(x, y, z)$ tal que

si $m^n = k$ entonces $Q \vdash E(\overline{m}, \overline{n}, \overline{k})$ y

para cada $m, n$, $Q \vdash \exists!zE(\overline{m}, \overline{n}, z)$

donde $\overline{m}$ es $Q$'s formal numeral para $m$. Y un montón de autores de la llamada que la definición (incluso "fuertemente de la definición de") exponenciación. De hecho, en este sentido, $Q$ puede (inicialmente sorprendentemente) definir todas las funciones recursivas primitivas.

Pero sí, $Q$ es absolutamente pésimo a probar las generalizaciones, y en particular (como creo que usted está señalando)

$Q \nvdash \forall x\forall y\exists!zE(x, y, z)$

y así, $Q$ no se puede demostrar que la exponenciación es (como dicen) una demostrablemente total de la función. Es esto lo que quieres decir por definición?

Probablemente así: no obstante, antes de continuar con sus preguntas, tal vez necesite una declaración explícita de lo que entendemos por "definición" aquí.

Answer 2

Si resultara que algunos de los "inofensivos" número natural predicados no puede ser definido en Robinson aritmética, entonces sería interesante saber si hay un tratamiento conservador de la extensión (="equiconsistent") de Robinson aritmética donde todos canónica "inofensivo" número natural predicados pueden ser definidos. Exponenciación no es "inofensivo", porque si $x$, $y$ y $z$ son binarios codificados, la longitud de $z=x^y$ será del orden de $|x|y$, que es exponencialmente mayor que $|x|+|y|$.

Asaf comentario de "Robinson aritmética ni siquiera puede demostrar que $Sx\neq x$ para todos los $x$" muestra que algunos de los "inofensivos" número natural predicados no puede ser definido en la aritmética de Robinson, al menos si "definir", se lee de acuerdo a los criterios descritos en la "aclaración de la sección". Pero debido a que estos criterios sólo requieren provability de "universal Cuerno propiedades", uno podría intentar añadir una restricción de la inducción axioma universal de los predicados a Robinson aritmética. Sin embargo, esta extensión es "casi seguro" no conservador. Una mejor estrategia podría ser comenzar por añadir el axioma de antisymmetry de la orden de relación (usando la definición implícita de $\leq$), debido a que es necesario en cualquier caso. Entonces uno puede probar para comprobar si esto le da a la solicitada (conservador?) la extensión. Sin embargo, la descripción dada de la canónica de "inofensivo" número natural predicado es "demasiado informal" para ser capaz de verificar esto.

Una característica es compartida por la propuesta de definiciones de la orden de relación, la resta y la división. Los predicados $P(x,y,z)$ son todos de la forma $P(x,y,z)=\exists u_1\ldots u_r:\phi(u_1,\ldots,u_r,x,y,z)$ con un cuantificador fórmula libre de $\phi$. La fórmula explícita para $E(x,y,z)=\operatorname{pow}(x,y,z)$ dado por Hagen von Eitzen por otro lado no tiene esta forma:

El uso de las siguientes abreviaturas

$$\begin{align}a\le b&\equiv\exists n\colon a+n=b\\ a< b&\equiv Sa\le b\\ \operatorname{mod}(a,b,c)&\equiv \exists n\colon a=b\cdot n+c\land c<b\\ \operatorname{seq}(a,b,k,x)&\equiv \operatorname{mod}(a,S(b\cdot Sk),x)\\ \operatorname{pow}(a,b,c)&\equiv\exists x\exists y\colon\operatorname{seq}(x,y,0,S0)\land\operatorname{seq}(x,y,b,c)\land \\&\quad\forall k\forall z\colon((k<c\land \operatorname{seq}(x,y,k,z))\to \operatorname{seq}(x,y,Sk,a\cdot z))\end{align}$$ tenemos $\operatorname{pow}(a,b,c)$ si y sólo si $c=a^b$. Curiosamente, necesita algunos elementales de la teoría de números (como el teorema del resto Chino) a la meta-apreciar esto.

Este parece tener la forma $P(x,y,z)=\exists u_1\ldots u_r\forall v_1\ldots v_s:\phi(u_1,\ldots,u_r,v_1,\ldots,v_s,x,y,z)$ o incluso $P(x,y,z)=\exists u_1\ldots u_r\forall v_1\ldots v_s\exists w_1\ldots w_t:\phi(u_1,\ldots,u_r,v_1,\ldots,v_s,w_1,\ldots,w_t,x,y,z)$ si insistimos en que el modulo no es una operación primitiva.

Por lo tanto podría ser una buena idea para interpretar "inofensivo" número natural predicado como los predicados que pueden ser definidas por el existencial de los predicados.