lection-02.tex

\documentclass[aspectratio=169]{beamer}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{cmll}
\usepackage{xcolor}
\usepackage{proof}
\setbeamertemplate{navigation symbols}{}
%\usetheme{Warsaw}
\begin{document}

\newtheorem{axiom}{Аксиома}
\newtheorem{exmprus}{Пример}
\newtheorem{defrus}{Определение}
\newtheorem{lemmarus}{Лемма}
\newtheorem{thmrus}{Теорема}

\begin{frame}{}
\begin{center}\Large Теоремы об исчислении высказываний.\end{center}
\end{frame}

\begin{frame}{Контекст, метаязык}

Будем обозначать большими греческими буквами середины
алфавита, возможно с индексами, ($\Gamma$, $\Delta_1$, ...) списки формул.
Будем использовать, где удобно:

$$\Gamma \vdash \alpha$$\pause

Списки можно указывать через запятую:

$$\Gamma, \Delta, \zeta \vdash \alpha$$\pause
это означает то же, что и 
$$\gamma_1,\gamma_2,\dots,\gamma_n,\delta_1,\delta_2,\dots,\delta_m,\zeta\vdash\alpha$$
если 
$$\Gamma = \{\gamma_1,\gamma_2,\dots,\gamma_n\},\quad \Delta = \{\delta_1,\delta_2,\dots,\delta_m\}$$

\end{frame}

\begin{frame}{Теорема о дедукции}

\begin{theorem}[О дедукции, Жак Эрбран, 1930]
$\Gamma,\alpha\vdash\beta$ выполнено тогда и только тогда, когда выполнено $\Gamma\vdash\alpha\rightarrow\beta$
\end{theorem}\pause

\vspace{0.5cm}
Доказательство <<в две стороны>>, сперва <<справа налево>>.
Пусть $\Gamma\vdash\alpha\rightarrow\beta$, покажем $\Gamma,\alpha\vdash\beta$\pause\vspace{0.5cm}

То есть по условию существует вывод: $$\delta_1, \delta_2, \dots, \delta_{n-1}, \alpha\rightarrow\beta$$\pause

Тогда следующая последовательность --- тоже вывод: 
$$\delta_1, \delta_2, \dots, \delta_{n-1}, \alpha\rightarrow\beta, \alpha, \beta$$

%Рассмотрим формулу $(A \rightarrow B) \rightarrow (\neg B)$

\end{frame}

\begin{frame}{Доказательство: $\Gamma\vdash\alpha\rightarrow\beta$ влечёт $\Gamma,\alpha\vdash\beta$}
\begin{tabular}{lll}
№ п/п & формула & пояснение\\
\hline
$(1)$ & $\delta_1$ & в соответствии с исходным доказательством\\
    & $\dots$ \\
$(n-1)$ & $\delta_{n-1}$ & в соответствии с исходным доказательством\\
$(n)$ & $\alpha\rightarrow\beta $ & в соответствии с исходным доказательством\\
$(n+1)$ & $\alpha$ & гипотеза\\
$(n+2)$ & $\beta$ & Modus Ponens n$+1$, $n$
\end{tabular}\pause\vspace{1cm}

Вывод $\Gamma,\alpha\vdash\beta$ предоставлен, первая часть теоремы доказана.
\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$}

Пусть даны формулы вывода $$\delta_1,\delta_2,\dots,\delta_{n-1},\beta$$

Аналогично предыдущему пункту, перестроим вывод.\pause

Построим <<черновик>> вывода, приписав $\alpha$ слева к каждой формуле:
$$\alpha\rightarrow\delta_1,\alpha\rightarrow\delta_2,\dots,\alpha\rightarrow\delta_{n-1},\alpha\rightarrow\beta$$\pause
Данная последовательность формул не обязательно вывод: $\Gamma=\varnothing$, $\alpha = A$
$$A\rightarrow B\rightarrow A$$\pause
припишем $A$ слева --- вывод не получим:
$$A \rightarrow (A\rightarrow B\rightarrow A)$$
\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$}

\begin{proof} (индукция по длине вывода). Утверждение: если данная последовательность $n$ высказываний --- вывод
$\Gamma,\alpha\vdash\beta$, то его можно перестроить в $\Gamma\vdash\alpha\rightarrow\beta$.

