Teorema de Trakhtenbrot

En lógica , teoría de modelos finitos y teoría de computabilidad , el teorema de Trakhtenbrot (debido a Boris Trakhtenbrot ) establece que el problema de validez en lógica de primer orden sobre la clase de todos los modelos finitos es indecidible . De hecho, la clase de oraciones válidas sobre modelos finitos no es recursivamente enumerable (aunque sí es correcursivamente enumerable ).

El teorema de Trakhtenbrot implica que el teorema de completitud de Gödel (que es fundamental para la lógica de primer orden) no se cumple en el caso finito. También parece contra-intuitivo que sea "más fácil" que sea válido para todas las estructuras que sólo para las finitas.

El teorema se publicó por primera vez en 1950: "La imposibilidad de un algoritmo para el problema de decidibilidad en clases finitas". ^[1]

Formulación matemática

Seguimos las formulaciones como en Ebbinghaus y Flum ^[2]

Teorema

La satisfacibilidad de estructuras finitas no es decidible en la lógica de primer orden .

Es decir, el conjunto {φ | φ es una oración de lógica de primer orden que es satisfecha por todas las estructuras finitas} es indecidible.

Corolario

Sea σ un vocabulario relacional con al menos un símbolo de relación binaria.

El conjunto de σ-oraciones válidas en todas las estructuras finitas no es recursivamente enumerable .

Observaciones

1. Esto implica que el teorema de completitud de Gödel falla en lo finito ya que la completitud implica enumerabilidad recursiva.
2. De ello se deduce que no existe ninguna función recursiva f tal que: si φ tiene un modelo finito, entonces tiene un modelo de tamaño como máximo f(φ). En otras palabras, no existe ningún análogo efectivo del teorema de Löwenheim-Skolem en lo finito.

Prueba intuitiva

Esta prueba está tomada del Capítulo 10, sección 4, 5 de Lógica matemática de H.-D. Ebbinghaus.

Como en la prueba más común del Primer Teorema de Incompletitud de Gödel mediante el uso de la indecidibilidad del problema de detención , para cada máquina de Turing existe una sentencia aritmética correspondiente , efectivamente derivable de , tal que es verdadera si y solo si se detiene en la cinta vacía. Intuitivamente, afirma que "existe un número natural que es el código de Gödel para el registro de cálculo de en la cinta vacía que termina con la detención". ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$ ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$

Si la máquina se detiene en pasos finitos, entonces el registro completo de cómputo también es finito, y entonces hay un segmento inicial finito de números naturales tal que la oración aritmética también es verdadera en este segmento inicial. Intuitivamente, esto se debe a que en este caso, la demostración requiere las propiedades aritméticas de solo un número finito de números. ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle \phi _{M}}$

Si la máquina no se detiene en pasos finitos, entonces es falso en cualquier modelo finito, ya que no hay registro de cálculo finito que termine con una detención. ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$

Por lo tanto, si se detiene, es cierto en algunos modelos finitos. Si no se detiene, es falso en todos los modelos finitos. Por lo tanto, no se detiene si y solo si es cierto en todos los modelos finitos. ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$ ${\displaystyle \neg \phi _{M}}$

El conjunto de máquinas que no se detiene no es recursivamente enumerable, por lo que el conjunto de oraciones válidas sobre modelos finitos no es recursivamente enumerable.

Prueba alternativa

En esta sección exhibimos una prueba más rigurosa de Libkin. ^[3] Nótese en la afirmación anterior que el corolario también implica el teorema, y ​​esta es la dirección que demostramos aquí.

Teorema

Para cada vocabulario relacional τ con al menos un símbolo de relación binaria, es indecidible si una oración φ del vocabulario τ es finitamente satisfacible.

Prueba

De acuerdo con el lema anterior, podemos utilizar de hecho un número finito de símbolos de relación binaria. La idea de la prueba es similar a la prueba del teorema de Fagin, y codificamos las máquinas de Turing en lógica de primer orden. Lo que queremos demostrar es que para cada máquina de Turing M construimos una oración φ _M de vocabulario τ tal que φ _M es finitamente satisfacible si y solo si M se detiene en la entrada vacía, lo que es equivalente al problema de la detención y, por lo tanto, indecidible.

Sea M= ⟨Q, Σ, δ, q ₀ , Q _a , Q _r ⟩ una máquina de Turing determinista con una única cinta infinita.

• Q es el conjunto de estados,
• Σ es el alfabeto de entrada,
• Δ es el alfabeto de la cinta,
• δ es la función de transición,
• q ₀ es el estado inicial,
• Q _a y Q _r son los conjuntos de estados de aceptación y rechazo.

Dado que estamos tratando con el problema de detenerse en una entrada vacía, podemos suponer que wlog Δ={0,1} y que 0 representa un espacio en blanco, mientras que 1 representa algún símbolo de cinta. Definimos τ de modo que podamos representar los cálculos:

τ := {<, mín , T ₀ (⋅,⋅), T ₁ (⋅,⋅), (H _q (⋅,⋅)) _{(q ∈ Q)} }

Dónde:

• < es un orden lineal y min es un símbolo constante para el elemento mínimo con respecto a < (nuestro dominio finito estará asociado con un segmento inicial de los números naturales).
• T ₀ y T ₁ son predicados de cinta. T _i (s,t) indica que la posición s en el tiempo t contiene a i, donde i ∈ {0,1}.
• Los H _q son predicados de la cabeza. H _q (s,t) indica que en el momento t la máquina está en el estado q y su cabeza está en la posición s.

