Na lógica, na teoria dos modelos finitos e na teoria da computabilidade, o teorema de Trakhtenbrot (devido a Boris Trakhtenbrot) estabelece que o problema da validade na lógica de primeira ordem sobre a classe de todos os modelos finitos é indecidível. De fato, a classe das sentenças válidas sobre modelos finitos não é recursivamente enumerável (embora seja co-recursivamente enumerável).
O teorema de Trakhtenbrot implica que o teorema da completude de Gödel (fundamental para a lógica de primeira ordem) não se sustenta no caso finito. Além disso, parece contraintuitivo que a validade sobre todas as estruturas seja "mais fácil" do que apenas sobre as finitas.
O teorema foi publicado pela primeira vez em 1950: "A Impossibilidade de um Algoritmo para o Problema da Decidibilidade em Classes Finitas".
O teorema está relacionado ao resultado de Alonzo Church de que o conjunto de fórmulas válidas na lógica de primeira ordem não é decidível (contudo, esse conjunto é semidecidível).
Formulação matemática Seguem-se as formulações conforme apresentadas por Ebbinghaus e Flum.
Teorema A satisfatibilidade para estruturas finitas não é decidível na lógica de primeira ordem. Isto é, o conjunto é indecidível. (p. 127, Teo. 7.2.1 em )
Corolário Seja um vocabulário relacional com pelo menos um símbolo de relação binária. O conjunto das -sentenças válidas em todas as estruturas finitas não é recursivamente enumerável.
Observações Isso implica que o teorema da completude de Gödel falha no caso finito, uma vez que a completude acarreta a enumerabilidade recursiva. Segue-se que não existe nenhuma função recursiva tal que: se possui um modelo finito, então possui um modelo de tamanho no máximo . Em outros termos, não existe um análogo efetivo ao teorema de Löwenheim-Skolem no domínio finito.
Demonstração A demonstração nesta seção segue a abordagem de Libkin. O corolário apresentado como parte da formulação matemática também acarreta o teorema, sendo esta a direção demonstrada aqui.
Teorema Para todo vocabulário relacional com pelo menos um símbolo de relação binária, é indecidível se uma sentença de vocabulário é finitamente satisfatível.
Demonstração De acordo com o lema anterior, pode-se, de fato, utilizar um número finito de símbolos de relação binária. A ideia da demonstração é análoga à do teorema de Fagin, codificando máquinas de Turing na lógica de primeira ordem. O objetivo é demonstrar que, para toda máquina de Turing , constrói-se uma sentença de vocabulário tal que é finitamente satisfatível se e somente se para com a entrada vazia, o que equivale ao problema da parada e, portanto, é indecidível.
Seja uma máquina de Turing determinística com uma única fita infinita: é o conjunto de estados, é o alfabeto de entrada, é o alfabeto da fita, é a função de transição, é o estado inicial, e são os conjuntos de estados de aceitação e de rejeição, respectivamente.
Como se trata do problema da parada com entrada vazia, pode-se assumir sem perda de generalidade que e que representa o símbolo em branco, enquanto representa um símbolo de fita. Define-se de modo a poder representar computações:
onde: é uma ordem linear e é um símbolo de constante para o elemento mínimo em relação a (o domínio finito será associado a um segmento inicial dos números naturais). e são predicados da fita. indica que a posição no instante contém , onde . Os são predicados do cabeçote. indica que no instante a máquina está no estado e seu cabeçote está na posição .
A sentença estabelece que (i) , , os e os são interpretados conforme acima e (ii) a máquina eventualmente para. A condição de parada equivale a dizer que é válida para algum , e , e após esse estado a configuração da máquina não se altera. As configurações de uma máquina que para (a não parada não é finita) podem ser representadas como uma -estrutura finita que satisfaz a sentença. A sentença é dada por: .
Decompondo-a em seus componentes: estabelece que é uma ordem linear e que é o seu elemento mínimo; define a configuração inicial de : ela está no estado , o cabeçote está na primeira posição e a fita contém apenas zeros:
estabelece que, em toda configuração de , cada célula da fita contém exatamente um elemento de :
impõe uma condição básica de consistência sobre os predicados : em qualquer instante, a máquina está em exatamente um estado:
estabelece que, em algum momento, atinge um estado de parada:
consiste em uma conjunção de sentenças afirmando que os e os comportam-se de acordo com as transições de . Por exemplo, seja , significando que, se está no estado lendo , ela escreve , move o cabeçote uma posição para a esquerda e passa para o estado . Representa-se essa condição pela conjunção de e :
onde é:
e:
onde é:
e são abreviações definíveis em primeira ordem para o predecessor e o sucessor de acordo com a ordenação . A sentença assegura que o conteúdo da fita na posição muda de 0 para 1, o estado muda de para , o restante da fita permanece inalterado e o cabeçote se move para (isto é, uma posição para a esquerda), assumindo que não é a primeira posição da fita. Se for a primeira posição, a situação é tratada por : tudo ocorre da mesma forma, exceto que o cabeçote não se move para a esquerda, permanecendo no mesmo lugar.
Se possui um modelo finito, então tal modelo representa uma computação de (que começa com a fita vazia — isto é, contendo apenas zeros — e termina em um estado de parada). Se para com a entrada vazia, então o conjunto de todas as configurações da computação de parada de (codificado com , os e os ) é um modelo de , o qual é finito, visto que o conjunto de todas as configurações de uma computação que para é finito. Segue-se que para com a entrada vazia se e somente se possui um modelo finito. Como a parada com entrada vazia é indecidível, a questão de se possui um modelo finito (equivalentemente, se é finitamente satisfatível) também é indecidível (recursivamente enumerável, mas não recursiva). Isso conclui a demonstração.
Corolário O conjunto de sentenças finitamente satisfatíveis é recursivamente enumerável.
Demonstração Enumere todos os pares onde é finito e .
Corolário Para qualquer vocabulário contendo pelo menos um símbolo de relação binária, o conjunto de todas as sentenças finitamente válidas não é recursivamente enumerável.
Demonstração Pelo lema anterior, o conjunto de sentenças finitamente satisfatíveis é recursivamente enumerável. Suponha que o conjunto de todas as sentenças finitamente válidas seja recursivamente enumerável. Como é finitamente válida se e somente se não for finitamente satisfatível, conclui-se que o conjunto das sentenças que não são finitamente satisfatíveis é recursivamente enumerável. Se tanto um conjunto quanto seu complemento forem recursivamente enumeráveis, então é recursivo. Segue-se que o conjunto das sentenças finitamente satisfatíveis seria recursivo, o que contradiz o teorema de Trakhtenbrot.
Ver também
Teoria de modelos finitos
Referências
Categoria:Teoria dos modelos finitos Categoria:Teoria da computabilidade Categoria:Problemas indecidíveis Categoria:Teoremas nos fundamentos da matemática