Saltar para o conteúdo
Topos Uranos
Português

O teorema da compacidade

Resumo

Uma dedução é uma sequência finita e só usa um número finito de premissas; a satisfação de um conjunto infinito de fórmulas, em contrapartida, exige uma só valoração que dê o valor 11 a infinitas fórmulas ao mesmo tempo, e nada em sua definição diz que baste examinar partes finitas. O teorema da compacidade afirma que basta: um conjunto de fórmulas é satisfatível se e somente se cada um de seus subconjuntos finitos o é. Esta aula o demonstra por um argumento semântico direto, sem passar pela dedução: fixam-se um a um os valores das variáveis v1,v2,…v_1, v_2, \ldots, conservando em cada passo o invariante de que todo subconjunto finito do conjunto continua sendo satisfatível por uma valoração que respeita o que já foi fixado; se nenhuma das duas escolhas possíveis o conservasse, a união das duas testemunhas finitas desse fracasso contradiria o invariante anterior, e no final cada fórmula fica satisfeita pelo lema da coincidência, porque tem um número finito de variáveis. Como as variáveis estão numeradas, a construção não precisa do axioma da escolha. Da compacidade seguem-se suas formas equivalentes (um conjunto é insatisfatível se e somente se alguma parte finita o é; uma fórmula é consequência de um conjunto se e somente se o é de alguma parte finita) e, com a completude para conjuntos finitos de premissas da aula anterior, a completude forte: Γ⊨φ\Gamma \models \varphi implica Γ⊢φ\Gamma \vdash \varphi para todo conjunto Γ\Gamma, donde a dedução e a consequência semântica coincidem sempre. A aula termina com aplicações combinatórias: a coloração de grafos infinitos a partir das colorações de suas partes finitas, as cotas finitas que se escondem nos enunciados infinitos e os limites do que um conjunto de fórmulas pode expressar.

Objetivos de aprendizagem

  1. Definir os conjuntos finitamente satisfatíveis e demonstrar o teorema da compacidade pela fixação sucessiva dos valores das variáveis, explicando o papel do invariante, do argumento das duas testemunhas e do lema da coincidência, e por que a construção não precisa do axioma da escolha.
  2. Enunciar, demonstrar e aplicar as formas equivalentes da compacidade, a da insatisfatibilidade e a da consequência, e passar de cada uma às outras.
  3. Deduzir a completude forte da compacidade, da completude para conjuntos finitos de premissas e da monotonicidade, e obter dela a coincidência da dedução com a consequência semântica e da consistência com a satisfatibilidade.
  4. Codificar em conjuntos de fórmulas problemas combinatórios sobre conjuntos infinitos (colorações, ordens, emparelhamentos) e resolvê-los com a compacidade, distinguindo o que o teorema garante do que não garante.

O que se usa das aulas anteriores

Esta aula trabalha quase inteiramente na semântica, e usa dela o seguinte. Uma valoração é uma função v ⁣:V→{0,1}v\colon V \to \{0, 1\} sobre o conjunto VV das variáveis v1,v2,v3,…v_1, v_2, v_3, \ldots, que se estende de um único modo a todas as fórmulas; uma valoração satisfaz um conjunto Γ\Gamma de fórmulas, v⊨Γv \models \Gamma, se dá o valor 11 a cada uma delas, e Γ\Gamma é satisfatível se alguma valoração o satisfaz e insatisfatível em caso contrário. Tudo isso está na aula sobre a semântica da lógica proposicional, junto com o instrumento central desta aula, o lema da coincidência: se duas valorações coincidem nas variáveis de φ\varphi, que formam um conjunto finito V(φ)V(\varphi), dão a φ\varphi o mesmo valor.

Da aula sobre consequência e equivalência semânticas usam-se a definição de Γ⊨φ\Gamma \models \varphi (toda valoração que satisfaz Γ\Gamma satisfaz φ\varphi), suas propriedades estruturais, em particular a monotonicidade (se Γ⊆Δ\Gamma \subseteq \Delta e Γ⊨φ\Gamma \models \varphi, então Δ⊨φ\Delta \models \varphi) e a quinta (um conjunto insatisfatível tem por consequência toda fórmula), e o teorema de consequência e insatisfatibilidade: Γ⊨φ\Gamma \models \varphi se e somente se Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} é insatisfatível. Da aula sobre as leis generalizadas de De Morgan e distributivas usa-se o lema do valor: ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i vale 11 se e somente se todos os seus termos valem 11, e ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i, se e somente se algum vale 11. Por último, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) é uma tautologia e ⊥:=¬⊤\bot := \neg\top, uma contradição.

Do lado da dedução, a aula sobre os sistemas dedutivos formais demonstrou a monotonicidade (Mon: se Γ⊆Δ\Gamma \subseteq \Delta e Γ⊢φ\Gamma \vdash \varphi, então Δ⊢φ\Delta \vdash \varphi) e a finitude (Fin: se Γ⊢φ\Gamma \vdash \varphi, algum subconjunto finito Γ0\Gamma_0 de Γ\Gamma cumpre Γ0⊢φ\Gamma_0 \vdash \varphi), e a aula sobre as quatro técnicas de dedução verificou que ambas valem no sistema do curso (os esquemas A1, A2 e A3, o modus ponens e a substituição da dupla negação, SDN), ao qual se refere doravante o símbolo ⊢\vdash. Finalmente, a aula sobre correção e completude demonstrou o teorema da correção (Γ⊢φ\Gamma \vdash \varphi implica Γ⊨φ\Gamma \models \varphi, para todo Γ\Gamma) e a completude para conjuntos finitos de premissas: se {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi, então {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.