View source for Satisfiability

{{MSC|68P05}} 

{{TEX|done}}

Many notions of logics (like logical consequence) can only be formulated if one is able to assign truth value to logical objects.  This can be done canonically for sentences using the technique of recursive [[Evaluation|evaluation]]. Generalizing the approach to [[Formula|formulas]] $p$, which may contain free variables in contrast to sentences, will however require the removal of ambiguities by assigning concrete objects to the free variables of $p$ at first. This leads to the concept of satisfiability, which defines the truth value of a formula relative to a given variable [[Assignement|assignment]].

==Definition of Satisfiability==

Let $p\in L(\Sigma,X)$ be a formula over a [[Signature (Computer Science)|signature]] $\Sigma$ and a set $X$ of variables and let $v\in B(A,X)$ be an assignement in a [[Sigma-algebra (Computer Science)|$\Sigma$-algebra]] $A$. Then $v$ <i>satisfies</i> $p$ in $A$, written as $v\models p[v]$ or $A\models p[v]$ or $A,v\models p[v]$, if it holds recursively
* $v\models r(t_1,\ldots,t_n) :\Longleftrightarrow (t_1[v],\ldots,t_n[v]) \in r$ for a relation $r$ like equality
* $v\models (\neg p)[v] :\Longleftrightarrow v\models \neg (p[v])$
* $v\models (p_1 \vee p_2)[v] :\Longleftrightarrow v\models (p_1[v] \vee p_2[v])$
* $v\models (p_1 \wedge p_2)[v] :\Longleftrightarrow v\models (p_1[v] \wedge p_2[v])$
* $v\models \big(\forall x_1\in X_{s_1},\ldots,x_n\in X_{s_n}\colon r(x_1,\ldots,x_n)[v]\big) :\Longleftrightarrow v\models \big(\forall a_1\in s_1^A,\ldots,a_n\in s_n^A\colon r(x_1,\ldots,x_n)[v(x_1\leftarrow t_1,\ldots,x_n\leftarrow t_n)]\big)$.  The expression $v(x_1\leftarrow t_1,\ldots,x_n\leftarrow t_n)$ denotes an assignment function $v$ changed at variables $x_i$ to $t_i$.
A set $\Phi \subseteq L(\Sigma,X)$ of formulas is called <i>satisfiable</i> iff there exists an assignement $v\in B(A,X)$ with $A\models p[v]$ for all formulas $p\in\Phi$. 

The principles underlying the definition of satisfaction are known from [[Interpretation (Formalized Language)|interpretations]], which extend assignements $v\in B(A,X)$ defined for variables $x\in X$ to [[Term (Formalized Language)|terms]] $t\in T(\Sigma,X)$.  Analogously, the concept of satisfaction extends assignements to formulas $p\in L(\Sigma,X)$.

==Properties of Satisfiability==

If $x\in X$ is used as a bounded variable in $p$ and if $p$ does not contain another variable $y\in X$, then for an assignement $v\in B(A,X)$ it holds {{Cite|TT95}} $$A\models p[v] \Longleftrightarrow A\models p[x\leftarrow y][v].$$ In other words, an appropriate renaming of bounded variables has no effect on the result of assignements resp. interpretations.

Another property of satisfiability is given by the Coincidence Theorem.  Its version known for terms can be adapted to the case of formulas.  Accordingly, for assignements $v_1,v_2\in B(A,X)$ the statement $\forall x\in V(p) \colon v_1(x)=v_2(x)$ implies the equivalence $v_1\models p \Longleftrightarrow v_2\models p$ {{Cite|M89}}.  

The substitution of a variable in a formula followed by an assignement can — at least in principle — be merged in a modified assignement {{Cite|TT95}}. In the following, let $A$ be a $\Sigma$-algebra, $x\in X$ a variable, $t\in T(\Sigma,X)$ a term, $p\in L(\Sigma,X)$ a formula, and $v\in B(A,X)$ an assignement. If $x$ is free in $p$ and if no bound variable $y$ of $p$ is free in $t$, then it holds $$A\models p[x\leftarrow t][v] \Longleftrightarrow A\models p[v[x\leftarrow t[v]]].$$ The statement is also true, if the variable $x$ does not occur in $p$ (i.e. if $x$ is neither a free nor a bound variable of $p$), because under this assumption the equalities $p[x\leftarrow t] = p$ and $p[v[x\leftarrow t[v]]] =p[v]$ are valid. 

==Definition of Validity==

