===== Teorema da Compacidade =====

Esta lista é um roteiro para provar um resultado bastante importante em lógica de primeira ordem, o Teorema da Compacidade:

Todo conjunto finitamente modelável de fórmulas é modelável

<WRAP info>
Dizemos que um conjunto $\Sigma$ de sentenças é modelável se existe $\mathcal{M}$ modelo tal que $\mathcal{M} \models \Sigma$.

Um conjunto $\Sigma$ de sentenças será finitamente modelável se todo subconjunto finito de $\Sigma$ for modelável

Um conjunto (finitamente) modelável será maximal se, adicionando outra sentença qualquer sentença, o conjunto deixa de ser 
</WRAP>

**~~#~~** Todo conjunto finitamente modelável pode ser estendido a um conjunto finitamente modelável máximal. <wrap tip>[[dica:compact1|Dica]]</wrap>

**~~#~~** Seja $\Sigma$ finitamente modelável maximal. Para todo $\Delta$ conjunto de sentenças e $\varphi, \psi$ sentenças, mostre que:

**~~#.#~~** $\Delta$ finito, $\Delta \models \varphi, \, \Delta \subset \Sigma \Rightarrow \varphi \in \Sigma$ (note que $\varphi \in \Sigma$ e $\Sigma \models \varphi$ são equivalentes)

**~~#.#~~** $\varphi \land \psi \in \Sigma \Leftrightarrow \varphi, \, \psi \in \Sigma$

**~~#.#~~** $\neg \varphi \in \Sigma \Leftrightarrow \varphi \notin \Sigma$

**~~#~~** Todo conjunto finitamente modelável $\Sigma$ sobre um vocabulário $\mathcal{L}$ pode ser estendido a um conjunto finitamente modelável $\Sigma '$ sobre um vocabulário $\mathcal{L}'$ expansão simples de $\mathcal{L}$ com a seguinte propriedade:
$$ (\exists x \varphi(x)) \in \Sigma \Rightarrow \exists \mathbf{c} \in \mathcal{L}' \, \varphi(\mathbf{c}) \in \Sigma '$$

**~~#~~** Chamamos a propriedade descrita no exercício acima de Propriedade Henkin. Mostre que, dado um vocabulário $\mathcal{L}$, existe uma expansão simples $\mathcal{L}'$ de $\mathcal{L}$ tal que todo conjunto finitamente modelável de sentenças em $\mathcal{L}$ pode ser estendido a um conjunto finitamente modelável maximal Henkin em $\mathcal{L}'$

**~~#~~** Seja $\Sigma$ um conjunto finitamente modelável maximal Henkin. Defina uma relação de equivalência nos termos livres de variáveis de $\mathcal{L}'$ a seguir:
$$s \sim t :\equiv (s=t) \in \Sigma$$
$$\vert t \vert := \{ s \, : \, s \sim t \}$$

**~~#.#~~** Prove que de fato $\sim$ é uma relação de equivalência

**~~#.#~~** Construa um modelo $\mathcal{A}$ de modo que $t^{\mathcal{A}}=\vert t \vert$. Mostre que $f^{\mathcal{A}}(\vert t_1 \vert,...,\vert t_n \vert) = \vert f(t_1,...,t_n) \vert$

**~~#.#~~** Use indução sobre sentenças para mostrar que, sendo $\varphi$ uma sentença, $\mathcal{A} \models \varphi \Leftrightarrow \varphi \in \Sigma$

**~~#.#~~** Conclua que todo conjunto finitamente modelável Henkin é modelável e, portanto, segue o Teorema da Compacidade.