\documentclass{article}

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

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

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

\begin{document}
\maketitle

\section{Секвенциальное исчисление предикатов}
\subsection{Алфавит:}
\begin{enumerate}
	\item $x_{1}, x_{2} \ldots$ - пропозициональные переменные
	\item $c_{1}, c_{2} \ldots$ - константы
	\item $P_{1}, P_{2} \ldots$ - предикаты
	\item $f_{1}, f_{2} \ldots$ - функции
	\item $\vee, \&, \rightarrow, \neg, \forall, \exists$
	\item $\vdash$
	\item '(', ')', ','
	\item =
\end{enumerate}

\subsection{Аксиомы:}
\begin{enumerate}
	\item $ \varphi \vdash \varphi $
	\item $ \vdash \forall x \quad (x=x) $
	\item $ \vdash \forall x \forall y \quad ((x=y) \rightarrow (y=x)) $
	\item $ \vdash \forall x \forall y \forall z \quad (((x=y) \& (y=z)) \rightarrow (x=z)) $
	\item $ (t_{1} = q_{1}), (t_{2} = q_{2}), \ldots, (t_{n}=q_{n}), \varphi(t_{1}, \ldots, t_{n})
		\vdash \varphi(q_{1}, \ldots, q_{n})$
\end{enumerate}


\subsection{Правила вывода:}
	\begin{tabular}{p{5cm} p{5cm} p{5cm}}
		$ \displaystyle 1) \quad \frac{\Gamma \vdash \varphi; \Gamma \vdash \psi}{\Gamma \vdash (\varphi \& \psi)} $ &
		$ \displaystyle 2) \quad \frac{\Gamma \vdash (\varphi \& \psi)}{\Gamma \vdash \psi} $ &
		$ \displaystyle 3) \quad \frac{\Gamma \vdash (\varphi \& \psi)}{\Gamma \vdash \varphi} $ \\ \\
		
		$ \displaystyle 4) \quad \frac{\Gamma \vdash \psi}{\Gamma \vdash ( \psi \vee \varphi )} $ &
		$ \displaystyle 5) \quad \frac{\Gamma \vdash \varphi}{\Gamma \vdash ( \psi \vee \varphi)} $ &
		$ \displaystyle 6) \quad \frac{\Gamma, \varphi \vdash \xi; \Gamma, \psi \vdash \xi; \Gamma \vdash (\varphi \vee \psi)}{\Gamma \vdash \xi} $ \\ \\

		$ \displaystyle 7) \quad \frac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash (\varphi \rightarrow \psi)} $ &
		$ \displaystyle 8) \quad \frac{\Gamma, \neg \psi \vdash}{\Gamma \vdash \psi} $ &
		$ \displaystyle 9) \quad \frac{\Gamma \vdash \varphi; \Gamma \vdash \neg \varphi}{\Gamma \vdash} $ \\ \\
		
		$ \displaystyle 10) \quad \frac{\Gamma \vdash \varphi; \Gamma \vdash (\varphi \rightarrow \psi)}{\Gamma \vdash \psi} $ &
		$ \displaystyle 11) \quad \frac{\Gamma_{1}, \varphi, \psi, \Gamma_{2} \vdash \xi}{\Gamma_{1}, \psi, \varphi, \Gamma_{2} \vdash \xi} $ &
		$ \displaystyle 12) \quad \frac{\Gamma \vdash \psi}{\Gamma, \varphi \vdash \psi} $ \\ \\
		
		$ \displaystyle 13) \quad \frac{\Gamma \vdash \varphi(t)}{\Gamma \vdash \forall x \, \varphi(x)}, x \notin FV\left(\Gamma)\right. $ &
		$ \displaystyle 14) \quad \frac{\Gamma \vdash \forall x \varphi(x)}{\Gamma \vdash \varphi(t)} $ &
		$ \displaystyle 15) \quad \frac{\Gamma \vdash \varphi(t)}{\Gamma \vdash \exists x \, \varphi(x)} $ \\ \\
		
		\multicolumn{3}{l}{$ \displaystyle 16) \quad \frac{\Gamma, \varphi(t) \vdash \psi}{\Gamma, \exists x \, \varphi(x) \vdash \psi}, x \notin Fv\left(\Gamma, \psi)\right.$}
	\end{tabular}
	
