¿Puede una teoría decidible tener modelos no recursivos?

Question

Teorema de Tennenbaum demuestra que ni la suma ni la multiplicación pueden ser recursivas en cualquier modelo no estándar de aritmética . La prueba de Tennenbaum se aplica a teorías mucho más débiles que PA .

La prueba de Tennenbaum es una prueba por contradicción. Si la adición o la multiplicación es recursiva en un modelo no estándar, entonces es posible utilizar una forma de inducción llamada overspill para demostrar que los conjuntos recursivamente inseparables pueden ser codificados como números naturales no estándar. El desbordamiento dice que si $f(n)$ es verdadera para todos los números naturales estándar, entonces $f(\alpha)$ es verdadera para algún número natural no estándar, $\alpha$ . Un ejemplo de conjunto recursivamente inseparable sería el conjunto de números naturales estándar que codifica una máquina de Turing que se detiene con una entrada en blanco.

Dejemos que $\mathbb{N}^*$ sea un modelo contable no estándar de PA y sea $\mathbb{Z}^*$ sean los enteros extendidos de $\mathbb{N}^*$ . Un "campo finito no estándar" sería un anillo $\mathbb{Z}^* /p^* \mathbb{Z}^*$ donde $p^*$ es un número primo no estándar mayor que cualquier número natural estándar. Los campos finitos no estándar admiten eliminación del cuantificador casi . Esto significa que los campos finitos no estándar deben ser "casi recursivos".

Se puede demostrar El teorema de Tennenbaum se aplica a campos finitos no estándar . Si existe un campo finito no estándar recursivo, entonces la prueba por contradicción de Tennenbaum se convierte en una prueba de contradicción. Esto significa que podemos determinar recursivamente si un número natural estándar, $n$ , codifica una TM de parada comprobando si $n$ es una raíz de uno de un conjunto finito de polinomios.

¿Es suficiente la "casi eliminación del cuantificador" para demostrar que un campo finito no estándar es recursivo? Incluso si no lo es, esto parece ser un gran problema. James Ax demostró la la teoría de los campos finitos es decidible . ¿Puede haber un mapeo recursivo desde un modelo recursivo de campos finitos a un modelo no recursivo o podríamos derivar de nuevo una contradicción?

Answer 1

Se pueden ver varias respuestas a esta pregunta en MathOverflow en https://mathoverflow.net/questions/157624/can-a-decidable-theory-have-non-recursive-models/ . En concreto, la respuesta a la pregunta del título es "sí".

Answer 2

Creo que aquí hay una confusión entre dos nociones de "recursividad".

El teorema de Tennenabum se refiere a las estructuras recursivas. Supongamos, para simplificar, que el lenguaje contiene un único símbolo de relación unario $R$ . Entonces una estructura recursiva $\mathcal M$ para esta lengua tiene un conjunto subyacente $\mathbb N$ y con $R^{\mathcal M}$ un subconjunto recursivo de $\mathbb N$ . La definición formal es más complicada, pero intuitivamente, en una estructura recursiva hay una codificación razonable de los elementos y podemos hacer cálculos razonables. Por ejemplo, los números naturales habituales, el anillo de polinomios sobre los racionales o el conjunto $\mathbb N$ con un predicado para los primos son todas estructuras recursivas. Por el contrario, si equipamos $\mathbb N$ con un único símbolo de relación unario para algún conjunto indecidible, entonces esta estructura no es recursiva.

El teorema de Tennenbaum dice que no existe un modelo recursivo no estándar de la teoría de los números naturales. Por lo tanto, mientras que tenemos programas de ordenador que suman y multiplican números enteros, no puede haber ningún programa de ordenador que pueda realizar manipulaciones en números enteros no estándar.

La eliminación de cuantificadores se ocupa de las teorías, no de las estructuras. Si una teoría tiene eliminación de cuantificadores, o algo parecido, entonces podríamos esperar que sea "fácil" o que esté más cerca de ser decidible. Pero estructuras muy complicadas pueden tener teorías muy simples. Tomemos el ejemplo de antes. La teoría de un conjunto infinito dividido en dos conjuntos infinitos es muy sencilla y fácil de entender. Es ciertamente decidible. Pero la estructura $\mathbb N$ con un predicado para el conjunto de esos números que codifican una máquina de Turing que se detiene es complicado desde este punto de vista, aunque su teoría es decidible.