Localizando um modelo finito

Eu sei que a pergunta "uma fórmula de primeira ordem tem um modelo" é indecidível em geral.$\phi$

Alguém poderia me dar um link ou um livro que dê a resposta para modelos finitos. Se eu tiver uma fórmula de primeira ordem , é decidível se ϕ possui um modelo finito? Tenho certeza de que a pergunta é bem conhecida, mas nem sei por onde começar a busca por uma resposta. (Por exemplo, eu esperava que estivesse nos "Elementos da teoria dos modelos finitos" de Libkin, mas parece que não consigo encontrá-la.)$\phi$$\phi$

A segunda parte da minha pergunta é: Existem restrições conhecidas para que o problema seja decidido?

Por exemplo, o problema pode se tornar decidível para a fórmula de primeira ordem apenas com predicados monádicos. Ou quando temos predicado monádico mais uma relação sucessora. Mas não consigo imaginar um algoritmo para decidir se existe um modelo (finito) sobre essas restrições.

A primeira parte da sua pergunta é respondida pelo Teorema de Trakhtenbrot . A segunda parte é uma questão bastante grande. Dependendo da estrutura relacional em que você está trabalhando, várias soluções podem ser fornecidas. Por exemplo, se você estiver interessado em linguagens formais, o MSO sobre estruturas de palavras corresponde a idiomas regulares, e a lógica de correspondência ( veja isso ) corresponde a CFL e, portanto, tem seu problema de satisfação resolvível.

Você deve dar uma olhada no Capítulo 14 de Libkin, onde segmentos agradáveis ​​de FO têm um problema de satisfação decidível, de acordo com a quantidade de alternâncias de quantificadores permitidas.

Não sei a resposta para fragmentos arbitrários de FO. A lógica modal clássica e suas extensões têm várias propriedades de decidibilidade. Pelas traduções padrão, você obtém fragmentos da lógica clássica que compartilham essas propriedades.

1. Modal Logic e o fragmento invariante de bisimulação do FOL de duas variáveis.
2. CTL * e o fragmento invariante de bisimulação da lógica do caminho monádico.
3. O mu-calculus e o fragmento invariante da bimimulação da lógica monádica de segunda ordem.

Todas as lógicas modais acima são decidíveis e têm a propriedade de modelo finito. Outras lógicas com propriedades robustas de decidibilidade são o fragmento protegido de FO, o fragmento fracamente protegido e as lógicas de pontos fixos protegidos. Essas lógicas foram projetadas para transferir a essência das propriedades bem comportadas das lógicas modais para uma configuração lógica clássica. A lógica de ponto fixo guardado é decidível, mas não possui a propriedade de modelo finito.

O que se segue não deve ser entendido como nenhuma verdade magisterial do livro, mas apenas sugestões para sua própria pesquisa. Os editores são convidados a fazer as correções que entenderem.

Primeiro, sua pergunta é aparentemente interessante para a comunidade de Dedução automatizada. William McCune tem um programa chamado Mace4, que procura modelos finitos. Você pode querer ler a documentação que descreve como é feita.

Quanto às restrições decidíveis específicas, você pode querer observar o seguinte:

1. Casos em que o Universo Herbrand é finito. Uma maneira mecânica de verificar um subconjunto desses casos é verificar se a fórmula possui algum símbolo de função. Caso contrário, o Universo Herbrand é finito.

2. Casos em que a eliminação do quantificador é possível: theory.stanford.edu/~tingz/talks/qe.ps

Além das respostas já dadas: uma referência muito boa sobre a (in) decidibilidade de fragmentos da lógica de primeira ordem é o livro O problema clássico de decisão de Börger, Grädel e Gurevich