\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[TS1,T2A]{fontenc}
\usepackage[russian]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}

\hoffset=-3cm
\textwidth=18cm
\voffset=-3cm
\textheight=26cm

\date{2010-03-16}
\title{Лекции по матлогу}
\author{Зайцев Вадим}

\begin{document}
\maketitle

\subsubsection{Случай с равенством}
$(t_1 = q_1) ... (t_n = q_n) \vdash f(t_1...t_n) = f(q_1...q_n)$\\
$(t_1 = q_1) ... (t_n = q_n) \quad [f(t_1...t_n) = f(x_1...x_n)]_{t_1...t_n}^{x_1...x_n} \vdash [f(t_1...t_n) = f(x_1...x_n)]_{q_1...q_n}^{x_1...x_n}$ - по аксиоме\\
$(t_1 = q_1) ... (t_n = q_n)  \quad (f(t_1...t_n) = f(t_1..t_n)) \vdash ( f(t_1...t_n) = f(q_1...q_n)) \quad \vdash f(t_1...t_n) = f(t_1...t_n)$\\ - по правилу сечения тут что-то уходит

\subsubsection{Лемма}
$t \in T(\sigma') \quad FV(t) = \varnothing$\\
$\exists c \in C : (t=c) \in T'$
\begin{proof}
	$\vdash (t=t) \Rightarrow \vdash [t=x]_t^x$\\
	$ \displaystyle \frac{\vdash [t=x]_t^x}{\vdash \exists x (t=x)}$\\
	$T' \vdash \exists x(t=x)$\\
	$\exists x (t=x) \in T' \Rightarrow \exists q \in C \quad (t=c) \in T'$
\end{proof}

\subsubsection{Опр.}
	$c, e \in C \quad c \sim e \Leftrightarrow (c=e) \in T'$
	
\subsubsection{Пред.}
	$\sim$ - отношение эквивалентности:
	\begin{enumerate}
		\item $ \forall c \in C  \quad \vdash (c=c) \Rightarrow T' \vdash (c=c) \Rightarrow (c=c) \in T'$
		\item $ \forall c, e, \in C \quad (c\sim e) \Rightarrow (c=e) \in T'$ и $ (c\sim e) \vdash (e=c) \Rightarrow T' \vdash (e=c) \Rightarrow (e=c) \in T'$
		\item $\forall c, e, v \in C$\\
			$ (c\sim e), (e\sim f) \Rightarrow (c=e) \in T', (e=f) \in T' \quad (c=e)(e=f) \vdash (c=f) \Rightarrow T' \vdash (c=f) \Rightarrow (c=f) \in T' \Rightarrow c \sim f$
	\end{enumerate}
	
\subsubsection{asdf}
	\begin{enumerate}
		\item $ \forall P \in \sigma' \quad \forall c_1...c_n \in C$\\
			$ \mathfrak{A} ]vDash P([c_1]...[c_n]) \Leftrightarrow P(c_1...c_n) \in T'$
		\item $\forall f \in \sigma' \quad \forall c_1...c_n \in C$\\
			$ f^{\mathfrak{A}'} ([c_1]...[c_n]) = [d]$, if $(f(c_1...c_n)=d) \in T' $
		\item $ \forall e \in \sigma' \quad e^{\mathfrak{A}'} = [c]$, if $(e=c) \in T'$
	\end{enumerate}
	