La oración φ _M establece que (i) <, min , T _i y H _q se interpretan como se indicó anteriormente y (ii) que la máquina finalmente se detiene. La condición de detención es equivalente a decir que H _q∗ (s, t) se cumple para algunos s, t y q∗ ∈ Q _a ∪ Q _r y después de ese estado, la configuración de la máquina no cambia. Las configuraciones de una máquina que se detiene (la que no se detiene no es finita) se pueden representar como una oración τ (finita) (más precisamente, una τ-estructura finita que satisface la oración). La oración φ _M es: φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ.

Lo desglosamos por componentes:

• α establece que < es un orden lineal y que min es su elemento mínimo
• γ define la configuración inicial de M: está en el estado q ₀ , la cabeza está en la primera posición y la cinta contiene solo ceros: γ ≡ H _{q 0} ( min , min ) ∧ ∀s T ₀ (s, min )
• η establece que en cada configuración de M, cada celda de cinta contiene exactamente un elemento de Δ: ∀s∀t(T ₀ (s, t) ↔ ¬ T ₁ (s, t))
• β impone una condición de consistencia básica sobre los predicados H _q : en cualquier momento la máquina está exactamente en un estado:

${\displaystyle \forall t\exists !s(\bigvee _{q\in Q}H_{q}(s,t))\land \neg \exists s\exists t(\bigvee _{q,q'\in Q,q\neq q}H_{q}(s,t)\land H_{q'}(s,t))}$

• ζ establece que en algún momento M se encuentra en un estado de detención:

${\displaystyle \exists s\exists t\bigvee _{q\in Q_{a}\cup Q_{r}}H_{q}(s,t)}$

• θ consiste en una conjunción de oraciones que establecen que T _i y H _q se comportan bien con respecto a las transiciones de M. Como ejemplo, sea δ(q,0)=(q',1, left) lo que significa que si M está en el estado q leyendo 0, entonces escribe 1, mueve la cabeza una posición a la izquierda y pasa al estado q'. Representamos esta condición mediante la disyunción de θ ₀ y θ ₁ :

${\displaystyle \theta _{0}\equiv \forall s\forall t(s\neq {\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{2}}$

Donde θ ₂ es:

${\displaystyle T_{1}(s,t+1)\land H_{q'}(s-1,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))}$

Y:

${\displaystyle \theta _{1}\equiv \forall s\forall t(s={\underline {min}}\land T_{0}(s,t)\land H_{q}(s,t))\to \theta _{3}}$

Donde θ ₃ es:

${\displaystyle T_{1}(s,t+1)\land H_{q'}(s,t+1)\land \forall s'(s\neq s'\to (\bigwedge _{i=0,1}T_{i}(s',t+1)\leftrightarrow T_{i}(s',t)))}$

s-1 y t+1 son abreviaturas definibles de primer orden para el predecesor y el sucesor según el orden <. La sentencia θ ₀ asegura que el contenido de la cinta en la posición s cambia de 0 a 1, el estado cambia de q a q', el resto de la cinta permanece igual y que el cabezal se mueve a s-1 (es decir, una posición a la izquierda), suponiendo que s no es la primera posición en la cinta. Si lo es, entonces todo es manejado por θ ₁ : todo es igual, excepto que el cabezal no se mueve a la izquierda sino que permanece en su lugar.

Si φ _M tiene un modelo finito, entonces un modelo que represente un cálculo de M (que comience con la cinta vacía (es decir, la cinta que contiene todos los ceros) y termine en un estado de detención). Si M se detiene en la entrada vacía, entonces el conjunto de todas las configuraciones de los cálculos de detención de M (codificados con <, T _i y H _q ) es un modelo de φ _M , que es finito, ya que el conjunto de todas las configuraciones de los cálculos de detención es finito. De ello se deduce que M se detiene en la entrada vacía si y solo si φ _M tiene un modelo finito. Dado que la detención en la entrada vacía es indecidible, también lo es la cuestión de si φ _M tiene un modelo finito (equivalentemente, si φ _M es finitamente satisfacible) también es indecidible (recursivamente enumerable, pero no recursiva). Esto concluye la prueba. ${\displaystyle {\mathcal {A}}}$

Corolario

El conjunto de oraciones finitamente satisfacibles es recursivamente enumerable.

Prueba

Enumerar todos los pares donde es finito y . ${\displaystyle ({\mathcal {A}},\phi )}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}\models \phi }$

Corolario

Para cualquier vocabulario que contenga al menos un símbolo de relación binaria, el conjunto de todas las oraciones finitamente válidas no es enumerable recursivamente.

Prueba

Del lema anterior, el conjunto de oraciones finitamente satisfacibles es recursivamente enumerable. Supongamos que el conjunto de todas las oraciones finitamente válidas es recursivamente enumerable. Como ¬φ es finitamente válido si y solo si φ no es finitamente satisfacible, concluimos que el conjunto de oraciones que no son finitamente satisfacibles es recursivamente enumerable. Si tanto un conjunto A como su complemento son recursivamente enumerables, entonces A es recursivo. De ello se deduce que el conjunto de oraciones finitamente satisfacibles es recursivo, lo que contradice el teorema de Trakhtenbrot.

Referencias

1. Trakhtenbrot, Boris (1950). "La imposibilidad de un algoritmo para el problema de decidibilidad en clases finitas". Actas de la Academia de Ciencias de la URSS (en ruso). 70 (4): 569–572.
2. Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995). Teoría de modelos finitos . Springer Ciencia + Medios comerciales. ISBN 978-3-540-60149-4.
3. Libkin, Leonid (2010). Elementos de la teoría de modelos finitos . Textos en informática teórica . ISBN 978-3-642-05948-3.

• Boolos, Burgess, Jeffrey. Computabilidad y lógica , Cambridge University Press, 2002.
• Simpson, S. "Teoremas de Church y Trakhtenbrot". 2001.[1]