> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/terms/satisfiability.md). # Satisfiability In mathematical logic, satisfiability and validity are elementary concepts of *semantics*. A formula is **satisfiable** if it is possible to find an interpretation (model) that makes the formula true. A formula is valid if all interpretations make the formula true. The opposites of these 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 4 concepts are related to each other in a manner exactly analogous to Aristotle's *square of opposition*. The 4 concepts can be raised to apply to whole theories: a theory is satisfiable (valid) if one (all) of the interpretations make each of the axioms of the theory true, and a theory is unsatisfiable (invalid) if all (one) of the interpretations make each of the axioms of the theory false. It is also possible to consider only interpretations that make all of the axioms of a second theory true. This generalization is commonly called *satisfiability modulo theories*. The question whether a sentence in propositional logic is satisfiable is *decidable*. The question whether a sentence in first-order logic is satisfiable is *not decidable*. In universal algebra and equational theory, the methods of term rewriting, congruence closure and unification are used to attempt to decide satisfiability. Whether a particular theory is decidable depends on many factors (such as whether the theory is variable-free). --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://mandober.gitbook.io/math-debrief/300-logic/terms/satisfiability.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.