Correção

Na lógica matemática, um sistema lógico possui a propriedade da correção se e somente se suas regras de inferências demonstram somente fórmulas que são válidas do ponto de vista de sua semântica. Geralmente, esta propriedade consiste na preservação da verdade por parte das regras do sistema.

Argumentos corretos

Um argumento é dito correto se e somente se:

1. O argumento é válido
2. Todas suas premissas são verdadeiras

Por exemplo,

Todos os homens são mortais.

Sócrates é um homem.

Logo, Sócrates é mortal.

O argumento é válido (pois a conclusão é verdadeira baseada nas premissas, isto é, a conclusão segue das premissas) e, uma vez que as premissas são, de fato, verdadeiras, o argumento é correto.

O seguinte argumento é válido mas não correto:

Todos os animais podem voar.

Porcos são animais.

Logo, porcos podem voar.

Uma vez que a primeira premissa é falsa, o argumento, embora válido, não é sólido.

Correção de sistemas lógicos

A correção está entre as propriedades mais fundamentais na lógica matemática. Uma propriedade da correção fornece a razão inicial para considerar um sistema lógico como desejável. A propriedade da completude significa que toda validade (verdade) é demonstrável. Juntos (correção e completude), estas propriedades implicam que todas e apenas validades são demonstráveis. A maioria das demonstrações de correção são triviais. Por exemplo, em um sistema axiomático, a demonstração da correção consiste na verificação da validade dos axiomas e de que as regras de inferência preservam a validade (ou a priopridade mais fraca, verdade). A maioria dos sistemas axiomáticos possuem somente a regra de modus ponens (e algumas vezes também a regra de substituição), então a demonstração da correção requer apenas a verificação da validade dos axiomas e uma regra de inferência. As propriedades de correção podem ser divididas em duas principais variantes: correção forte e fraca, onde a correção fraca é um caso particular da forte.

Correção fraca

A correção fraca de um sistema dedutivo é a propriedade segundo a qual toda sentença que é demonstrável no sistema dedutivo é também verdadeira sobre todas as interpretações ou modelos da teoria semântica para a linguagem sobre a qual a teoria está baseada. Em símbolos, quando S é o sistema dedutivo, L a linguagem junto com sua teoria semântica, e P uma sentença de L : ⊢ P, então também ⊨ P. Em outras palavras, um sistema é fracamente correto se cada um dos seus teoremas (isto é, formulas provadas a partir do conjunto vazio) é válido em cada estrutura da linguagem.

Correção forte

A correção forte de um sistema dedutivo é a propriedade segundo a qual qualquer sentença P de uma linguagem sobre a qual o sistema dedutivo está baseado que é derivável de um conjunto C de sentenças da linguagem também é consequência semântica de um conjunto C, no sentido de que qualquer modelo que faça todos os membros de C verdadeiros também fará os de P verdadeiros. Em símbolos, onde C é um conjunto de sentenças de L: se C ⊢ P, então também C ⊨ P. Repare que no enunciado da correção forte, quando C é vazio, nós temos o enunciado da correção fraca.

Relação com a completude

A recíproca da propriedade da correção é a propriedade da completude semântica. Um sistema dedutivo com uma teoria semântica é fortemente completo se qualquer sentença arbitrária "P" que é uma consequência semântica de um conjunto de sentenças Γ pode ser derivada deste mesmo conjunto no sistema dedutivo. Em símbolos: sempre quando Γ ⊨ P, então tem-se também Γ ⊢ P. A completude da lógica de primeira ordem foi pela primeira vez explicitamente estabelecida por Gödel, embora alguns dos principais resultados estivessem contidos em trabalhos anteriores de Skolem.

Informalmente, um teorema de correção para um sistema dedutivo expressa que todas as sentenças demonstráveis são verdadeiras. A completude estabelece que todas as sentenças verdadeiras são demonstráveis.

O primeiro teorema da incompletude de Gödel mostra que para as linguagens suficientes para fazer um certo montante de aritmética, não pode haver sistema dedutivo efetivo que seja completo no que diz respeito à interpretação pretendida do simbolismo daquela linguagem. Desse modo, nem todos os sistemas dedutivos corretos são completos neste sentido especial da completude, no qual as classes de modelos (a menos de isomorfismo) são restringidas à interpretação pretendida. A demonstração original da completude se aplica a todos os modelos clássicos, e não apenas a uma subclasse própria dos modelos pretendidos.