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.