Satisfiable formula
Contents
Definition
Let [ilmath]\mathscr{L} [/ilmath] be a first order language. Let [ilmath]A\in\mathscr{L}_F[/ilmath] be a formula of [ilmath]\mathscr{L} [/ilmath] and let [ilmath]\Gamma\subseteq\mathscr{L}_F[/ilmath] be a collection of formulas of [ilmath]\mathscr{L} [/ilmath]. If [ilmath](\mathbf{M},\sigma)[/ilmath] is a model of [ilmath]\mathscr{L} [/ilmath] such that[1]:
- [ilmath]A_{\mathbf{M}[\sigma]}=T[/ilmath] (where [ilmath]T[/ilmath] represents "true" as an element of set of truth values and [ilmath]A_{\mathbf{M}[\sigma]} [/ilmath] represents the semantics of the formula [ilmath]A[/ilmath])[Note 1]
Then the formula, [ilmath]A[/ilmath], is said to be satisfiable under the model [ilmath](\mathbf{M},\sigma)[/ilmath][1], or the model [ilmath](\mathbf{M},\sigma)[/ilmath] satisfies [ilmath]A[/ilmath][1], or that [ilmath]A[/ilmath] is satisfiable if the model is understood[1]; we denote this by:
- [ilmath]\mathbf{M}\models_\sigma A[/ilmath], if [ilmath]A[/ilmath] is a sentence then we may write just: [ilmath]\mathbf{M}\models A[/ilmath]
If for every formula, [ilmath]B[/ilmath], in the collection [ilmath]\Gamma[/ilmath] of formulas of [ilmath]\mathscr{L} [/ilmath] under the model [ilmath](\mathbf{M},\sigma)[/ilmath] we have [ilmath]\mathbf{M}\models_\sigma B[/ilmath] then[1]:
- We may say the formula set [ilmath]\Gamma[/ilmath] is satisfiable under the model [ilmath](\mathbf{M},\sigma)[/ilmath][1], the model [ilmath](\mathbf{M},\sigma)[/ilmath] satisfies [ilmath]\Gamma[/ilmath][1] or [ilmath]\Gamma[/ilmath] is satisfiable if the model is understood[1], we denote this:
- [ilmath]\mathbf{M}\models_\sigma\Gamma[/ilmath], if though every formula in [ilmath]\Gamma[/ilmath] is a sentence then we may write: [ilmath]\mathbf{M}\models\Gamma[/ilmath]
See next
Notes
- ↑ Recall that we use [ilmath]\doteq[/ilmath] for equality in the FOL, here we mean equals as in "LHS evaluates to the same thing as the RHS in the meta-language"
