# Consistência

Na lógica clássica dedutiva, uma teoria é chamada de consistente se não contém contradição. A ausência de contradição pode ser definida tanto em termos sintáticos como em termos semânticos. A definição semântica diz que uma teoria é consistente, se e somente se, tem um modelo, i.e. existe uma interpretação sob as quais todas as fórmulas são verdadeiras. Essa é a compreensão usada na lógica aristotélica, embora na lógica matemática contemporânea o termo usado é satisfatível. A definição sintática diz que uma teoria é consistente, se e somente se, não existe nenhuma fórmula P, tal que tanto P como sua negação são demonstráveis a partir dos axiomas da teoria do sistema dedutivo, as quais estão associados.
Se as definições semânticas e sintáticas são equivalentes para qualquer teoria formulada usando a lógica dedutiva, a lógica é chamada de completa. A completude da lógica proposicional foi provada por Paul Bernays em 1918 e Emil Post em 1921, enquanto a completude da lógica de predicados foi provada por Kurt Gödel em 1930 e a prova de consistência para aritmética restrita que serve para o axioma da indução matemática foi provada por Ackermann (1924), von Neumann (1927) e Herbrand (1931). Lógicas mais fortes, como a lógica de segunda ordem, não são completas.
Uma prova de consistência é uma prova matemática que uma teoria particular é consistente. O desenvolvimento precoce da teoria da prova matemática foi dirigida pelo desejo de fornecer provas finitas consistentes para toda a matemáticas, como parte do programa de Hilbert. O programa de Hilbert foi fortemente impactado pelos teoremas da incompletude, que mostraram que teorias de provas suficientemente fortes não podem provar suas próprias consistências (dado que elas sejam de fato consistentes).
Embora consistência possa ser provada por meio da teoria dos modelos, muitas vezes é feito simplesmente pelo método sintático, sem precisar de fazer nenhuma referência a algum modelo da lógica. O teorema da eliminação do corte (ou equivalentemente a normalização do cálculo subjacente, caso exista algum) implica a consistência do cálculo: desde de que não exista obviamente uma prova de corte livre da falsidade, no geral, não existe nenhuma contradição.

## Consistência e completude na aritmética e na teoria dos conjuntos

Em teorias da aritmética, como a aritmética de Peano, existe uma complexa relação entre a consistência e a completude de uma teoria. Uma teoria é completa se, para toda fórmula φ em um idioma, pelo menos um φ ou ¬ φ é uma consequência lógica dessa teoria.
A Aritmética de Presburger é um sistema axiomático para os números naturais sob a adição. Ela é tanto consistente, como completa.
Os teoremas da incompletude de Gödel mostram que qualquer teoria efetiva suficientemente forte da aritmética não pode ser completa e consistente ao mesmo tempo. O teorema de Gödel se aplica às teorias da Aritmética de Peano (PA) e à Aritmética primitiva recursiva (PRA), mas não para a aritmética de Presburger.
Além disso, o segundo teorema da incompletude de Gödel mostra que a consistência de uma teoria suficientemente eficaz da aritmética pode ser testada de uma maneira particular. Tal teoria é consistente se e somente se ele não prova uma sentença particular, chamada de sentença de Gödel da teoria, que é uma afirmação sustentada no fato de que uma teoria é de fato consistente. Assim a consistência de uma suficientemente forte, efetiva, consistente teoria da aritmética não pode nunca ser provada nesse sistema por si só. O mesmo resultado de teorias efetivas pode se descrever um fragmento suficientemente forte de aritmética – incluindo um conjunto de teorias como os axiomas de Zermelo-Fraenkel(ZF). Esses axiomas não podem provar as suas próprias sentenças de Gödel – fornecendo que elas são consistentes, que é o que se acredita.
Por causa da consistência de ZF não é provável em ZF, a noção mais fraca de consistência relativa é interessante em um conjunto de teorias (e em outros sistemas axiomáticos suficientemente expressivos). Se T é uma teoria e A é um axioma adicional, T + A é consistente. Se ambas A e ¬A sãos consistentes com T, então A é dita ser independente de T.

## Lógica de primeira ordem
### Notação

⊢ (símbolo de catraca) no contexto da lógica matemática, significa “dedutível de”. Ou seja, a ⊢ b é lido como: b é dedutível de a (em algum sistema formal) – veja Lista de símbolos lógicos. Em outros casos, o símbolo de catraca pode ter o significado de inferir; derivável de. Veja Tabela de símbolos matemáticos.

### Definição