The specific notion of satisfiability defined above — designated here as weak satisfiability — calls a formula $p\in L(\Sigma,X)$ satisfiable iff it exists an assignement $v$ for which $p[v]$ is true.  One can also formulate a stronger version {{Cite|ST99}}{{Cite|W90}} calling a formula $p \in L(\Sigma,X)$ satisfiable iff it is true for all interpretations. Clearly, satisfiability implies weak satisfiability but not vice versa. This leads to the following definition.

A $\Sigma$-algebra $A$ <i>satisfies</i> a formula $p\in L(\Sigma,X)$, written as $A \models p$ (or more precisely $A\models^\Sigma p$ in cases where $\Sigma$ is not obvious), if $\forall v\in B(A,X)\colon v\models p$. One also says, that $A$ is a <i>model</i> of $p$ and that $p$ is <i>valid</i> in $A$. This alternative wording is also used in the other cases below generalizing the notion of satisfiability to sets of formulas and classes of $\Sigma$-algebras. 
* A $\Sigma$-algebra $A$ <i>satisfies</i> a set $\Phi\subseteq L(\Sigma,X)$ of formulas, written $A \models \Phi$, if $A\models p$ for every formula $p \in \Phi$. Based on this definition, one can easily show that a $\Sigma$-algebra $A$ satisfies a formula $p\in L(\Sigma,X)$, iff it satisfies the universal closure of $p$ {{Cite|W90}}.
* A class $K$ of $\Sigma$-algebras <i>satisfies</i> a formula $p\in L(\Sigma,X)$, written $A\models p$, if $A \models p$ for every $\Sigma$-algebra $A \in K$. 
* A class $K$ of $\Sigma$-algebras <i>satisfies</i> a set $\Phi\subseteq L(\Sigma,X)$ of formulas, written $K \models \Phi$, if $A\models \Phi$ for every $\Sigma$-algebra $A\in K$.

==Properties of Validity==

For a formula $p\in L(\Sigma,X)$ with a free variable $x\in V(p)$ it holds {{Cite|M89}} $$A\models p(x) \Longleftrightarrow A\models \forall x\colon p(x)$$ according to the definition. An immediate consequence is $$A\models p(x) \Longrightarrow A\models p(t)$$ for terms $t\in T(\Sigma,X)$. In the case of partial functions and formulas, the assertions are somewhat more complicated, because the well-definedness of all expressions have to be assured. 

==Equations and Validity==

If one is working with $\Sigma$-algebras, the handling of equalities is indispensible e.g. for deciding which terms have to be identified in a quotient $\Sigma$-algebra. Thus, the satisfiability of equalities (and inequalities) are of special interest. As it turns out, $\Sigma$-algebra-morphism can sometimes transfer equalities and/or inequalities between $\Sigma$-algebras.

Let $m\colon A\longrightarrow B$ be a $\Sigma$-algebra-morphism and let $t_1,t_2\in T(\Sigma)$ be ground terms. Then it holds {{Cite|M89}} $$A\models t_1=t_2 \Longrightarrow B\models t_1=t_2$$ and $$B\models t_1\neq t_2 \Longrightarrow A\models t_1\neq t_2$$ If $m\colon A\longrightarrow B$ is surjective, the assertion $A\models t_1=t_2 \Longrightarrow B\models t_1=t_2$ can be generalized to terms $t_1,t_2\in T(\Sigma,X)$ not being ground {{Cite|EM85}}.  With help of these properties one can show for example that no (surjective) $\Sigma$-algebra-morphism exist between two given $\Sigma$-algebras {{Cite|EM85}}.

Similarly to the theorem given above, the Satisfaction Lemma states that translations of syntax (terms, equations) and semantics (algebras) induced by signature morphisms are compatible with the definition of satisfaction {{Cite|ST99}}: Let $\sigma \colon \Sigma \longrightarrow  \Sigma'$ be a signature morphism, $t_1,t_2\in T(\Sigma,X)$ be terms over $\Sigma$, and $A'$ be a $\Sigma'$-algebra. Then it holds $$A' \models^{\Sigma'} \sigma(t_1) = \sigma(t_2) \,\,\,\,\,\Longleftrightarrow \,\,\,\,\, A'|_\sigma \models^\Sigma t_1=t_2.$$

==References==

{|
|-
|valign="top"|{{Ref|EM85}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
|-
|valign="top"|{{Ref|EM90}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
|-
|valign="top"|{{Ref|M89}}||valign="top"| B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I", lecture notes, Technical University Munich 1989
|-
|valign="top"|{{Ref|ST99}}||valign="top"| D. Sannella, A. Tarlecki, "Algebraic Preliminaries", in Egidio Astesiano, Hans-Joerg Kreowski, Bernd Krieg-Brueckner, "Algebraic Foundations of System Specification", Springer 1999
|-
|valign="top"|{{Ref|W90}}||valign="top"| M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990
|-
|}