\begin{itemize}
\item База $(n=1)$: частный случай перехода (без M.P.).

\item Переход. Пусть $\delta_1, \dots, \delta_{n+1}$ --- исходный вывод. И пусть (по индукционному предположению)
уже перестроен вывод $\delta_1, \dots, \delta_n$ в вывод $\Gamma\vdash\alpha\rightarrow\delta_n$.
Достроим его. Рассмотрим 3 случая.

\begin{enumerate}
\item $\delta_{n+1}$ --- аксиома или $\delta_{n+1} \in \Gamma$ (выполнено без доказательства в новом выводе)\pause
\item $\delta_{n+1}$ --- гипотеза $\alpha$\pause
\item $\delta_{n+1}$ --- получено по правилу Modus Ponens из предыдущих формул $\delta_j$ и 
$\delta_k = \delta_j\rightarrow\delta_{n+1}$.
\end{enumerate}

В каждом из случаев можно дополнить черновик до полноценного вывода.
\end{itemize}\end{proof}

\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$, случай аксиомы}
\begin{tabular}{lll}
№ п/п & новый вывод & пояснение \\
\hline
& \dots\\
$(1)$ & $\alpha\rightarrow\delta_1$ \\
& \dots\\
$(2)$ & $\alpha\rightarrow\delta_2$ \\
    & \dots \\
$(n)$ & $\alpha\rightarrow\delta_n$ \\
 & \color{cyan}$\alpha\rightarrow\delta_{n+1}$ & \color{cyan}$\delta_{n+1}$ --- аксиома, либо $\delta_{n+1} \in \Gamma$\\
\end{tabular}
\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$, случай аксиомы}
\begin{tabular}{lll}
№ п/п & новый вывод & пояснение \\
\hline
& \dots\\
$(1)$ & $\alpha\rightarrow\delta_1$ \\
& \dots\\
$(2)$ & $\alpha\rightarrow\delta_2$ \\
    & \dots \\
\color{cyan}$(n+0.3)$ & \color{cyan}$\delta_{n+1}\rightarrow\alpha\rightarrow\delta_{n+1}$ & \color{cyan}схема аксиом 1\\
\color{cyan}$(n+0.6)$ & \color{cyan}$\delta_{n+1}$ & \color{cyan}аксиома, либо $\delta_{n+1} \in \Gamma$\\
$(n+1)$ & $\alpha\rightarrow\delta_{n+1}$ & Modus Ponens $n+0.6$, $n+0.3$\\
\end{tabular}
\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$, случай $\delta_i=\alpha$}
\begin{tabular}{lll}
№ п/п & новый вывод & пояснение \\
\hline
    & \dots \\
$(1)$ & $\alpha\rightarrow\delta_1$ \\
    & \dots \\
$(2)$ & $\alpha\rightarrow\delta_2$ \\
    & \dots \\
\color{cyan}$(n+0.2)$ & \color{cyan}$\alpha \rightarrow (\alpha \rightarrow \alpha)$ & \color{cyan} Сх. акс. 1\\
\color{cyan}$(n+0.4)$ & \color{cyan}$(\alpha \rightarrow (\alpha \rightarrow \alpha)) \rightarrow 
  (\alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha) \rightarrow
  (\alpha \rightarrow \alpha)$& \color{cyan}Сх. акс. 2\\
\color{cyan}$(n+0.6)$ & \color{cyan}$(\alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha) \rightarrow
  (\alpha \rightarrow \alpha)$ &\color{cyan}M.P. $n+0.2$, $n+0.4$\\
\color{cyan}$(n+0.8)$ & \color{cyan}$\alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha$ & 
    \color{cyan}Сх. акс. 1\\
$(n+1)$ & $\alpha \rightarrow \alpha$ & M.P. $n+0.8$, $n+0.6$\\
\end{tabular}
\end{frame}

\begin{frame}{Доказательство: $\Gamma,\alpha\vdash\beta$ влечёт $\Gamma\vdash\alpha\rightarrow\beta$, случай Modus Ponens}
\begin{tabular}{lll}
№ п/п & новый вывод & пояснение \\
\hline
    & \dots \\
