Satisfatibilidade

Na lógica matemática, satisfatibilidade e validade são conceitos elementares da semântica. Uma fórmula é satisfazível se é possível achar uma interpretação ( modelo) que torne a fórmula verdadeira. Uma fórmula é válida se todas as interpretações tornam a fórmula verdadeira. Os opostos deste conceito são insatisfatibilidade e invalidade, isto é, uma fórmula é insatisfazível se nenhuma das interpretações tornam a fórmula verdadeira, e inválida se alguma dessas interpretações tornam a fórmula falsa. Estes quatro conceitos estão relacionados uns aos outros de maneira exatamente análoga ao quadrado das oposições de Aristóteles.

Os quatro conceitos podem ser usados para aplicar todas as teorias: uma teoria é satisfazível (válida) se uma (todas) as interpretações torna(m) cada um dos axiomas da teoria verdade, e a teoria é insatisfazível (inválida) se todas (uma) as interpretações tornam(a) cada um dos axiomas da teoria falso.

Também é possível considerar apenas as interpretações que tornam todos os axiomas de uma segunda teoria verdadeiros. Esta generalização é comumente chamada satisfatibilidade módulo teorias.

A questão de saber se uma sentença em uma proposição lógica é satisfatíval é um problema de decisão. Em geral, a questão de saber se sentenças em lógica de primeira ordem são satisfeitas não é decidível. Na álgebra universal e teoria das equações, os métodos de reescrita de termos, fecho de congruência e unificação são usados para tentar decidir satisfatibilidade. Uma teoria particular é decidida ou não depende se a teoria é livre de variável ou está em outras condições.

Redução de validade para satisfatibilidade

Para a lógica clássica, geralmente é possível reexpressar a questão da validade da fórmula para uma envolvendo satisfatibilidade, por causa da relação entre os conceitos expressados acima, no quadrado das oposições. Em particular φ é válido se e somente se ¬φ é insatisfazível, o que significa dizer que não é verdade que ¬φ é satisfazível. Por outro lado, φ é satisfazível se e somente se ¬φ é inválida.

Para lógica sem negação, tal como o cálculo proposicional positivo, as questões de validade e satisfatibilidade não devem estar relacionadas. No caso do cálculo proposicional positivo, o problema da satisfatibilidade é trivial, pois toda fórmula é satisfazível, enquanto o problema da validade é co-NP completo.

Satisfatibilidade proposicional

Principal Propositional_satisfiability

No caso da lógica proposicional clássica, satisfatibilidade é decidível para fómulas proposicionais. Em particular, satisfatibilidade é um problema NP-completo, e é um dos problemas mais intensamente estudados na teoria da complexidade computacional.

Satisfatibilidade em lógica de primeira ordem

Satisfatibilidade é indecidível e de fato nem sequer é uma propriedade das fómulas na lógica de primeira ordem (LPO), Este fato tem a ver com a indecidibilidade do problema da validade para LPO. A validade universal da fórmula é um problema semi-decidível. Se satisfatibilidade também fosse um problema semi-decidível, então o problema da exsitência de contramodelos deveria ser também (uma fórmula tem contramodelos se sua negação é satisfeita). Então o problema da validade lógica seria decidível, o que contradiz a tese de Church-Turing.

Satisfatibilidade na teoria dos modelos

Na teoria dos modelos, uma formula atômica é satisfazível se existe uma coleção de elementos da estrutura que tornam a fórmula verdadeira. Se A é uma estrutura, φ é uma fórmula, e a é uma coleção de elementos, tirados da estrutura, que satisfazem φ. Comumente é escrito assim

A ⊧ φ [a]

Se φ não possui variáveis, isto é, φ é uma sentença atômica, e é satisfeita por A, então escreve-se

A ⊧ φ

Neste caso, pode se dizer também que A é um modelo para φ, ou que φ é verdadeiro em A. Se T é uma coleção de sentenças atômicas (uma teoria) satisfeita por A, se escreve

A ⊧ T

Referências

• Boolos and Jeffrey, 1974. Computability and Logic. Cambridge University Press.