\subsection{Определения (из ИВ):}
	Док-во, дерево секвенций, дерево выводов, допустимое правило вывода, доказуемая секвенция.

\subsection{Предоложение:}
	Секвенция доказуема $\Leftrightarrow$ когда существует дерево вывода, оканчивающееся на
	эту секвенцию.

\subsection{Предложение:}
	Если секвенция логики предикатов получена подстановкой в доказуемую секвенцию логики высказываний
	вместо пропизициоальных переменных формул логики предикатов, то эта секвенция доказуема и в
	исчислении предикатов.
	
\subsection{Предложение:}
	Правила вывода, допустимые в ИВ являются допустимыми в ИП. \\ \textit{Доказывается просто :)}
	
\subsection{Следующие правила вывод являются допустимыми:}
	\begin{tabular}{p{5cm} p{5cm} p{5cm}}
		$ \displaystyle 1) \quad \frac{\varphi \vdash \psi}{(\varphi \,\&\, \xi) \vdash (\psi \,\&\, \xi)} $ &
		$ \displaystyle 2) \quad \frac{\varphi \vdash \psi}{(\xi \,\&\, \varphi) \vdash (\xi \,\&\, \psi)} $ &
		$ \displaystyle 3) \quad \frac{\varphi \vdash \psi}{(\varphi \vee \xi) \vdash (\psi \vee \xi)} $ \\ \\
		
		$ \displaystyle 4) \quad \frac{\varphi \vdash \psi}{(\xi \vee \varphi) \vdash (\xi \vee \psi)} $ &
		$ \displaystyle 5) \quad \frac{\varphi \vdash \psi}{(\varphi \rightarrow \xi) \vdash (\psi \rightarrow \xi)} $ &
		$ \displaystyle 6) \quad \frac{\varphi \vdash \psi}{(\xi \rightarrow \varphi) \vdash (\xi \rightarrow \psi)} $ \\ \\
		
		$ \displaystyle 7) \quad \frac{\varphi \vdash \psi}{\neg \psi \vdash \neg \varphi} $ &
		$ \displaystyle 8) \quad \frac{\varphi \vdash \psi}{\forall x \, \varphi \vdash \forall x \,\psi} $ &
		$ \displaystyle 9) \quad \frac{\varphi \vdash \psi}{\exists x \, \varphi \vdash \exists x \,\psi} $ \\
	\end{tabular}
	
\subsection{Теорема о замене:}
	$ \psi' = [\psi]_{\varphi'}^{\varphi} $, где $\varphi \equiv \varphi'$, то $ \psi' \equiv \psi $
