# Teoria de modelos finitos

Teoria dos modelos finitos (TMF) é uma subárea da Teoria dos modelos (TM). A TM é um ramo da Lógica matemática que lida com a relação entre a linguagem formal (sintaxe) e suas interpretações (semântica). A TMF é uma restrição da TM para a interpretação de estruturas que tem um universo finito.
* Como muitos teoremas centrais da TM são inconsistentes quando restritos a estruturas finitas, a TMF é bem diferente da TM em seus métodos de prova. Os resultados desses teoremas centras da Teoria dos Modelos clássica que falham para estruturas finitas incluem o Teorema da compacidade, Teorema da completude de Gödel, e o método do ultraproduto para a Lógica de primeira ordem (LPO).
* Como a TM está muito relacionada à álgebra, a TMF se tornou um "efetivo mas não usual" instrumento na Ciência da computação. Em outras palavras: "Na história da Lógica matemática, sempre houve mais interesse nas estruturas infinitas... No entanto, os objetos que os computadores tratam são sempre finitos. Para estudar computação, nós precisamos de uma teoria de estruturas finitas." Assim, as principais áreas de aplicação da TMF são: Teoria da complexidade descritiva, Teoria do banco de dados (Banco de dados relacional) e teoria da linguagem formal.
* A TMF trata da separação de estruturas. A pergunta de motivação usual é se uma dada classe de estruturas pode ser descrita em uma linguagem dada. Por exemplo, todos os grafos cíclicos podem ser separados (dos não cíclicos) através de uma sentença da LPO? Isso também pode ser escrito como: A propriedade "cíclico" de um grafo é expressável na LPO?

## Desafios Básicos

Uma única estrutura sempre pode ser descrita de forma única na LPO. Alguns conjuntos finitos de estruturas também pode ser descritos em LPO. Contudo, essa lógica não é suficiente para descrever qualquer conjunto que contém estruturas infinitas.

### Caracterização de uma Estrutura Simples

Uma linguagem (assinatura) L é expressiva o suficiente para descrever uma estrutura finita S de uma única forma (ignorando isomorfismo)?

#### Problema

Uma estrutura como (1) na figura pode ser descrita na lógica de primeira ordem assim:
* Todo vértice tem uma aresta para outro vértice: $\forall _{x}\exists _{y}G(x,y).$
* Nenhum vértice tem uma aresta para ele mesmo: $\forall _{x,y}(G(x,y)\Rightarrow x\neq y).$
* Existe pelo menos um vértice que está conectado a todos os outros: $\exists _{x}\forall _{y}(x\neq y\Rightarrow G(x,y)).$
No entanto, essas propriedades não descrevem a estrutura unicamente (ignorando isomorfismo), uma vez que para a estrutura (1'), as propriedades acima também são satisfeitas, mas as estruturas (1) e (1') não são isomorfas.
Informalmente, a questão é se, adicionando algumas propriedades, essas propriedades descrevem exatamente (1) e não são válidas para nenhuma outra estrutura (exceto as isomorfas).

#### Abordagem

É sempre possível descrever uma estrutura finita precisamente por uma sentença da LPO. Esse princípio é ilustrado aqui para uma estrutura com uma relação binária $R(-,-)$ e sem constantes:
* Digamos que existem pelo menos $n$ elementos: $\varphi _{1}=\bigwedge _{i\neq j}\neg (x_{i}=x_{j})$
* Digamos que existem no máximo $n$ elementos: $\varphi _{2}=\forall _{y}\bigvee _{i}(x_{i}=y)$
* Verificar todos os elementos que pertencem a $R$: $\varphi _{3}=\bigwedge _{(a_{i},a_{j})\in R}R(x_{i},x_{j})$
* Verificar todos os elementos que não pertencem a $R$: $\varphi _{4}=\bigwedge _{(a_{i},a_{j})\notin R}\neg R(x_{i},x_{j})$
todos para a mesma tupla $x_{1}..x_{n}$, produzindo a sentença $\exists _{x_{1}}\dots \exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})$.

#### Extensão para um número fixo de estruturas

O método de descrever uma única estrutura através de uma sentença de lógica de primeira ordem pode ser facilmente estendido para um número fixo de estruturas. Uma única descrição pode ser obtida das disjunções das descrições de cada estrutura. Por exemplo, para duas estruturas, seria:
    $\exists _{x_{1}}...\exists _{x_{n}}(\varphi _{1}\land \varphi _{2}\land \varphi _{3}\land \varphi _{4})\lor \exists _{x_{1}}...\exists _{x_{n}}(\varrho _{1}\land \varrho _{2}\land \varrho _{3}\land \varrho _{4}).$

