Cada máquina de Turing corresponde a un sistema formal de

Question

Solomon Feferman, en la página 138 de su papel de 2006 "hay absolutamente irresolubles problemas", dice que cada sistema formal de axiomas puede ser hecho de corresponder a un diseño adecuado máquina de Turing, de modo que

[...] con cada efectivamente determinado sistema formal está asociada a una Turing máquina de $M$ que enumera el conjunto de los teoremas de $S$, o-más pintorescamente-imprime los teoremas de S, uno tras otro.

He omitido el argumento que da para esto porque no me parece problemático. Luego continúa

Por el contrario, dado cualquier lenguaje formal $L$, cualquier máquina de Turing $M$ puede se hace corresponder a un sistema formal $S$ $L$ mediante la extracción de los números que se enumera a aquellos que son los números de Gödel de las fórmulas de $L$, y tomando su deductivo de cierre a los teoremas de $S$. De esta manera, hablar de una bien definida o eficaz, dado que los sistemas formales pueden ser convertidos en hablar de máquinas de Turing y viceversa.

Pregunta: Es el ex informal, aunque correcto argumento que puede ser dado por la identidad entre máquinas de Turing y los sistemas formales?

Mi problema con este informal argumento es el siguiente: si tenemos de todos los números de $M$ enumera, sólo el deductivo de cierre de esas fórmulas que corresponden a los números de Gödel de una lengua determinada,$L$, ¿qué acerca de aquellos números que no corresponden a cualquier número de Gödel? ¿Cómo van a ser considerados en el sistema formal, que supuestamente corresponde a $M$?

A mí me parece que esos números son simplemente ignorados por este argumento, y que tal vez de una manera más directa argumento que dice más acerca de las reglas de inferencia sería el más adecuado en este caso. Pero tal vez hay algo que me estoy perdiendo aquí...

Answer 1

Creo que esto es en última instancia, no es un problema (que no es decir que esta es una pregunta tonta!).

Tenga en cuenta que podemos elegir el uso de un método de numeración de Gödel, que es surjective - que es, en la que cada número corresponde a un bien formado fórmula. Esta no es la única Gödel introducido, y toma un poco de trabajo para cocinar, pero es perfectamente aceptable (y, en particular, es en sí mismo computable en el sentido obvio). Esto le da un muy rápido gracias a la traducción entre máquinas de Turing y los sistemas formales. La motivación para "tirar" falta de sentido de los números cuando estamos usando otras numeraciones, entonces, es hacer de la traducción adecuadamente independientemente de la numeración que utilizamos.

Por el contrario, esto significa que no sólo debe estar preocupado por tirar la falta de sentido de los números si nos activamente desea trabajar con un no-surjective de numeración. En ese punto, ¿cómo debemos tratar la falta de sentido de los números de abajo a por qué queremos trabajar con una numeración en primer lugar, y sin que yo creo que no hay manera de adivinar cuál es la acción correcta sería.

La única objeción que ver a tirar la falta de sentido de los números es que hace varios equipos corresponden al mismo sistema. Yo no creo que eso sea un inconveniente, sin embargo, ya que el mismo sistema formal tendrá un montón de equivalente axiomatizations (mucho menos eficaz en las enumeraciones de los axiomas)! De hecho, la redundancia es a menudo una parte inevitable de la teoría de la computabilidad, e incluso hay situaciones donde la ausencia de redundancia es patológico.