| Version 14 |
Version 13 |
| \PMlinkescapeword{relations} |
\PMlinkescapeword{relations} |
|
|
| Let $L$ be a formal language with function symbols $F$, relation |
Let $L$ be a logical language with function symbols $F$, relations $R$, and types $T$. Then $$\mathcal{M}=\langle \{\mathcal{M}_t\mid t\in T\},\{f^\mathcal{M}\mid f\in F\},\{r^\mathcal{M}\mid r\in R\}\rangle$$ is a \emph{model} of $L$ (also called an $L$-structure, or, if the underlying logic is clear, a $\Sigma$-structure, where $\Sigma$ is a signature specifying just $F$ and $R$) if: |
| symbols $R$, and sorts $S$ (if $L$ includes more than one sort of |
|
| quantifiable variable, then $L$ is a \emph{many-sorted} language, |
|
| otherwise $S$ may be omitted). Then $$\mathcal{M}=\langle |
|
| \{\mathcal{M}_s\mid s\in S\},\{f^\mathcal{M}\mid f\in |
|
| 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 |
|
| $\Sigma$-structure, where $\Sigma$ is a signature specifying just |
|
| $F$ and $R$) if: |
|
|
|
| \begin{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$
|
\item Whenever $f$ is an $n$-ary function symbol such that $\operatorname{Type}(f)=t$ and $\operatorname{Inputs}_n(f)=\langle t_1,\ldots,t_n\rangle$ then $f^\mathcal{M}:\prod_1^n \mathcal{M}_{t_i}\rightarrow\mathcal{M}_t$
|
|
\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}$
|
\item Whenever $r$ is an $n$-ary relation symbol such that $\operatorname{Inputs}_n(r)=\langle t_1,\ldots,t_n\rangle$ then $r^\mathcal{M}$ is a relation on $\prod_1^n \mathcal{M}_{t_i}$
|
| \end{itemize} |
\end{itemize} |
|
|
| If $t$ is a term of $L$ of sort $s_t$ without free variables then |
If $s$ is a term of $L$ of type $t_s$ without free variables then it follows that $s=fs_1\ldots s_n$ and $s^\mathcal{M}=f^\mathcal{M}(s_1^\mathcal{M},\ldots,s_n^\mathcal{M})\in M_{t_s}$. |
| it follows that $t=ft_1\ldots t_n$ and |
|
| $t^\mathcal{M}=f^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})\in |
If $\phi$ is a sentence then we write $\mathcal{M}\vDash\phi $ (and say that $\mathcal{M}$ satisfies $\phi$) if $\phi$ is true in $\mathcal{M}$, where truth of a relation is defined by: |
| M_{s_t}$. |
|
|
|
| If $\phi$ is a sentence then we write $\mathcal{M}\vDash\phi $ |
|
| (and say that $\mathcal{M}$ satisfies $\phi$ or that $\mathcal{M}$ |
|
| is a \emph{model} of $\phi$ ) if $\phi$ is true in $\mathcal{M}$, |
|
| where truth is defined as follows: |
|
|
|
| \begin{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})$
|
\item $Rt_1\ldots t_n$ is true if if $R^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})$
|
| \item truth of a non-atomic formula is defined using the semantics of the underlying logic. |
\item truth of a non-atomic formula is defined using the semantics of the underlying logic. |
| \end{itemize} |
\end{itemize} |
|
|
| If $\Phi$ is a class of sentences, we write |
If $\Phi$ is a class of sentences, we write $\mathcal{M}\vDash\Phi$ if for every $\phi\in\Phi$, $\mathcal{M}\vDash\phi$. |
| $\mathcal{M}\vDash\Phi$ if for every $\phi\in\Phi$, |
|
| $\mathcal{M}\vDash\phi$. |
For any term $s$ of $L$ whose only free variables are included in $x_1,\ldots,x_n$ with types $t_1,\ldots,t_n$ then for any $a_1,\ldots,a_n$ such that $a_i\in M_{t_i}$ define $s^\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 |
|
| $a_1,\ldots,a_n$ such that $a_i\in M_{s_i}$ define |
|
| $t^\mathcal{M}(a_1,\ldots,a_n)$ by: |
|
|
|
| \begin{itemize} |
\begin{itemize} |
|
\item If $t_i=x_i$ then $t_i^\mathcal{M}(a_1,\ldots,a_n)=a_i$
|
\item If $s_i=x_i$ then $s_i^\mathcal{M}(a_1,\ldots,a_n)=a_i$
|
|
\item If $t=ft_1\ldots t_m$ then $t^\mathcal{M}(a_1,\ldots,a_n)=
|
\item If $s=fs_1\ldots s_m$ then $s^\mathcal{M}(a_1,\ldots,a_n)=
|
|
f ^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n),
|
f ^\mathcal{M}(s_1^\mathcal{M}(a_1,\ldots,a_n),
|
|
\ldots,t_n^\mathcal{M}(a_ 1,\ldots,a_n))$
|
\ldots,s_n^\mathcal{M}(a_ 1,\ldots,a_n))$
|
| \end{itemize} |
\end{itemize} |
|
|
| If $\phi$ is a formula whose only free variables are included in |
If $\phi$ is a formula whose only free variables are included in $x_1,\ldots,x_n$ with types $t_1,\ldots,t_n$ then for any $a_1,\ldots,a_n$ such that $a_i\in \mathcal{M}_{t _i}$ define $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$ recursively by: |
| $x_1,\ldots,x_n$ of sorts $s_1,\ldots,s_n$ then for any |
|
| $a_1,\ldots,a_n$ such that $a_i\in \mathcal{M}_{t _i}$ define |
|
| $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$ recursively by: |
|
|
|
| \begin{itemize} |
\begin{itemize} |
|
\item If $\phi=Rt_1 \ldots t_m$ then $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$ if and only if $R^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n),\ldots,
|
\item If $\phi=Rs_1 \ldots s_m$ then $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$ iff $R^\mathcal{M}(s_1^\mathcal{M}(a_1,\ldots,a_n),\ldots,
|
|
t_n^\mathcal{M}(a_1,\ldots,a_n))$
|
s_n^\mathcal{M}(a_1,\ldots,a_n))$
|
| \item Otherwise the truth of $\phi$ is determined by the semantics of the underlying logic. |
\item Otherwise the truth of $\phi$ is determined by the semantics of the underlying logic. |
| \end{itemize} |
\end{itemize} |
|
|
| As above, $\mathcal{M}\vDash\Phi(a_1,\ldots,a_n)$ if and only if |
As above, $\mathcal{M}\vDash\Phi(a_1,\ldots,a_n)$ iff for every $\phi\in\Phi$, $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$. |
| for every $\phi\in\Phi$, $\mathcal{M}\vDash\phi(a_1,\ldots,a_n)$. |
|