Um conjunto de fórmulas $\Phi$ na lógica de primeira ordem é consistente (escrito como Con$\Phi$) se e somente se não existe nenhuma fórmula $\phi$ tal que $\Phi \vdash \phi$ e $\Phi \vdash \lnot \phi$. Caso contrário $\Phi$ é inconsistente e é escrito com Inc$\Phi$.
$\Phi$ é dito ser simplesmente consistente se e somente se para nenhuma fórmula $\phi$ de $\Phi$, ambas $\phi$ e a negação de $\phi$ são teoremas de $\Phi$.
$\Phi$ é dito ser absolutamente consistente se e somente se pelo menos uma fórmula de $\Phi$ não é um teorema de $\Phi$.
$\Phi$ é dito ser maximamente consistente se e somente se para toda fórmula , se Con($\Phi \cup \phi$) então $\phi \in \Phi$.
$\Phi$ é dito conter testemunhas se e somente se para toda fórmula na forma $\exists x\phi$ existe um termo $t$ tal que $(\exists x\phi \to \phi {t \over x})\in \Phi$. Veja Lógica de primeira ordem.

### Resultados básicos

* A fórmulas a seguir são equivalentes:
** Inc $\Phi$
** Para todo $\phi ,\;\Phi \vdash \phi .$
* Todo conjunto de fórmulas satisfazíveis é consistente, onde um conjunto de fórmulas $\Phi$ é satisfazível se e somente se existe um modelo ${\mathfrak {I}}$ tal que ${\mathfrak {I}}\vDash \Phi$.
* Para todo $\Phi$ e $\phi$
** se não $\Phi \vdash \phi$, então Con$\left(\Phi \cup \{\lnot \phi \}\right)$;
** se Con $\Phi$ e $\Phi \vdash \phi$, então Con$\left(\Phi \cup \{\phi \}\right)$;
** se Con $\Phi$, então Con$\left(\Phi \cup \{\phi \}\right)$ ou Con$\left(\Phi \cup \{\lnot \phi \}\right)$.
* Deixe $\Phi$ ser um conjunto de fórmulas maximamente consistente e conter testemunhas. Para todo $\phi$ e $\psi$:
** se $\Phi \vdash \phi$, então $\phi \in \Phi$,
** ou $\phi \in \Phi$ ou $\lnot \phi \in \Phi$,
** $(\phi \lor \psi )\in \Phi$se e somente se $\phi \in \Phi$ ou $\psi \in \Phi$,
** se $(\phi \to \psi )\in \Phi$ e $\phi \in \Phi$, então $\psi \in \Phi$,
** $\exists x\phi \in \Phi$ se e somente se existe um termo $t$ tal que $\phi {t \over x}\in \Phi$.

### Teorema de Henkin

Deixe $\Phi$ ser um conjunto de $S$-fórmulas maximamente consistente contendo testemunhas.
Defina uma relação binária $\sim$ no conjunto de $S$-termos tal que $t_{0}\sim t_{1}$ se e somente se $\;t_{0}\equiv t_{1}\in \Phi$; e deixe ${\overline {t}}\!$ denotar a classe de equivalência dos termos que contem $t\!$; e deixe $T_{\Phi }:=\{\;{\overline {t}}\;|\;t\in T^{S}\}$, onde $T^{S}\!$ é o conjunto de termos no conjunto de símbolos $S\!$.
Defina a $S\!$-estrutura ${\mathfrak {T}}_{\Phi }$ sobre$T_{\Phi }\!$ a estrutura de termos correspondente a $\Phi$ por:
* Para cada símbolo de relação $R$ de aridade $n$, $R\in S$, $R^{{\mathfrak {T}}_{\Phi }}{\overline {t_{0}}}\ldots {\overline {t_{n-1}}}$ se e somente se $\;Rt_{0}\ldots t_{n-1}\in \Phi$;
* Para cada símbolo de função $f$ de aridade $n$, $f\in S$, $f^{{\mathfrak {T}}_{\Phi }}({\overline {t_{0}}}\ldots {\overline {t_{n-1}}}):={\overline {ft_{0}\ldots t_{n-1}}}$;
* Para $c\in S$, $c^{{\mathfrak {T}}_{\Phi }}:={\overline {c}}$.
Deixe ${\mathfrak {I}}_{\Phi }:=({\mathfrak {T}}_{\Phi },\beta _{\Phi })$ ser a interpretação do termo associado com $\Phi$, onde $\beta _{\Phi }(x):={\bar {x}}$.
Para todo $\phi$, $\;{\mathfrak {I}}_{\Phi }\vDash \phi$ se e somente se $\;\phi \in \Phi$.

### Esboço da prova

Existem diversas coisas para serem verificadas. Primeiro, que $\sim$ é uma relação de equivalência. Depois, é preciso verificar que (1), (2) e (3) são bem definidas. Isso decorre do fato que $\sim$ é uma relação de equivalência e também é necessário uma prova que (1) e (2) são escolhas independentes dos representantes da classe de equivalência de $t_{0},\ldots ,t_{n-1}$. Finalmente, ${\mathfrak {I}}_{\Phi }\vDash \Phi$ pode ser verificado por indução nas fórmulas.

## Veja também

* Equiconsistência
* Problemas de Hilbert
* Segundo problema de Hilbert
* Jan Lukasiewicz
* Lógica paraconsistente