\subsubsection{Лемма}
	$ t \in T(\sigma') \quad FV(t) = \varnothing$\\
	$ \exists c \in C \quad t^{\mathfrak{A}'} = [c] \Leftrightarrow (t-c) \in T'$
\begin{proof}
	по построению терма:\\
	\begin{enumerate}
		\item $t=e - const$ - всё получается, всё хорошо и т.п.
		\item $t=f(q_1...q_n) \quad q_1...q_n \in T(\sigma'), \, FV(q_i) = \varnothing$\\
			$\exists c_1...c_n \\ q_i^{\mathfrak{A}'} = [c_i] \Leftrightarrow (q_i =c_i) \in T'$\\
			$(q_1 = c_1)...(q_n=c_n) \vdash f(q_1...q_n) = f(c_1...c_n)$\\
			$\Rightarrow T' \vdash (f(q_1...q_n) = f(c_1...c_n)) \Rightarrow T' \vdash (t=f(c_1...c_n)) \Rightarrow (t=f(c_1...c_n)) \in T'$.\\
			$\Rightarrow ) \quad t^{\mathfrak{A}'} = [c]$\\
				$t^{\mathfrak{A}'} = f^{\mathfrak{A}'}(q_1^{\mathfrak{A}'}...q_n^{\mathfrak{A}'}) = f^{\mathfrak{A}'}([c_1]...[c_n]) = [c]$\\
				$\Rightarrow (f(c_1 \ldots c_n) = c) \in T'$\\
				$(t=f(c_1...c_n))(f(c_1...c_n)=c) \vdash (t=c)$\\
				$T' \vdash (t=c) \Rightarrow (t=c) \in T'$\\
			$\Leftarrow ) (t=c) \in T'$\\
				$\quad (t=c)(t=f(c_1...c_n) \vdash (f(c_1...c_n)=c)$\\
				$T' \vdash (f(c_1...c_n)=c)\\(f(c_1..c_n)=c) \in T' \Rightarrow f^{\mathfrak{A}'}([c_1]...[c_n]) = [c] \Rightarrow f^{\mathfrak{A}'} = [c]$
	\end{enumerate}
\end{proof}

\subsubsection{Следующая лемма}
	$t,q$ - замкнутые термы\\
	$\mathfrak{A}' \vDash (t=q) \Leftrightarrow (t=q) \in T'$
\begin{proof}
	$\exists c,d \in C \quad (t=c) \in T' \quad (q=d) \in T'$\\
	$\Rightarrow t^{\mathfrak{A}'} = [c] \quad q^{\mathfrak{A}'}=[d]$\\
	$\mathfrak{A}' \vDash (t=q) \Leftrightarrow t^{\mathfrak{A}'} = q^{\mathfrak{A}'} \Leftrightarrow  [c]=[d] \Leftrightarrow c\sim d \Leftrightarrow (c=d) \in T'$\\
	$\Rightarrow) \quad \mathfrak{A}' \vDash (t=q) \Rightarrow (c=d) \in T' \Rightarrow (c=d)(t=c)(q=d) \vdash (t=q) \Rightarrow T' \vdash (t=q) \Rightarrow (t=q) \in T'$\\
	$\Leftarrow) (t=q) \in T'$\\
		$(t=q)(t=c)(q=d) \vdash (c=d) \Rightarrow T' \vdash (c=d) \Rightarrow (c=d) \in T'$\\
	$\Rightarrow \mathfrak{A}' \vDash (t=q)$
\end{proof}

\subsubsection{Очередная лемма}
	$ P \in \sigma'$\\
	$t_1 \ldots t_n$ - зам. терм.\\
	$\mathfrak{A}' \vDash$\\
	
	$\exists c_1 \ldots c_n \in C$\\
	$(t_i = c_i) \in T'$\\
	$t_i^{\mathfrak{A}'} = [c_i]$\\
	$\mathfrak{A}' \vDash P(t_1^{\mathfrak{A}'}...t_n^{\mathfrak{A}'}) \Leftrightarrow \mathfrak{A}' \vDash([c_1]...[c_n]) \Leftrightarrow P(c_1...c_n) \in T'$\\
	$\Rightarrow) (t_1=c_1)...(t_n=c_n)  \quad P(c_1...c_n) \vdash P(t_1...t_n) \Rightarrow T' \vdash P(t_1...t_n) \Rightarrow P(t_1...t_n) \in T'$\\
	$\Leftarrow) P(t_1...t_n) \in T'$\\
		$ (t_1=c_1)...(t_n = c_n)P(t_1...t_n) \vdash P(c_1...c_n) \Rightarrow T' \vdash P(c_1...c_n) \Rightarrow P(c_1...c_n) =\in T' \Rightarrow\\
		\Rightarrow \mathfrak{A}' \vDash P([c_1]...[c_n]) \Rightarrow \mathfrak{A}' \vDash P(t_1^{\mathfrak{A}'}...t_n^{\mathfrak{A}'})$

\subsubsection{Последняя лемма}
	$ \varphi = \varphi(t_1...t_n) \in S(\sigma')\\
	t_1..t_n$ - замкнутый терм\\
	$\mathfrak{A}' \vDash \varphi(t_1^{\mathfrak{A}'}...t_n^{\mathfrak{A}'}) \Leftrightarrow \varphi(t_1...t_n) \in T'$
	\begin{proof}
		$\varphi=(t=q) \quad \varphi  = P(t_1...t_n)$ (3,4 леммы)\\
		$\varphi = \xi_1 \& \xi_2\\
		\mathfrak{A}' \vDash (\varphi_1 \& \varphi_2) \Leftrightarrow \mathfrak{A}' \vDash \varphi_1$ и $\mathfrak{A}' \vDash \varphi_2 \Leftrightarrow\\
		\Leftrightarrow \varphi_1 \in T'$ и $\varphi_2 \in T' \Leftrightarrow \varphi_1 \& \varphi_2 \in T'$\\
		$ \varphi = \varphi \vee \varphi$\\
		$ \varphi \neg \varphi_1 \quad \mathfrak{A}' \vDash \neg \varphi_1 \Leftrightarrow \mathfrak{A}' \not\vDash \varphi_1 \Leftrightarrow \varphi \not\in T' \Leftrightarrow $\\
		$ \varphi = \varphi_1 \rightarrow \varphi_2$\\
		$ \varphi = \exists x \psi(x) \quad \mathfrak{A}' \vDash \varphi \Leftrightarrow \exists c \in C \quad \mathfrak{A}' \vDash \psi([c])$
	\end{proof}

\subsubsection{Следствие}
	$ \mathfrak{A}' \vDash T' $\\
	$ \Gamma' = T_0 \subseteq T' \Rightarrow  \mathfrak{A}' \vDash \Gamma'$\\
	$ \Gamma' = [\Gamma]_D^X $\\
	$ \displaystyle  \mathfrak{A} = \mathfrak{A}' |_\sigma  \quad \gamma : X \rightarrow |\mathfrak{A}|  \quad  \gamma(x_i) = d_i^{\mathfrak{A}'} (=[c_i])$\\
	$ \mathfrak{A}' \vDash \Gamma[\gamma] $
что-то доказано.

\subsubsection{Опр}
	$\Gamma \subseteq F(\sigma)\\ \Gamma$ - совместна, если $\exists \mathfrak{A} \exists \gamma :  \quad \mathfrak{A}\vDash \Gamma[\gamma]$\\
	$\Gamma$ - локально совместна, если $ \vdash \Gamma_0 \subseteq \Gamma; \quad \Gamma_0$ - коечно, $\Gamma_0$ - совместна.
	
\subsubsection{Теорема мальцева о компактности}
	$ \Gamma$ - совместна $ \Leftrightarrow \Gamma$ - локально совместна.
	\begin{proof}
		\begin{description}
			\item[$ \Rightarrow $] очевидно.
			\item[$\Leftarrow$] $\Gamma$ - локально совместна. $\Gamma$ - несовместна. $ \Rightarrow  \Gamma \vdash$\\
				$\exists \varphi_1...\varphi_n \in \Gamma$, $\varphi_1...\varphi_n \vdash$ - доказуемо.\\
				$ \Gamma_0 = \{ \varphi_1... \varphi_n \} \subseteq \Gamma$\\
				$ \Rightarrow \exists \mathfrak{A}' \exists \gamma : \quad \mathfrak{A} \vDash \Gamma_0 [\gamma] \Rightarrow \mathfrak{A} \vDash \varphi_1[\gamma] ... \mathfrak{A} \vDash \varphi_n[\gamma]  \Rightarrow \varphi_1...\varphi_n \vdash$ - не т.и.
		\end{description}

	\end{proof}


\end{document}
