En lógica , teoría de modelos finitos y teoría de la computabilidad , el teorema de Trakhtenbrot (debido a Boris Trakhtenbrot ) establece que el problema de validez en la 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í recursivamente 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 es 'más fácil' que solo en las finitas.
El teorema se publicó por primera vez en 1950: "La imposibilidad de un algoritmo para el problema de decidabilidad en clases finitas". [1]
Formulación matemática
Seguimos las formulaciones como en Ebbinghaus y Flum [2]
Teorema
- La satisfacción 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 se puede satisfacer entre estructuras finitas} es indecidible.
Corolario
Sea σ un vocabulario relacional con al menos un símbolo de relación binario.
- El conjunto de oraciones σ válidas en todas las estructuras finitas no es recursivamente enumerable .
Observaciones
- Esto implica que el teorema de completitud de Gödel falla en lo finito ya que la completitud implica enumerabilidad recursiva.
- 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 efectivo al teorema de Löwenheim-Skolem en el finito.
Prueba intuitiva
Esta demostración está tomada del Capítulo 10, sección 4, 5 de Lógica matemática por 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 , de modo que es cierto 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 en la cinta vacía que termina con un alto ".
Si la maquina 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 cierto en este segmento inicial. Intuitivamente, esto se debe a que en este caso, demostrar requiere las propiedades aritméticas de sólo un número finito de números.
Si la maquina no se detiene en pasos finitos, entonces es falso en cualquier modelo finito, ya que no hay un registro de cálculo finito de que termina con una pausa.
Por tanto, si se detiene, es cierto en algunos modelos finitos. Si no se detiene, es falso en todos los modelos finitos. Entonces, no se detiene si y solo si es cierto en todos los modelos finitos.
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 el enunciado 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 binario, es indecidible si una oración φ de vocabulario τ es finitamente satisfactoria.
Prueba
De acuerdo con el lema anterior, de hecho podemos usar 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 probar es que para cada máquina de Turing M construimos una oración φ M de vocabulario τ tal que φ M es finitamente satisfactoria si y solo 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 0 , Q una , Q r ⟩ ser una máquina de Turing determinista con una sola 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 0 es el estado inicial,
- Q a y Q r son los conjuntos de estados de aceptación y rechazo.
Dado que estamos lidiando con el problema de detenerse en una entrada vacía, podemos asumir wlog 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 0 (⋅, ⋅), T 1 (⋅, ⋅), (H q (⋅, ⋅)) (q ∈ Q) }
Dónde:
min es un símbolo constante para el elemento mínimo con respecto a <(nuestro dominio finito se asociará con un segmento inicial de los números naturales). - T 0 y T 1 son predicados de cinta. T i (s, t) indica que la posición s en el tiempo t contiene i, donde i ∈ {0,1}.
- Los H q son predicados principales. H q (s, t) indica que en el momento t la máquina está en el estado q y su cabezal en la posición s.
La sentencia φ M establece que (i) <, min , T i 's y H q ' s se interpretan como anteriormente y (ii) que la máquina se detiene finalmente. La condición de parada es equivalente a decir que H q ∗ (s, t) se cumple durante 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 (lo que no se detiene no es finito) 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
min es su elemento mínimo - γ define la configuración inicial de M: está en el estado q 0 , el cabezal está en la primera posición y la cinta contiene solo ceros: γ ≡ H q 0 ( min , min ) ∧ ∀s T 0 (s, min )
- η establece que en cada configuración de M, cada celda de cinta contiene exactamente un elemento de Δ: ∀s∀t (T 0 (s, t) → ¬ T 1 (s, t))
- β impone una condición de consistencia básica a los predicados H q 's: en cualquier momento la máquina está en exactamente un estado:
- ζ establece que en algún momento M se encuentra en un estado de detención:
- θ consiste en una conjunción de oraciones que indican que T i y H q se comportan bien con respecto a las transiciones de M. Como ejemplo, sea δ (q, 0) = (q ', 1, izquierda) significando que si M está en el estado q leyendo 0, entonces escribe 1, mueve la cabeza una posición a la izquierda y entra en el estado q '. Representamos esta condición por la disyunción de θ 0 y θ 1 :
Donde θ 2 es:
Y:
Donde θ 3 es:
s-1 y t + 1 son abreviaturas definibles de primer orden para el predecesor y sucesor según el orden <. La oración θ 0 asegura que el contenido de la cinta en la posición s cambia de 0 a 1, el estado cambia de qa 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 θ 1 : todo es igual, excepto que la cabeza no se mueve hacia la izquierda sino que permanece quieta.
Si φ M tiene un modelo finito, entonces ese modelo representa un cálculo de M (que comienza con la cinta vacía (es decir, una cinta que contiene todos los ceros) y termina 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 <, Ti 'sy H q ' s) es un modelo de φ M , que es finito, ya que el conjunto de todas las configuraciones de detener los cálculos son finitas. De ello se deduce que M se detiene en la entrada vacía si f φ 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 satisfactorio) también es indecidible (recursivamente enumerable, pero no recursivo). Con esto concluye la prueba.
Corolario
- El conjunto de oraciones finitamente satisfactorias es recursivamente enumerable.
Prueba
Enumerar todos los pares dónde es finito y .
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 satisfactorias es recursivamente enumerable. Suponga que el conjunto de todas las oraciones finitamente válidas es recursivamente enumerable. Dado que ¬φ es finitamente válido si f φ no es finitamente satisfactorio, 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 satisfactorias es recursivo, lo que contradice el teorema de Trakhtenbrot.
Referencias
- ^ 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.
- ^ Ebbinghaus, Heinz-Dieter ; Flum, Jörg (1995). Teoría de modelos finitos . Springer Science + Business Media. ISBN 978-3-540-60149-4.
- ^ 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]