10-leccia.tex

\subsection{Лекция 10}

\subsubsection{Свойства выводимости, теория Хенкина}
% В нумерации лектора это девятый раздел
% TODO: (оформление) не стоит создавать отдельные subsection для лекций, а вот для тем надо бы. Но оставить обозначение границ лекций было бы удобно – так легче искать конспект по номеру лекции.

% TODO: Добавить этот раздел. Примерно первые пятьдесят минут 10 лекции. Пара определений + задания из девятого ДЗ целиком + схема доказательства задачи 5

%\begin{definition}
    %$\text{ИП}_\sigma$ -- исчисление предикатов в сигнатуре $\sigma$ (со всеми тавтологиями). $\text{ИП}^*_\sigma$ (только с основными тавтологиями)
%\end{definition}
%
%Из теоремы о полноте исчисления высказываний очевидно, что они эквивалентны. Так как любая тавтология может быть выведена из основных тавтологий с помощью правил вывода исчисления высказываний.

\subsubsection{Теоремы о существовании модели и полноте $\text{ИП}_\sigma$}
% В нумерации лектора это десятый раздел
% Начинается примерно на 50 минуте 10 лекции

\begin{theorem}[О существовании модели]
Любое непротиворечивое множество предложений имеет модель.
\end{theorem}

\begin{proof}
    Пусть $S$ -- непротиворечивое множество предложений сигнатуры $\sigma$. Хотим показать, что $S$ имеет модель. По теореме о компактности можем считать, что $S$ конечна. Тогда в формулы $S$ входит конечное подмножество символов сигнатуры $\sigma$, поэтому можно считать, что $\sigma$ конечна. Тогда, по доказанному выше факту, существует теория Хенкина $T$ сигнатуры $\sigma_C$, расширяющая $S$.

    Пусть $M$ -- множество всех термов сигнатуры $\sigma_C$, не содержащих переменных (то есть это константы с "накрученными" на них функциональными символами). Введём на этом множестве отношение $\sim$ следующим образом: $s\sim t$, если $T\vdash s=t$.

    Дальше проверяем несколько несложных утверждений:
    \begin{enumerate}
        \item $\sim$ является отношением эквивалентности
        \item Если $s_1\sim t_1, \ldots, s_n\sim t_n$, выполняется $T\vdash P(s_1, \ldots, s_n)$, то $T\vdash P(t_1, \ldots, t_n)$
        \item Если $s_1\sim t_1, \ldots, s_n\sim t_n$, то $f(s_1, \ldots, s_n)\sim f(t_1, \ldots, t_n)$
        \item Пусть $t = t(x_1, \ldots, x_n)$ -- терм, $s_1, \ldots, s_n\in M$. Тогда $t^\mathbb{A}([s_1], \ldots, [s_n]) = [t(s_1, \ldots, s_n)]$
        \item %TODO
    \end{enumerate}
\end{proof}