#### Extensão para uma estrutura infinita

Por definição, um conjunto contendo uma estrutura infinita sai da área de atuação da TMF. Note que estruturas infinitas nunca podem ser separadas das outras em lógica de primeira ordem por causa do Teorema da compacidade da Teoria dos Modelos clássica: Para todo modelo infinito, um modelo não-isomórfos pode ser descoberto, o qual tem exatamente as mesmas propriedades da descrição do anterior.
O exemplo mais famoso é o Teorema de Löwenheim–Skolem , que tem um modelo contável e não-padrão da aritmética.

### Caracterização de uma Classe de Estruturas

Uma linguagem (assinatura) L é expressiva o suficiente para descrever exatamente as estruturas finitas que tem possuem uma propriedade P em comum (ignorando isomorfismo)?

#### Problema

As descrições dadas até agora especificam o número de elementos do universo. Infelizmente a maioria dos conjuntos de estruturas não são restritos a um certo tamanho, como todos os grafos que são árvores, sejam eles conexos ou acíclicos. Contudo, para separar um número finito de estruturas, essa restrição é de grande importância.

#### Abordagem

Em vez de um método geral, a seguir está um esboço de uma metodologia para diferenciar as estruturas que podem e que não podem ser separadas.
1. A ideia central é que sempre que se quer ver se uma propriedade P pode ser expressa na lógica de primeira ordem, escolhem-se estruturas A e B, onde A tem P e B não. Se as sentenças são válidas para A e também para B, então P não pode ser expresso em lógica de primeira ordem (caso contrário, pode). Resumindo:
$A\in P,B\not \in P$ e $A\equiv B$
onde $A\equiv B$ é uma abreviação de $A\models \alpha \Leftrightarrow B\models \alpha$ para todas as sentenças α, e P representa a classe de estruturas com a propriedade P.
2. A metodologia considera contáveis muitos subconjuntos da linguagem, linguagens estas cuja união forma a própria linguagem. Por exemplo, para a lógica de primeira ordem, considere as classes [m] para cada m. Para cada m, a ideia central acima tem que ser mostrada. Isto é:
$A\in P,B\not \in P$ e $A\equiv _{m}B$
com um par $A,B$ para cada $m$ e α; (in ≡) de [m]. Isso pode ser apropriado para escolher as classes [m] que formam uma partição da linguagem.
3. Um jeito comum de definir [m] é pelo número de quantificadores qr(α) de uma fórmula ALFA. Por exemplo, para uma formula na Forma normal prenex, qr é simplesmente o total de quantificadores (se atentando ao fato de que uma fórmula pode ter um número diferente de quantificadores antes e depois de estar na forma Prenex). Visto isso, [m] pode ser definido com todas as fórmulas α da LPO com qr(α) ≤ m (ou, se é desejada uma partição, todas as fórmulas da LPO com qr(α) = m).
4. Assim, tudo se resume a mostrar que $A\models \alpha \Leftrightarrow B\models \alpha$ nos subconjuntos [m]. A principal abordagem aqui é usar a caracterização algébrica fornecida pelo Jogo de Ehrenfeucht–Fraïssé. Informalmente, são pegos isomorfismos parciais em A e B e depois, estendidos m vezes, para provar (ou não) $A\equiv _{m}B$, dependendo de quem ganhar o jogo.

#### Exemplo

Nós queremos mostrar que a propriedade do tamanho de uma estrutura (com Relação de ordem) A = (A, ≤) ser par não pode ser expressa em LPO.
1. A ideia é escolher um A ∈ PAR e um B ∉ PAR, onde PAR é a classe de todas as estruturas de tamanho par.
2. Nós começamos com 2 estruturas em ordem parcial A$_2$ e B$_2$ com universos A$_2$ = {1, 2, 3, 4} e B$_2$ = {1, 2, 3, 4, 5}. Obviamente A$_2$ ∈ PAR e B$_2$ ∉ PAR.
3. Para m = 2, nos podemos mostrar* que, em um Jogo de Ehrenfeucht–Fraïssé de 2-movimentos entre A$_2$ e B$_2$, o Duplicador (membro do jogo) sempre ganha, e assim A$_2$ e B$_2$ não podem ser separadas na PO[2], ou seja, A$_2$ $\models$ α; ⇔ B$_2$ $\models$ α; para todo α; ∈ FO[2].
4. Agora nós temos que escalar as estruturas com o aumento de m. Por exemplo, para m = 3 nós precisamos encontrar um A$_3$ e um B$_3$ onde o Duplicador sempre ganhe um jogo de 3-movimentos. Isso pode ser conseguido em A$_3$ = {1, ..., 8} e B$_3$ = {1, ..., 9}. Generalizando, nós podemos escolher A$_m$ = {1, ..., 2$^m$} e B$_m$ = {1, ..., 2$^m$+1}; para qualquer m, o Duplicador sempre ganha um jogo de m-movimentos entre essas duas estruturas*.
5. Assim, a classe PAR nas estruturas finitas e ordenadas não pode ser expressa na LPO.
(*) Os resultados do Jogo de Ehrenfeucht–Fraïssé foram omitidos, uma vez que não são a questão principal tratada aqui.

