¿Cómo se representa el poder de 10 en la teoría de números tipográficos de Hofstadter?

Esto se da como un ejercicio en Gödel, Escher, Bach. Es divertido e instructivo hacer ejercicio por ti mismo, así que deja de leer si no quieres spoilers.

Hofstadter escribió:

Curiosamente, este requiere una gran inteligencia para representar en nuestra notación. Le advierto que lo intente solo si está dispuesto a pasar horas y horas en él, ¡y si conoce bastante teoría de números!

De hecho, las soluciones típicas que puede encontrar en Internet involucran maquinaria como el Teorema del resto chino. Pero tal teoría de números avanzada no es realmente necesaria.

Comencemos con algunos problemas más fáciles. Un número es una potencia de 2 cuando no tiene factores impares mayores que 1:

  1: = S0
 2: = S1
 Divide (d, a): = ∃b: a = (d⋅b)
 PowerOfTwo (a): = ~ ∃b: Divide (S (2⋅Sb), a)

Podemos generalizar esto a los poderes de cualquier primo [matemáticas] p [/ matemáticas]. Un número es una potencia de un primo [matemático] p [/ matemático] cuando todos sus factores mayores que [matemático] 1 [/ matemático] son ​​divisibles por [matemático] p [/ matemático]:

  PowerOfPrime (a, p): = ∀b: ⟨Divides (SSb, a) ⊃ Divides (p, SSb)⟩

Tenga en cuenta que si [math] a \ ne 1 [/ math], esto implica automáticamente que [math] p [/ math] es primo.

Sin embargo, no podemos usar este tipo de idea directamente para definir potencias de 10. Podríamos obtener potencias de 2 veces potencias de 5, pero no tendríamos una forma obvia de asegurar que sus exponentes sean los mismos.

En cambio, comencemos con la definición recursiva de potencias de 10. Un número es una potencia de 10 cuando es igual a 1 o igual a 10 veces otra potencia positiva de 10 (positiva, para excluir [matemáticas] 0 = 0 \ cdot 10 [/ math]):

  10: = SSSSSSSSSS0
 PowerOfTen (a) “: =”
   ⟨A = 1 ∨ ∃b: ⟨PowerOfTen (Sb) ∧ a = (Sb⋅10) ⟩⟩

Por supuesto, TNT no tiene definiciones recursivas (por una buena razón, sin restricciones cuidadosas, algunas definiciones recursivas serían contradictorias). Entonces, tenemos que formalizar esto de alguna manera. Podemos traducirlo al lenguaje de la teoría de conjuntos. Un número es una potencia de 10 cuando es miembro de un conjunto de [math] s [/ math] de naturales, de modo que cada miembro de [math] s [/ math] es igual a 1 o igual a 10 veces otro miembro positivo de [math] s [/ math]:

  PowerOfTen (a) “: =”
   ∃s: ⟨a ∈ s ∧ ∀b: ⟨b ∈ s ⊃ ⟨b = 1 ∨ ∃c: ⟨Sc ∈ s ∧ b = (Sc⋅10) ⟩⟩⟩⟩

Todavía no podemos escribir eso en TNT porque TNT no le permite hablar sobre conjuntos de naturales, solo sobre naturales. De hecho, los sistemas que le permiten hablar sobre conjuntos arbitrarios de naturales son estrictamente más poderosos que TNT, ya que hay más conjuntos de naturales que naturales. Pero para nuestros propósitos, es suficiente hablar sobre conjuntos finitos de productos naturales. Resulta que podemos diseñar una forma bastante simple de hablar sobre conjuntos finitos de naturales en TNT.

En particular, dado que ya somos tan buenos para hablar sobre las potencias de un primo [math] p [/ math], es posible que se dé cuenta de que una posible representación para conjuntos finitos es usar los dígitos de una base [math] p [/ math ] número ! Como sabemos que hay infinitos números primos, siempre podremos encontrar una base [math] p [/ math] lo suficientemente grande como para poder representar los elementos de un conjunto usando los dígitos [math] 0, \ ldots, p – 1 [/ matemáticas]. Podemos decir que [math] a <p [/ math] es un dígito base- [math] p [/ math] de [math] s [/ math] si uno puede escribir [math] s = p ^ {k + 1} q + p ^ ka + r [/ math] para algunos [math] r <p ^ k [/ math]:

  Menos (a, b): = ∃c: (a + Sc) = b
 IsDigit (a, s, p): =
   ⟨Menos (a, p) ∧ ∃b: ⟨PowerOfPrime (b, p) ∧
       ∃q: ∃r: ⟨Menos (r, b) ∧ s = ((((p⋅q) + a) ⋅b) + r) ⟩⟩⟩

Ahora solo traducimos a IsDigit para formalizar nuestra definición de teoría de conjuntos de PowerOfTen . (Como [math] 0 [/ math] es un dígito de cada número, en realidad agregamos 1 a cada número cuando lo convertimos en un dígito).

  PowerOfTen (a): =
   ∃p: ∃s: ⟨IsDigit (Sa, s, p) ∧
       ∀b: ⟨IsDigit (Sb, s, p) ⊃ ⟨b = 1 ∨ ∃c: ⟨IsDigit (SSc, s, p) ∧ b = (Sc⋅10) ⟩⟩⟩⟩