¿Es una máquina de Turing un sistema formal?

Ok, esta es mi mejor conjetura.

La posición de la cabeza de la máquina Turing, su estado y la parte finita sobreescrita de su cinta se pueden concatenar en una cadena finita. Esta cadena es un teorema (o axioma si es la configuración inicial). La regla de transición de la máquina de Turing, cuando se aplica, produce una nueva tupla de posición-estado-cinta, que es un nuevo teorema. Las reglas implícitas de inferencia del sistema formal isomórfico podrían ser declaraciones como “Si positionX-stateX-tapeX, positionY-stateY-tapeY”, donde X e Y indexan configuraciones específicas. El número de reglas de inferencia sería enorme (posiblemente ilimitado), pero técnicamente parece ser un sistema formal.

Esto todavía deja un enigma de cómo representar la aritmética. Tal vez esto podría hacerse, como sugiere Suber, interpretando grupos de 8 bits como caracteres, incluidos los dígitos (0-9), +, =, etc. Una configuración de cinta particular podría decir, por ejemplo, 2 + 3 = 5. Pero no sería el caso de que cada configuración de cinta sucesiva sería una expresión aritmética válida, especialmente porque la máquina Turing solo puede cambiar un bit a la vez. Tal vez los símbolos en la cinta podrían tomar todos los caracteres ASCII como primitivas de símbolos, no solo 0 y 1, pero aun así no creo que cada estado intermedio de la cinta sea una expresión válida.

La máquina de Turing también tiene las reglas de inferencia en su definición. Esto lo hace formal. Ver Wikipedia