| Version 23 |
Version 22 |
| Let $\tau$ be a signature and $\varphi$ be a $\tau$-sentence. A \emph{model} of $\varphi$ is a $\tau$-structure $\mathcal{M}$ such that $$\mathcal{M}\models \varphi$$ |
\PMlinkescapeword{relations} |
| where $\models$ is the satisfaction relation. When $\mathcal{M}\models \varphi$, we says that $\varphi$ satisfies $\mathcal{M}$. |
|
|
|
| More generally, we say that a $\tau$-structure $\mathcal{M}$ is a \emph{model} of a theory $T$ over $\tau$, if every sentence in $T$ satisfies $\mathcal{M}$. When $\mathcal{M}$ is a model of $T$, we say that $T$ satisfies $\mathcal{M}$. |
Let $L$ be a formal language with function symbols $F$, relation |
|
symbols $R$, and sorts $S$ (if $L$ includes more than one sort of |
| %\PMlinkescapeword{relations} |
quantifiable variable, then $L$ is a \emph{many-sorted} language, |
|
otherwise $S$ may be omitted). Then $$\mathcal{M}=\langle |
| %Let $L$ be a formal language with function symbols $F$, relation |
\{\mathcal{M}_s\mid s\in S\},\{f^\mathcal{M}\mid f\in |
| %symbols $R$, and sorts $S$ (if $L$ includes more than one sort of |
F\},\{r^\mathcal{M}\mid r\in R\}\rangle$$ \emph{interprets} $L$ |
| %quantifiable variable, then $L$ is a \emph{many-sorted} language, |
(or is an $L$-structure, or, if the underlying logic is clear, a |
| %otherwise $S$ may be omitted). Then $$\mathcal{M}=\langle |
$\Sigma$-structure, where $\Sigma$ is a signature specifying just |
| %\{\mathcal{M}_s\mid s\in S\},\{f^\mathcal{M}\mid f\in |
$F$ and $R$) if: |
| %F\},\{r^\mathcal{M}\mid r\in R\}\rangle$$ \emph{interprets} $L$ |
|
| %(or is an $L$-structure, or, if the underlying logic is clear, a |
\begin{itemize} |
| %$\Sigma$-structure, where $\Sigma$ is a signature specifying just |
\item Whenever $f$ is an $n$-ary function symbol such that $\operatorname{Sort}(f)=s$ and $\operatorname{Inputs}_n(f)=\langle s_1,\ldots,s_n\rangle$ then $f^\mathcal{M}:\prod_1^n \mathcal{M}_{s_i}\rightarrow\mathcal{M}_s$ |
| %$F$ and $R$) if: |
\item Whenever $r$ is an $n$-ary relation symbol such that $\operatorname{Inputs}_n(r)=\langle s_1,\ldots,s_n\rangle$ then $r^\mathcal{M}$ is a relation on $\prod_1^n \mathcal{M}_{s_i}$ |
|
\end{itemize} |
| %\begin{itemize} |
|
| %\item Whenever $f$ is an $n$-ary function symbol such that $\operatorname{Sort}(f)=s$ and %$\operatorname{Inputs}_n(f)=\langle s_1,\ldots,s_n\rangle$ then $f^\mathcal{M}:\prod_1^n %\mathcal{M}_{s_i}\rightarrow\mathcal{M}_s$ |
If $t$ is a term of $L$ of sort $s_t$ without free variables then |
| %\item Whenever $r$ is an $n$-ary relation symbol such that $\operatorname{Inputs}_n(r)=\langle s_1,\ldots,s_n\rangle$ %then $r^\mathcal{M}$ is a relation on $\prod_1^n \mathcal{M}_{s_i}$ |
it follows that $t=ft_1\ldots t_n$ and |
| %\end{itemize} |
$t^\mathcal{M}=f^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})\in |
|
M_{s_t}$. |
| %If $t$ is a term of $L$ of sort $s_t$ without free variables then |
|
| %it follows that $t=ft_1\ldots t_n$ and |
If $\phi$ is a sentence then we write $\mathcal{M}\models\phi $ |
| %$t^\mathcal{M}=f^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})\in |
(and say that $\mathcal{M}$ satisfies $\phi$ or that $\mathcal{M}$ |
| %M_{s_t}$. |
is a \emph{model} of $\phi$ ) if $\phi$ is true in $\mathcal{M}$, |
|
where truth is defined as follows: |
| %If $\phi$ is a sentence then we write $\mathcal{M}\models\phi $ |
|
| %(and say that $\mathcal{M}$ satisfies $\phi$ or that $\mathcal{M}$ |
\begin{itemize} |
| %is a \emph{model} of $\phi$ ) if $\phi$ is true in $\mathcal{M}$, |
\item $Rt_1\ldots t_n$ is true if and only if $R^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})$ |
| %where truth is defined as follows: |
\item truth of a non-atomic formula is defined using the semantics of the underlying logic. |
|
\end{itemize} |
| %\begin{itemize} |
|
| %\item $Rt_1\ldots t_n$ is true if and only if $R^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})$ |
If $\Phi$ is a class of sentences, we write |
| %\item truth of a non-atomic formula is defined using the semantics of the underlying logic. |
$\mathcal{M}\models\Phi$ if for every $\phi\in\Phi$, |
| %\end{itemize} |
$\mathcal{M}\models\phi$. |
|
|
| %If $\Phi$ is a class of sentences, we write |
For any term $t$ of $L$ whose only free variables are included in |
| %$\mathcal{M}\models\Phi$ if for every $\phi\in\Phi$, |
$x_1,\ldots,x_n$ of sorts $s_1,\ldots,s_n$ then for any |
| %$\mathcal{M}\models\phi$. |
$a_1,\ldots,a_n$ such that $a_i\in M_{s_i}$ define |
|
$t^\mathcal{M}(a_1,\ldots,a_n)$ by: |
| %For any term $t$ of $L$ whose only free variables are included in |
|
| %$x_1,\ldots,x_n$ of sorts $s_1,\ldots,s_n$ then for any |
\begin{itemize} |
| %$a_1,\ldots,a_n$ such that $a_i\in M_{s_i}$ define |
\item If $t_i=x_i$ then $t_i^\mathcal{M}(a_1,\ldots,a_n)=a_i$ |
| %$t^\mathcal{M}(a_1,\ldots,a_n)$ by: |
\item If $t=ft_1\ldots t_m$ then $t^\mathcal{M}(a_1,\ldots,a_n)= |
|
f ^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n), |
| %\begin{itemize} |
\ldots,t_n^\mathcal{M}(a_ 1,\ldots,a_n))$ |
| %\item If $t_i=x_i$ then $t_i^\mathcal{M}(a_1,\ldots,a_n)=a_i$ |
\end{itemize} |
| %\item If $t=ft_1\ldots t_m$ then $t^\mathcal{M}(a_1,\ldots,a_n)= |
|
| %f ^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n), |
If $\phi$ is a formula whose only free variables are included in |
| %\ldots,t_n^\mathcal{M}(a_ 1,\ldots,a_n))$ |
$x_1,\ldots,x_n$ of sorts $s_1,\ldots,s_n$ then for any |
| %\end{itemize} |
$a_1,\ldots,a_n$ such that $a_i\in \mathcal{M}_{s_i}$ define |
|
$\mathcal{M}\models\phi(a_1,\ldots,a_n)$ recursively by: |
| %If $\phi$ is a formula whose only free variables are included in |
|
| %$x_1,\ldots,x_n$ of sorts $s_1,\ldots,s_n$ then for any |
\begin{itemize} |
| %$a_1,\ldots,a_n$ such that $a_i\in \mathcal{M}_{s_i}$ define |
\item If $\phi=Rt_1 \ldots t_m$ then $\mathcal{M}\models\phi(a_1,\ldots,a_n)$ if and only if $R^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n),\ldots, |
| %$\mathcal{M}\models\phi(a_1,\ldots,a_n)$ recursively by: |
t_n^\mathcal{M}(a_1,\ldots,a_n))$ |
|
\item Otherwise the truth of $\phi$ is determined by the semantics of the underlying logic. |
| %\begin{itemize} |
\end{itemize} |
| %\item If $\phi=Rt_1 \ldots t_m$ then $\mathcal{M}\models\phi(a_1,\ldots,a_n)$ if and only if %$R^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n),\ldots, |
|
| %t_n^\mathcal{M}(a_1,\ldots,a_n))$ |
As above, $\mathcal{M}\models\Phi(a_1,\ldots,a_n)$ if and only if |
| %\item Otherwise the truth of $\phi$ is determined by the semantics of the underlying logic. |
for every $\phi\in\Phi$, $\mathcal{M}\models\phi(a_1,\ldots,a_n)$. |
| %\end{itemize} |
|
|
\begin{thebibliography}{9} |
| %As above, $\mathcal{M}\models\Phi(a_1,\ldots,a_n)$ if and only if |
\bibitem{Manzano} Manzano, Maria, {\em Extensions of First Order Logic}, Cambridge University Press, New York, 1996. |
| %for every $\phi\in\Phi$, $\mathcal{M}\models\phi(a_1,\ldots,a_n)$. |
\end{thebibliography} |
|
|
| %\begin{thebibliography}{9} |
|
| %\bibitem{Manzano} Manzano, Maria, {\em Extensions of First Order Logic}, Cambridge University Press, New York, 1996. |
|
| %\end{thebibliography} |
|