## Aplicações
### Teoria de Bancos de Dados

Um fragmento substancial do SQL (aplicado na Álgebra relacional) é baseado em LPO (mais precisamente, pode ser traduzido, em termos do teorema de Edgar Frank Codd, para cálculo do domínio relacional), como o exemplo a seguir ilustra: Imagine uma tabela de banco de dados "MULHERES" com as colunas "PRIMEIRO_NOME" e "ULTIMO_NOME". Isso corresponde a uma relação binária, digamos, G(p,u) com PRIMEIRO_NOME x ULTIMO_NOME. A busca (em LPO) {u : G('Renata', u)}, que retorna todos os últimos nomes de quem tem 'Renata' como primeiro nome, em SQL, seria assim:
Perceba que nós assumimos aqui que todos os últimos nomes aparecem apenas uma vez.
A seguir, queremos fazer uma coisa mais complexa. Além da tabela "MULHERES", temos agora a tabela "HOMENS" com as mesmas colunas. A busca (em LPO) é {(p,u) : ∃h ( G(p, u) ∧ B(h, l) )}, que em SQL é:
Perceba que para expressar o "∧", nós introduzimos o novo elemento de linguagem "IN", seguido de uma seleção. Isso torna a linguagem mais difícil de se aprender e de implementar. Essa é uma relação comum na criação de linguagens. Essa extensão da linguagem mostrada acima não é (nem de longe) a única. Por exemplo, outra maneira de escrever a mesma busca é:
A LPO é muito restritiva para algumas aplicações de banco de dados, por causa da falta de habilidade de expressar o Fecho transitivo. Esse fato propiciou a criação construções poderosas em termos de "linguagem de busca", como o recursive WITH (buscas recursivas em SQL) em SQL:1999. Lógicas mais expressivas têm então sido estudadas na Teoria dos Modelos Finitos por causa de sua relevância para a teoria dos bancos de dados e suas aplicações.

### Consultando e Buscando

Dados na forma de palavra não têm relações definidas. Dessa maneira, as estruturas lógicas de busca e consulta de texto podem ser expressas na Lógica proposicional, como em:
Perceba que os desafios na busca de texto são diferentes das de consulta num banco de dados, como por exemplo uma ordenação de resultados.

## História

* Trakhtenbrot 1950: falha no teorema da completude em LPO,
* Scholz 1952: caracterização de espectros em LPO,
* Fagin 1974: o conjunto de todas as propriedades expressáveis em lógica de segunda ordem existencial é precisamente a classe de complexidade NP,
* Chandra, Harel 1979/ 80: Extensão com ponto-fixo (fixed-point) da LPO para linguagem de consulta em bancos de dados capaz de expressar o fecho transitivo -> consultas como objetos centrais da TMF.
* Immerman, Vardi 1982: lógica de ponto-fixo (fixed point logic) em estruturas ordenadas captura PTIME -> complexidade descritiva (... Teorema de Immerman–Szelepcsényi)
* Ebbinghaus, Flum 1995: Primeiro livro de compreensão da "Teoria dos Modelos Finitos" (Finite Model Theory)
* Abiteboul, Hull, Vianu 1995: Livro "Fundamentos de Bancos de Dados" (Foundations of Databases)
* Immerman 1999: Livro "Complexidade Descritiva" (Descriptive Complexity)
* Kuper, Libkin, Paredaens 2000: Livro "Bancos de Dados baseados em Restrições" (Constraint Databases)
* Darmstadt 2005/ Aachen 2006: primeiro workshop internacional abordando "Teoria de Modelos Algorítmica" (Algorithmic Model Theory)

## Citações

* ↑ Fagin, Ronald (1993). «Finite-model theory – a personal perspective» (PDF). Theoretical Computer Science. 116: 3–31. doi:10.1016/0304-3975(93)90218-I
* ↑ Immerman, Neil (1999). Descriptive Complexity. New York: Springer-Verlag. p. 6. ISBN 0-387-98600-6