\paragraph*{Док-во:} \hangindent=1.73cm
	\begin{enumerate}
		\item $\ln(\psi)=0, \psi = \varphi $
		\item $\ln(\psi)=n $ \\
			$ \forall \xi \, \ln(\xi)<n $ - теорема верна
			\begin{enumerate}
				\item $ \psi = \psi_{1}\,\&\, \psi_{2} \quad \ln(\psi_{1}) < n, \ln(\psi_{2})<n.$
					\begin{enumerate}
						\item $ \psi' = [\psi_{1}]_{\varphi}^{\varphi'} \,\&\, \psi_{2} $: \\
							$ \psi_{1}' = [\psi_{1}]_{\varphi}^{\varphi_{1}} $ \\
							$ \psi_{1}' \equiv \psi_{1} $ по индукционному предположению. Отсюда следуют 2 пункта: \\
							$ \psi_{1} \vdash \psi_{1}' $ - доказуема. По (1.3.1) $ (\psi_{1} \,\&\, \psi_{2}) \vdash (\psi_{1}' \,\&\, \psi_{2}) $ - доказуема. \\
							$ \psi_{1}' \vdash \psi_{1} $ - доказуема. По (1.3.1) $ (\psi_{1}' \,\&\, \psi_{2}) \vdash (\psi_{1} \,\&\, \psi_{2}) $ - доказуема. \\
							Получаем, что $ (\psi_{1} \,\&\, \psi_{2}) \equiv (\psi_{1}' \,\&\, \psi_{2}) \Rightarrow \psi \equiv \psi' $
						\item $ \psi' = \psi_{1} \,\&\, [\psi_{1}]_{\varphi}^{\varphi'} $ - делается через (1.3.2).
					\end{enumerate}
				\item $ \psi = \psi_{1} \,\vee\, \psi_{2} $ - с помощью (1.3.3) и (1.3.4).
				\item $ \psi = \psi_{1} \rightarrow \psi_{2} $ - с помощью (1.3.5) и (1.3.6).
				\item $ \psi = \neg \psi_{1} $ - с помощью (1.3.7).
				\item $ \psi = \forall x \, \psi_{1} $ \\
					$ \psi' = \forall x \, [ \psi_{1}]_{\varphi}^{\varphi'}, \quad \ln(\psi_{1}) = n-1 $. Применяем мега-индукцию по кол-ву связок и кванторов. \\
					$ \psi_{1}' = [\psi_{1}]_{\varphi}^{\varphi'}, \quad \psi_{1}' \equiv \psi{1} $ - по индуктивном предположению. \\ Используем (1.3.8):
					\begin{equation}
						\frac{\psi_{1} \vdash \psi_{1}'}{\forall x \, \psi_{1} \vdash \forall x \, \psi_{1}'}, \quad
						\frac{\psi_{1}' \vdash \psi_{1}}{\forall x \, \psi_{1}' \vdash \forall x \, \psi_{1}} \notag
					\end{equation}
					Прыгаем, радуемся и хлопаем ушами.
				\item $ \psi = \exists x \, \psi_{1} $ - доказывается аналогично предыдущему через (1.3.9).
			\end{enumerate}
	\end{enumerate}
	
\subsection{Определение (Семантика исчисления предикатов):}
	\begin{enumerate}
		\item $ \Gamma \vdash \varphi $ - т.и. \\
			$ \forall \mathfrak{A} \in K(\sigma(\Gamma, \varphi)) \\
			\forall \gamma \colon FV(\Gamma, \varphi) \rightarrow |\mathfrak{A}| \\
			\exists \psi \in \Gamma : \mathfrak{A} \not\vDash \psi [\gamma] \text{ или } \mathfrak{A} \vDash \psi [\gamma] $
		\item $ \vdash \varphi $ - т.и. \\
		$ \forall \mathfrak{A} \in K(\sigma(\varphi)) $ \\
		$ \forall \gamma \colon FV(\Gamma, \varphi) \rightarrow |\mathfrak{A}| $ \\
		$ \mathfrak{A} \vDash \varphi[\gamma] $
		\item $ \Gamma \vdash $ - т.и. \\
			$ \forall \mathfrak{A} \in K(\sigma(\Gamma)) $ \\
			$ \forall \gamma \colon FV(\Gamma) \rightarrow |\mathfrak{A}| $ \\
			$ \exists \psi \in \Gamma : \mathfrak{A} \nvDash \psi [\gamma] $
	\end{enumerate}
	
\subsection{Замечания:}
	\begin{enumerate}
		\item $ \vdash \varphi \text{ - т.и. } \Leftrightarrow \varphi $ - т.и.
		\item $ \varphi_{1}, \ldots, \varphi_{n} \vdash \text{ - т.и. } \Leftrightarrow (\varphi_{1} \,\&\, \ldots \,\&\,  \varphi_{n}) $ - т.и.
	\end{enumerate}

	
\subsection{Теорема о корректности:}
	Если секвенция доказуема, то она тождественно истинна.

\end{document}