$(1)$ & $\alpha\rightarrow\delta_1$ \\
    & \dots \\
$(2)$ & $\alpha\rightarrow\delta_2$ \\
    & \dots \\
$(j)$ & $\alpha\rightarrow\delta_j$ \\
    & \dots \\
$(k)$ & $\alpha\rightarrow\delta_j\rightarrow\delta_{n+1}$ \\
    & \dots \\
\color{cyan}$(n+0.3)$ & \color{cyan}$(\alpha\rightarrow\delta_j)
    \rightarrow(\alpha\rightarrow\delta_j\rightarrow\delta_{n+1})\rightarrow(\alpha\rightarrow\delta_{n+1})$ & \color{cyan}Сх. акс. 2\\
\color{cyan}$(n+0.6)$ & \color{cyan}$(\alpha\rightarrow\delta_j
    \rightarrow\delta_{n+1})\rightarrow(\alpha\rightarrow\delta_{n+1})$ & \color{cyan}M.P. $j$, $n+0.3$\\
$(n+1)$ & $\alpha\rightarrow\delta_{n+1}$ & Modus Ponens $k$, $n + 0.6$\\
\end{tabular}
\end{frame}

\begin{frame}{Некоторые полезные правила}

\begin{lemmarus}[Правило контрапозиции]Каковы бы ни были формулы $\alpha$ и $\beta$, справедливо, что 
$\vdash (\alpha \rightarrow \beta) \rightarrow (\neg\beta \rightarrow \neg\alpha)$.
\end{lemmarus}\pause

\begin{lemmarus}[правило исключённого третьего]Какова бы ни была формула $\alpha$, $\vdash\alpha\vee\neg\alpha$.
\end{lemmarus}

\begin{lemmarus}[об исключении допущения]
Пусть справедливо $\Gamma, \rho \vdash \alpha$ и $\Gamma, \neg \rho \vdash \alpha$.
Тогда также справедливо $\Gamma \vdash \alpha$.
\end{lemmarus}

\begin{proof}Доказывается с использованием лемм, указанных выше.\end{proof}

\end{frame}

\begin{frame}{Теорема о полноте исчисления высказываний}
\begin{thmrus}Если $\models\alpha$, то $\vdash\alpha$.
\end{thmrus}
\end{frame}

\begin{frame}{Специальное обозначение}
\begin{defrus}[условное отрицание]
Зададим некоторую оценку переменных, такую, что $\llbracket\alpha\rrbracket = x$. 

