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 en 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í 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 contrario a la intuición que ser válido en todas las estructuras sea "más fácil" que sólo en 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 lógica de primer orden .

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

Corolario

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

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

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 una 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 un análogo eficaz 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 hay una oración aritmética correspondiente , efectivamente derivable de , tal que es verdadera si y solo si se detiene en la cinta vacía. Intuitivamente, afirma "existe un número natural que es el código de Gödel para el registro de cálculo de la cinta vacía que termina con una parada". ${\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 de cálculo completo también es finito, entonces hay un segmento inicial finito de los números naturales tal que la oración aritmética también es cierta en este segmento inicial. Intuitivamente, esto se debe a que, en este caso, la demostración requiere las propiedades aritméticas de sólo 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 un registro de cálculo finito que termine con la detención. ${\displaystyle M}$ ${\displaystyle \phi _{M}}$ ${\displaystyle M}$

Por 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 sólo 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] Tenga en cuenta 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 satisfactoria.

Prueba

Según el lema anterior, de hecho podemos utilizar 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 satisfactible si y sólo si M se detiene en la entrada vacía, lo que es equivalente al problema de 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 detenernos en una entrada vacía, podemos suponer que Δ={0,1} y que 0 representa un espacio en blanco, mientras que 1 representa algún símbolo de cinta. Definimos τ para que podamos representar cálculos:

τ := {<, min , 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 a 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 momento t contiene i, donde i ∈ {0,1}.
• Los H _q son predicados principales. H _q (s,t) indica que en el instante t la máquina está en el estado q, y su cabezal 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 eventualmente se detiene. La condición de parada equivale 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 ₀ , el cabezal está en la primera posición y la cinta contiene sólo 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 a los predicados H _q 's: 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 punto M está en estado de parada:

${\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 indican que T _i 's y H _q 's se comportan bien con respecto a las transiciones de M. Como ejemplo, sea δ(q,0)=(q',1, left) que significa que si M está en el estado q leyendo 0, entonces escribe 1, mueve la cabeza una posición hacia 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), asumiendo que s no es la primera posición en la cinta. Si es así, entonces todo es manejado por θ ₁ : todo es igual, excepto que la cabeza no se mueve hacia la izquierda sino que permanece quieta.

Si φ _M tiene un modelo finito, entonces dicho modelo representa un cálculo de M (que comienza con la cinta vacía (es decir, la cinta que contiene todos ceros) y termina en un estado detenido). 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 <, Ti _y H _q ) es un modelo de φ _M , que es finito, ya que el conjunto de todas las configuraciones de cálculos detenidos son finitas. De ello se deduce que M se detiene en la entrada vacía si y sólo si φ _M tiene un modelo finito. Dado que detenerse en la entrada vacía es indecidible, también lo es la cuestión de si φ _M tiene un modelo finito (de manera equivalente, si φ _M es finitamente satisfactible) también es indecidible (recursivamente enumerable, pero no recursiva). Esto concluye la prueba. ${\displaystyle {\mathcal {A}}}$

Corolario

El conjunto de oraciones finitamente satisfactibles es recursivamente enumerable.

Prueba

Enumere todos los pares donde sea 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 recursivamente enumerable.

Prueba

Del lema anterior, el conjunto de oraciones finitamente satisfactibles es recursivamente enumerable. Supongamos que el conjunto de todas las oraciones finitamente válidas es recursivamente enumerable. Dado que ¬φ es finitamente válido si y sólo si φ no es finitamente satisfactible, concluimos que el conjunto de oraciones que no son finitamente satisfactibles 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 satisfactibles 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 de 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]