|
In mathematical logic, satisfiability and validity are elementary concepts concerning interpretation . A formula is satisfiable with respect to a class of interpretations if it is possible to find an interpretation that makes the formula true[1]. A formula is valid if all such interpretations make the formula true. These notions can be relativised to satisfiability and validity within an axiomatic theory, where we count only interpretations that make all axioms true.
The negations of the concepts are unsatisfiability and invalidity, that is, a formula is unsatisfiable if none of the interpretations make the formula true, and invalid if some such interpretation makes the formula false.
These four concepts are related to each other in a manner exactly analogous to Aristotle's square of opposition.
The four concepts can be raised to apply to whole theories: a theory is satisfiable (valid) if one (all) of the interpretations make(s) each of the axioms of the theory true, and a theory is unsatisfiable (invalid) if all (one) of the interpretations make(s) each of the axioms of the theory false.
For classical logics, it is generally possible to reexpress the question of the validity of a formula to one involving satisfiability, because of the relationships between the concepts expressed in the above square of opposition. In particular φ is valid if and only if ¬φ is unsatisfiable, which is to say it isn't true that ¬φ is satisfiable.
In the case of classical propositional logic, satisfiability is decidable for propositional formulae. In particular, satisfiability is an NP-complete problem, and is one of the most intensively studied problems in computational complexity theory.
Satisfiability is a semidecidable property of formulae in first-order logic.
|
|
Wikis
Quiz
Search