Тогда \emph{условным отрицанием} формулы $\alpha$ назовём следующую формулу $\llparenthesis\alpha\rrparenthesis$:
$$\llparenthesis\alpha\rrparenthesis = \left\{\begin{array}{ll}\alpha, & x = \textnormal{И}\\
       \neg\alpha, & x = \textnormal{Л}\end{array}\right.$$

\end{defrus}

Аналогично записи для оценок, будем указывать оценку переменных, если это потребуется / будет неочевидно из контекста:
$$\llparenthesis \neg X \rrparenthesis^{X:=\textnormal{Л}} = \neg X\quad\quad\quad\llparenthesis \neg X \rrparenthesis^{X:=\textnormal{И}} = \neg\neg X$$

Также, если $\Gamma = \gamma_1, \gamma_2, \dots, \gamma_n$, то за $\llparenthesis \Gamma \rrparenthesis$ обозначим $\llparenthesis \gamma_1 \rrparenthesis, \llparenthesis \gamma_2 \rrparenthesis, \dots \llparenthesis \gamma_n \rrparenthesis$.
\end{frame}

\begin{frame}{Таблицы истинности и высказывания}

Рассмотрим связку <<импликация>> и её таблицу истинности:

\begin{center}\begin{tabular}{cccc}
$\llbracket A\rrbracket$ & $\llbracket B\rrbracket$ & $\llbracket A\rightarrow B\rrbracket$ & формула\\\hline
Л & Л & И & $\neg A, \neg B \vdash A \rightarrow B$\\
Л & И & И & $\neg A, B \vdash A \rightarrow B$\\
И & Л & Л & $A, \neg B \vdash \neg (A \rightarrow B)$\\
И & И & И & $A, B \vdash A \rightarrow B$
\end{tabular}\end{center}\pause

Заметим, что с помощью условного отрицания данную таблицу можно записать в одну строку:

$$\llparenthesis A \rrparenthesis, \llparenthesis B \rrparenthesis \vdash \llparenthesis A \rightarrow B \rrparenthesis $$

\end{frame}


\begin{frame}{Полнота исчисления высказываний}

\begin{thmrus}[О полноте исчисления высказываний]
Если $\models\alpha$, то $\vdash\alpha$
\end{thmrus}\pause

\begin{enumerate}
\item Построим таблицы истинности для каждой связки $(\star)$ и докажем в них каждую строку:
$$ \llparenthesis\varphi\rrparenthesis, \llparenthesis\psi\rrparenthesis \vdash \llparenthesis\varphi\star\psi\rrparenthesis$$\pause
\vspace{-0.5cm}
\item Построим таблицу истинности для $\alpha$ и докажем в ней каждую строку:
$$\llparenthesis \Xi \rrparenthesis \vdash \llparenthesis \alpha \rrparenthesis$$\pause
\vspace{-0.5cm}
\item Если формула общезначима, то в ней все строки будут иметь вид $\llparenthesis \Xi \rrparenthesis \vdash\alpha$,
потому от гипотез мы сможем избавиться и получить требуемое $\vdash\alpha$.
\end{enumerate}

\end{frame}

\begin{frame}{Шаг 1. Лемма о связках}

Запись

$$\llparenthesis\varphi\rrparenthesis, \llparenthesis\psi\rrparenthesis \vdash \llparenthesis\varphi\star\psi\rrparenthesis$$

сводится к 14 утверждениям:

\begin{center}\begin{tabular}{rclp{1cm}rcl}
$\neg\varphi, \neg\psi$&$ \vdash $&$\neg (\varphi \with \psi)$& & $\neg\varphi, \neg\psi$&$ \vdash $&$     (\varphi \rightarrow  \psi)$ \\
$\neg\varphi,     \psi$&$ \vdash $&$\neg (\varphi \with \psi)$& &$\neg\varphi,     \psi$&$ \vdash $&$     (\varphi \rightarrow  \psi)$ \\
$    \varphi, \neg\psi$&$ \vdash $&$\neg (\varphi \with \psi)$& &$ \varphi, \neg\psi$&$ \vdash $&$\neg (\varphi \rightarrow  \psi)$ \\
$    \varphi,     \psi$&$ \vdash $&$     (\varphi \with \psi)$& &$    \varphi,     \psi$&$ \vdash $&$     (\varphi \rightarrow  \psi)$ \\
$\neg\varphi, \neg\psi$&$ \vdash $&$\neg (\varphi \vee  \psi)$& &$    \varphi          $&$ \vdash $&$     \neg\neg\varphi$ \\
$\neg\varphi,     \psi$&$ \vdash $&$     (\varphi \vee  \psi)$& &$\neg\varphi          $&$ \vdash $&$         \neg\varphi$\\
$    \varphi, \neg\psi$&$ \vdash $&$     (\varphi \vee  \psi)$ \\
$    \varphi,     \psi$&$ \vdash $&$     (\varphi \vee  \psi)$
\end{tabular}\end{center}
\end{frame}

\begin{frame}{Шаг 2. Обобщение на любую формулу}

\begin{lemmarus}[Условное отрицание формул]
Пусть пропозициональные переменные $\Xi = X_1, \dots, X_n$ ---
все переменные, которые используются в формуле $\alpha$. И пусть
задана некоторая оценка переменных.

Тогда, $\llparenthesis \Xi \rrparenthesis \vdash\llparenthesis\alpha\rrparenthesis$
\end{lemmarus}\pause

\begin{proof}Индукция по длине формулы $\alpha$.
\begin{itemize}
\item База: формула $\alpha$ --- атомарная, т.е. $\alpha = X_i$. Тогда при любом $\Xi$ выполнено 
$\llparenthesis\Xi\rrparenthesis^{X_i := \text{И}} \vdash X_i$ и $\llparenthesis\Xi\rrparenthesis^{X_i := \text{Л}} \vdash \neg X_i$.
\item Переход: $\alpha = \varphi\star\psi$, причём $\llparenthesis\Xi\rrparenthesis\vdash\llparenthesis\varphi\rrparenthesis$
и $\llparenthesis\Xi\rrparenthesis\vdash\llparenthesis\psi\rrparenthesis$\pause

Тогда построим вывод: 

\begin{tabular}{lll}
$(1)\dots(n)$ & $\llparenthesis\varphi\rrparenthesis$ & индукционное предположение\\
$(n+1)\dots(k)$ & $\llparenthesis\psi\rrparenthesis$ & индукционное предположение\\
$(k+1)\dots(l)$ & $\llparenthesis\varphi\star\psi\rrparenthesis$ & 
  лемма о связках: $\llparenthesis\varphi\rrparenthesis$ и $\llparenthesis\psi\rrparenthesis$ доказаны выше,\\
  & & значит, их можно использовать как гипотезы
\end{tabular}
\end{itemize}
\end{proof}

\end{frame}

\begin{frame}{Шаг 3. Избавляемся от гипотез}

\begin{lemmarus}Пусть при всех оценках переменных
$\llparenthesis\Xi\rrparenthesis \vdash \alpha$, тогда
$\vdash\alpha$.
\end{lemmarus}\pause

\begin{proof}
Индукция по количеству переменных $n$.

\begin{itemize}
\item База: $n=0$. Тогда $\vdash\alpha$ есть из условия.\pause
\item Переход: пусть $\llparenthesis X_1, X_2,  \dots X_{n+1} \rrparenthesis \vdash \alpha$.
Рассмотрим $2^n$ пар выводов:
$$\infer
  {\llparenthesis X_1, X_2, \dots X_n \rrparenthesis \vdash \alpha}
  {\llparenthesis X_1, X_2, \dots X_n\rrparenthesis,\neg X_{n+1} \vdash \alpha\quad\quad 
   \llparenthesis X_1, X_2, \dots X_n\rrparenthesis,X_{n+1} \vdash \alpha
}$$
\end{itemize}
При этом, $\llparenthesis X_1, X_2, \dots X_n \rrparenthesis  \vdash \alpha$ при всех оценках
переменных $X_1, \dots X_n$. Значит, $\vdash\alpha$ по индукционному предположению.
\end{proof}

\end{frame}

\begin{frame}{Заключительные замечания}
Теорема о полноте --- конструктивна. Получающийся вывод --- экспоненциальный по длине.

Несложно по изложенному доказательству разработать программу, строящую вывод.

Вывод для формулы с 3 переменными --- порядка 3 тысяч строк.

\end{frame}

\begin{frame}
\LARGE\begin{center}Интуиционистская логика\end{center}
\end{frame}

\begin{frame}{Критика доказательств чистого существования}

\begin{thmrus}Существует пара иррациональных чисел $a$ и $b$,
такая, что $a^b$ — рационально.
\end{thmrus}\pause

\begin{itemize}
\item $2^5$, $3^3$, $7^{10}$, $\sqrt{2}^2$ — рациональны;
\item $2^{\sqrt{2}}$, $e ^ \pi$ — иррациональны;
\item задача выглядит довольно сложно.
\end{itemize}
\end{frame}

\begin{frame}{Критика доказательств чистого существования}
\begin{thmrus}Существует пара иррациональных чисел $a$ и $b$,
такая, что $a^b$ — рационально.
\end{thmrus}

\begin{proof}
Рассмотрим $a = b = \sqrt{2}$ и рассмотрим $a^b$.
Возможны два варианта:

\begin{enumerate}
\item $a^b = \sqrt{2}^{\sqrt{2}}$ — рационально;
\item $a^b = \sqrt{2}^{\sqrt{2}}$ — иррационально; отлично, 
тогда возьмём $a_1 = \sqrt{2}^{\sqrt{2}}$ и получим
$$a_1^b = \left({\sqrt{2}^{\sqrt{2}}}\right)^{\sqrt{2}} = \sqrt{2}^2 = 2$$
\end{enumerate}
\end{proof}

\end{frame}

\begin{frame}{Интуиционизм}

``Over de Grondslagen der Wiskunde'' (Брауэр, 1907 г.)

Основные положения:
\begin{enumerate}
\item Математика не формальна.
\item Математика независима от окружающего мира.
\item Математика не зависит от логики — это логика зависит от математики.
\end{enumerate}


%\begin{center}
%\includegraphics[width=3cm]{brower}
%
%Лёйтзен Брауер\end{center}

%Критика доказательств чистого существования
\end{frame}

\begin{frame}{BHK-интерпретация логических связок}

BHK — это сокращение трёх фамилий: Брауэр, Гейтинг, Колмогоров. \pause

\vspace{1cm}

Пусть $\alpha$, $\beta$ --- некоторые конструкции, тогда:\pause

\begin{itemize}
\item $\alpha\ \&\ \beta$ построено, если построены $\alpha$ и $\beta$ \pause
\item $\alpha \vee \beta$ построено, если построено $\alpha$ или $\beta$,
и мы знаем, что именно \pause
\item $\alpha\rightarrow\beta$ построено, если есть способ перестроения
$\alpha$ в $\beta$\pause
\item $\bot$ — конструкция, не имеющая построения\pause
\item $\neg\alpha$ построено, если построено $\alpha\rightarrow\bot$
\end{itemize}
\end{frame}

\begin{frame}{Дизъюнкция}

Конструкция $\alpha\vee\neg\alpha$ не имеет построения в общем случае.
Что может быть построено: $\alpha$ или $\neg\alpha$?\pause

\vspace{1cm}

Возьмём за $\alpha$ нерешённую проблему, например, $P = NP$\pause
\vspace{1cm}

Авторам в данный момент не известно, выполнено $P = NP$ или же $P \ne NP$.
\end{frame}

\begin{frame}{Импликация}

Высказывание общезначимо в И.В. и не выполнено в BHK-интерпретации:
$$(A \rightarrow B) \vee (B \rightarrow C) \vee (C \rightarrow A)$$\pause

Давайте дадим следующий смысл пропозициональным переменным:
\begin{itemize}
\item $A$ --- идёт дождь
\item $B$ --- светит солнце
\item $C$ --- в прошлом году я получил пятёрку по матанализу
\end{itemize}\pause

Импликацию можно понимать как <<формальную>> и как <<материальную>>.
\begin{itemize}
\item Материальная импликация $A\rightarrow B$ для автора в данный момент
выполнена, поскольку дождя за окном не идёт.\pause

\item Формальная импликация $A\rightarrow B$ места не имеет.
\end{itemize}

\end{frame}

\begin{frame}{Формализация}
Формализация интуиционистской логики возможна, но интуитивное понимание --- основное.

\begin{defrus}Аксиоматика интуиционистского исчисления высказываний в гильбертовском стиле: 
аксиоматика КИВ, в которой 10 схема аксиом

\begin{center}\begin{tabular}{ll}
(10) & $\neg \neg \alpha \rightarrow \alpha$
\end{tabular}\end{center}

заменена на 

\begin{center}\begin{tabular}{ll}
(10и) & $\alpha \rightarrow \neg\alpha \rightarrow \beta$
\end{tabular}\end{center}
\end{defrus}
\end{frame}

\begin{frame}{Теория моделей: битовые шкалы и множества как модели для КИВ}

Оценка: размер шкалы $n$ (множество $X$) и функция $f: P \rightarrow 2^n-1$ ($f : P \rightarrow \mathcal{X}$).

\begin{center}\begin{tabular}{lll} 
 КИВ & Битовые шкалы & Множества \\\hline
 $V$ & $0 \dots 2^{n}-1$ & $\mathcal{P}(X)$ \\
 истина & \texttt{1 shl n - 1} & $X$\\
 $\llbracket \alpha \with \beta \rrbracket$ & $\llbracket \alpha \rrbracket\texttt{ and }\llbracket \beta \rrbracket$  & $\llbracket \alpha \rrbracket \cap \llbracket \beta \rrbracket$\\
 $\llbracket \alpha \vee \beta \rrbracket$ & $\llbracket \alpha \rrbracket\texttt{ or }\llbracket \beta \rrbracket$ & $\llbracket \alpha \rrbracket \cup \llbracket \beta \rrbracket$\\
 $\llbracket \alpha \rightarrow \beta \rrbracket$ & $((\texttt{not } \llbracket \alpha \rrbracket)\texttt{ or }\llbracket \beta \rrbracket) {\color{blue}\texttt{ and (1 shl n - 1)}}$ & $(X \setminus \llbracket \alpha \rrbracket) \cup \llbracket \beta \rrbracket$\\
 $\llbracket \neg\alpha \rrbracket$ & $(\texttt{not } \llbracket \alpha \rrbracket){\color{blue}\texttt{ and (1 shl n - 1)}} $ & $X \setminus \llbracket \alpha \rrbracket$\\
\end{tabular}\end{center}

\begin{exmprus}Пусть $X = \{ \square, \star, \circ \}$, $A = \{ \square \}$, $B = \{\circ\}$, тогда 
\begin{center}\begin{tabular}{rl}
$\llbracket A \rightarrow A\vee B \rrbracket = $& $\left(X \setminus \{ \square \}\right) \cup (\{\square\}\cup\{\circ\}) = \{\star,\circ\}\cup\{\square,\circ\} = X$ \\
$\llbracket A \rightarrow B\rrbracket =$ & $(X \setminus \{ \square \}) \cup \{ \circ \} = \{ \star, \circ \} \ne X$
\end{tabular}\end{center}
\end{exmprus}
\end{frame}

\begin{frame}{Теория моделей ИИВ: топологическая модель}

Оценка задаётся пространством $\langle X, \Omega \rangle$ и функцией $f : P \rightarrow \Omega$.

\begin{center}\begin{tabular}{lll} 
 И.В. & Множества (КИВ) & Топология (ИИВ) \\\hline
 $V$ & $\mathcal{P}(X)$ & $\Omega$ \\
 истина & $X$ & $X$\\
 $\llbracket \alpha \with \beta \rrbracket$  & $\llbracket \alpha \rrbracket \cap \llbracket \beta \rrbracket$  & $\llbracket \alpha \rrbracket \cap \llbracket \beta \rrbracket$\\
 $\llbracket \alpha \vee \beta \rrbracket$ & $\llbracket \alpha \rrbracket \cup \llbracket \beta \rrbracket$ & $\llbracket \alpha \rrbracket \cup \llbracket \beta \rrbracket$\\
 $\llbracket \alpha \rightarrow \beta \rrbracket$ & $(X \setminus \llbracket \alpha \rrbracket) \cup \llbracket \beta \rrbracket$ &  $((X \setminus \llbracket \alpha \rrbracket) \cup \llbracket \beta \rrbracket)^\circ$\\
 $\llbracket \neg\alpha \rrbracket$ & $X \setminus \llbracket \alpha \rrbracket$ & $(X \setminus \llbracket \alpha \rrbracket)^\circ$\\
\end{tabular}\end{center}

\begin{defrus}$\models \alpha$, если $\llbracket\alpha\rrbracket$ истинно во всех пространствах при всех функциях оценки.\end{defrus}

\begin{thmrus}ИИВ с топологической интерпретацией корректна и полна.\end{thmrus}
\end{frame}

\begin{frame}{Закон исключённого третьего не выполнен в ИИВ}
Несколько схожих формулировок (упорядочены по убыванию силы): $\alpha \rightarrow \neg\neg \alpha$, $\alpha \vee \neg\alpha$, $((\alpha\rightarrow\beta)\rightarrow\alpha)\rightarrow\alpha$.

\begin{thmrus}$\not\vdash A \vee \neg A$ в интуиционистском исчислении высказываний.
\end{thmrus}
\begin{proof}
$X = \mathbb{R}$, $A = (0,1)$, $\llbracket A \vee \neg A \rrbracket = (0,1)\cup((-\infty,0]\cup[1,\infty))^\circ = (-\infty,0)\cup(0,1)\cup(1,\infty) \ne \mathbb{R}$
\end{proof}

\end{frame}

\end{document}