|
|
|
Viewing Version
25
of
'model'
|
[ view 'model'
|
back to history
]
| Title of object: |
model |
| Canonical Name: |
Model |
| Type: |
Definition |
| Created on: |
2002-08-28 22:47:24 |
| Modified on: |
2007-11-18 15:43:22 |
| Classification: |
msc:03C95 |
| Keywords: |
$L$-structure |
| Defines: |
model |
| Synonyms: |
model=structure
model=$L$-structure |
Preamble:
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{amsfonts}
%\usepackage{psfrag}
%\usepackage{graphicx}
%\usepackage{amsthm}
%\usepackage{xypic} |
Content:
Let $\tau$ be a signature and $\varphi$ be a sentence over $\tau$. A \PMlinkname{structure}{Structure} $\mathcal{M}$ for $\tau$ is called a \emph{model} of $\varphi$ if $$\mathcal{M}\models \varphi,$$
where $\models$ is the satisfaction relation. When $\mathcal{M}\models \varphi$, we says that $\varphi$ \emph{satisfies} $\mathcal{M}$, or that $\mathcal{M}$ is \emph{satisfied by} $\varphi$.
More generally, we say that a $\tau$-structure $\mathcal{M}$ is a \emph{model} of a theory $T$ over $\tau$, if $\mathcal{M}\models \varphi$ for every $\varphi\in T$. When $\mathcal{M}$ is a model of $T$, we say that $T$ \emph{satisfies} $\mathcal{M}$, or that $\mathcal{M}$ is satisfied by $T$, and is written $$\mathcal{M}\models T.$$
%\PMlinkescapeword{relations}
%Let $L$ be a formal language with function symbols $F$, relation
%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}
%\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 $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}
%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
%$t^\mathcal{M}=f^\mathcal{M}(t_1^\mathcal{M},\ldots,t_n^\mathcal{M})\in
%M_{s_t}$.
%If $\phi$ is a sentence then we write $\mathcal{M}\models\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}
%\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 truth of a non-atomic formula is defined using the semantics of the underlying logic.
%\end{itemize}
%If $\Phi$ is a class of sentences, we write
%$\mathcal{M}\models\Phi$ if for every $\phi\in\Phi$,
%$\mathcal{M}\models\phi$.
%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}
%\item If $t_i=x_i$ then $t_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)=
%f ^\mathcal{M}(t_1^\mathcal{M}(a_1,\ldots,a_n),
%\ldots,t_n^\mathcal{M}(a_ 1,\ldots,a_n))$
%\end{itemize}
%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
%$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:
%\begin{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))$
%\item Otherwise the truth of $\phi$ is determined by the semantics of the underlying logic.
%\end{itemize}
%As above, $\mathcal{M}\models\Phi(a_1,\ldots,a_n)$ if and only if
%for every $\phi\in\Phi$, $\mathcal{M}\models\phi(a_1,\ldots,a_n)$.
%\begin{thebibliography}{9}
%\bibitem{Manzano} Manzano, Maria, {\em Extensions of First Order Logic}, Cambridge University Press, New York, 1996.
%\end{thebibliography} |
|
|
|
|
|
