... ... @@ -99,13 +99,24 @@ reassignment. A ground $\Sigma$-formula is said to be satisfiable in the $\Sigma$-theory $\mathcal{T}$, or $\mathcal{T}$-satisfiable, if there exists a $\Sigma$-structure $\mathcal{A} \in \mathcal{T}$ such that $\mathcal{A}$ satisfies $\varphi$. The structure $\mathcal{A}$ is then called a \emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ and $\psi$ are ground $\Sigma$-formulas such that $\varphi \wedge \neg \psi$ is $\mathcal{T}$-unsatisfiable, we say that \emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as $\varphi \models_T \psi$. A $\Sigma$-formula $\varphi$ such that $\neg \varphi$ is $\mathcal{T}$-unsatisfiable is called a \emph{theory lemma}. then called a \emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$ is a ground $\Sigma$-formula and $\Gamma$ is a set of ground $\Sigma$-formulas, we say that \emph{$\Gamma$ entails $\varphi$ in $\mathcal{T}$}, written $\Gamma \models_\mathcal{T} \varphi$, if every $\Sigma$-structure that satisfies all formulas in $\Gamma$ also satisfies $\varphi$. If $\emptyset \models_\mathcal{T} \varphi$ for a ground $\Sigma$-formula $\varphi$, the formula $\varphi$ is called \emph{$\mathcal{T}$-valid} or a \emph{theory lemma}. A set $\Gamma$ of ground $\Sigma$-formulas is called \emph{$\mathcal{T}$-inconsistent}, if $\Gamma \models_{\mathcal{T}} \bot$. % If $\varphi$ % and $\psi$ are ground $\Sigma$-formulas such that % $\varphi \wedge \neg \psi$ is $\mathcal{T}$-unsatisfiable, we say that % \emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as % . A $\Sigma$-formula $\varphi$ such that % $\neg \varphi$ is $\mathcal{T}$-unsatisfiable is called a \emph{theory % lemma}. For two signatures $\Sigma$ and $\Omega$, we call $\Omega$ a \emph{sub-signature} of $\Sigma$ if $\Omega \subseteq \Sigma$, ... ...