lection-07.tex

\documentclass[aspectratio=169]{beamer}
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{cancel}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{cmll}
\usepackage{graphicx}
\usepackage{amsthm}
\usepackage{tikz}
\usetikzlibrary{patterns}
\usepackage{chronosys}
\usepackage{proof}
\usepackage{multirow}
\usepackage{multicol}
\setbeamertemplate{navigation symbols}{}
%\usetheme{Warsaw}

\newtheorem{thm}{Теорема}[section]
\newtheorem{lmm}{Лемма}[section]
\newtheorem{dfn}{Определение}[section]
\newtheorem{exm}{Пример}[section]
\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}
\newcommand\mdoubleplus{\ensuremath{\mathbin{+\mkern-10mu+}}}

\begin{document}

\begin{frame}
\begin{center}\Large {\it Лекция 7}\\\vspace{0.5cm}
Неразрешимость исчисления предикатов\\
Аксиоматика Пеано и формальная арифметика
\end{center}
\end{frame}

\begin{frame}{Общие результаты об исчислениях}
\begin{tabular}{llll}
      & К.И.В. & И.И.В. & К.И.П.\\\hline
корректность & да (лекция 1) & да (ДЗ III.9) & да (лекция 5)\\
непротиворечивость & да (очев.) & да (из непр. КИВ) & да (лекция 6)\\
полнота & да (лекция 2) & да (будет в лабах) & да (лекция 6)\\
разрешимость & да (лекция 2) & да (будет в лабах) & \pause\color{red}Нет (сейчас)
\end{tabular}
\end{frame}

\begin{frame}{Полнота ИП доказывается от противного}
\begin{enumerate}
\item Противоречиво ли $\{\neg\varphi\}$? Видимо, <<метод Британского музея>>: перебрать все доказуемые формулы. 
\item Если в процессе нашли $\neg\varphi \vdash \alpha \with \neg \alpha$, то $\vdash\varphi$ (способ перестроения --- см. ДЗ VI.3).
\item Если, {\color{olive}перебрав все $\aleph_0$ формул,} противоречия не нашли --- значит, есть модель $\{\neg\varphi\}$, и $\not\vdash\varphi$.
\item Итого: теорема о полноте ИП не поможет найти доказательство.
\end{enumerate}
\end{frame}

\begin{frame}{Машина Тьюринга}
\begin{dfn}Машина Тьюринга:
\begin{enumerate}
\item Внешний алфавит $q_1, \dots, q_n$, выделенный символ-заполнитель $q_\varepsilon$
\item Внутренний алфавит (состояний) $s_1, \dots, s_k$; $s_s$ --- начальное, $s_f$ --- допускающее, $s_r$ --- отвергающее.
\item Таблица переходов $\langle k, s \rangle \Rightarrow \langle k', s', \leftrightarrow \rangle$
\end{enumerate}
\end{dfn}

\begin{dfn}Состояние машины Тьюринга:
\begin{enumerate}
\item Бесконечная лента с символом-заполнителем $q_\varepsilon$, текст конечной длины.
\item Головка над определённым символом.
\item Символ состояния (состояние в узком смысле) --- символ внутреннего алфавита.
\end{enumerate}
\end{dfn}

\end{frame}

\begin{frame}{Машина, меняющая все 0 на 1, а все 1 --- на 0}
\begin{enumerate}
\item Внешний алфавит $\varepsilon, 0, 1$.
\item Внутренний алфавит $s_s, s_f$ (начальное и допускающее состояния соответственно).
\item Переходы:

\begin{tabular}{l|lll}
    & $\varepsilon$ & 0 & 1\\\hline
$s_s$ & $\langle s_f,\varepsilon,\cdot\rangle$ & $\langle s_s,1,\rightarrow\rangle$ & $\langle s_s,0,\rightarrow\rangle$\\
$s_f$ & $\langle s_f,\varepsilon,\cdot\rangle$ & $\langle s_f,0,\cdot\rangle$ & $\langle s_f,1,\cdot\rangle$
\end{tabular}
\end{enumerate}\pause

\begin{exm}
Головка --- на первом символе $011$, состояние $s_s$.\pause

$\underline{0}11$ \pause $\Rightarrow 1\underline{1}1$ \pause $\Rightarrow 10\underline{1}$ \pause $\Rightarrow 100\underline{\varepsilon}$
\pause

Состояние $s_f$, допускающее.
\end{exm}

\end{frame}

\begin{frame}{Разрешимость}
\begin{dfn}Язык --- множество строк\end{dfn}
\begin{dfn}Язык $L$ разрешим, если существует машина Тьюринга, которая для любого слова $w$ переходит в допускающее состояние, если $w \in L$,
и в отвергающее, если $w \notin L$.\end{dfn}
\end{frame}

\begin{frame}{Неразрешимость задачи останова}
\begin{dfn}Рассмотрим все возможные описания машин Тьюринга. Составим упорядоченные пары: описание машины Тьюринга и входная строка.
Из них выделим язык останавливающихся на данном входе машин Тьюринга.\end{dfn}
\begin{thm}Язык всех останавливающихся машин Тьюринга неразрешим\end{thm}
\begin{proof}От противного. Пусть $S(x,y)$ --- машина Тьюринга, определяющая, остановится ли машина $x$, примененная к строке $y$.\pause
\begin{center}W(x) = if (S(x,x)) \{ while (true); return 0; \} else \{ return 1; \}\end{center}\pause
Что вернёт $S(code(W),code(W))$?
\end{proof}
\end{frame}

\begin{frame}{Кодируем состояние}
\begin{enumerate}
\item внешний алфавит: $n$ 0-местных функциональных символов $q_1, \dots, q_n$; $q_\varepsilon$ --- символ-заполнитель.
\item список: $\varepsilon$ и $c(l,s)$; <<abc>> представим как $c(q_a,c(q_b,c(q_c,\varepsilon)))$.
\item положение головки: <<$ab\underline{p}q$>> как $(c(q_b,c(q_a,\varepsilon)), c(q_p,c(q_q,\varepsilon)))$.
\item внутренний алфавит: $k$ 0-местных функциональных символов $s_1, \dots, s_k$. Из них выделенные $s_s$ --- начальное и
$s_f$ --- допускающее состояние.
\end{enumerate}
\end{frame}
OA
\begin{frame}{Достижимые состояния}
Предикатный символ $F_{x,y}(w_l,w_r,s)$: если у машины $x$ с начальной строкой $y$ состояние $s$ достижимо на строке $rev(w_l) @ w_r$. 
\pause
Будем накладывать условия: семейство формул $C_m$. \pause
Очевидно, начальное состояние достижимо:
$$C_0 = F_{x,y}(\varepsilon,y,s_s)$$
\end{frame}


\begin{frame}{Кодируем переходы}
\begin{enumerate}
\item Занумеруем переходы.\pause
\item Закодируем переход $m$: $$\langle k, s \rangle \Rightarrow \langle k', s', \rightarrow \rangle$$
$C_m = \forall w_l.\forall w_r.F_{x,y}(w_l,c(q_k,w_r),s_s) \rightarrow F_{x,y}(c(q_{k'},w_l),w_r,s_{s'})$\pause

\item Переход посложнее:
$$\langle k, s \rangle \Rightarrow \langle k', s', \leftarrow \rangle$$
$C_m = \forall w_l.\forall w_r.\forall t.F_{x,y}(c(t,w_l),c(q_k,w_r),s_s) \rightarrow F_{x,y}(w_l,c(t,c(q_{k'},w_r)),s_{s'}) \with
\forall w_l.\forall w_r.F_{x,y}(\varepsilon,c(q_k,w_r),s_s) \rightarrow F_{x,y}(\varepsilon,c(q_\varepsilon,c(q_{k'},w_r)),s_{s'})$\\
\pause
\item и т.п.
\end{enumerate}
\end{frame}

\begin{frame}{Итоговая формула}
$$C = C_0 \with C_1 \with \dots \with C_n$$
<<правильное начальное состояние и правильные переходы между состояниями>>\pause

\begin{thm}
состояние $s$ со строкой $rev(w_l)@w_r$ достижимо тогда и только тогда, когда
$C \vdash F_{x,y}(w_l,w_r,s)$\pause
\end{thm}
\begin{proof}
$(\Leftarrow)$ Рассмотрим модель: предикат $F_{x,y}(w_l,w_r,s)$ положим истинным, если состояние достижимо. \pause
Это --- модель для $C$ (по построению $C_m$). \pause
Значит, доказуемость влечёт истинность (по корректности). \pause

$(\Rightarrow)$ Индукция по длине лога исполнения.
\end{proof}
\end{frame}

\begin{frame}{Неразрешимость исчисления предикатов: доказательство}
\begin{thm}Язык всех доказуемых формул исчисления предикатов неразрешим\end{thm}
Т.е. нет машины Тьюринга, которая бы по любой формуле $\alpha$ определяла, доказуема ли она.\pause
\begin{proof} $s_f$ --- допускающее состояние.\pause

Умение определять доказуемость формулы $\exists w_l.\exists w_r.F_{x,\alpha}(w_l,w_r,s_f)$ разрешает задачу останова.
\end{proof}
\end{frame}

\begin{frame}
\begin{center}{\LARGE Аксиоматика Пеано и формальная арифметика}\end{center}

\end{frame}


\begin{frame}{Формализуем дальше: числа}

{\itshape \hfill \begin{tabular}{r} <<Бог создал целые числа, всё остальное — дело рук человека.>>\\
                                 Леопольд Кронекер, 1886 г.\end{tabular}}\pause
\begin{enumerate}
\item Рациональные ($\mathbb{Q}$).\pause

      $Q = \mathbb{Z} \times \mathbb{N}$ --- множество всех простых дробей.\pause

      $\langle p,q \rangle$ --- то же, что $\frac{p}{q}$ \pause

      $\langle p_1,q_1 \rangle \equiv \langle p_2, q_2 \rangle$, если $p_1q_2 = p_2q_1$\pause

\vspace{0.1cm}
      $\mathbb{Q} = Q/_\equiv$

\item Вещественные ($\mathbb{R}$). \pause $X = \{ A, B \}$, где $A,B \subseteq \mathbb{Q}$ --- дедекиндово сечение, если:\pause
\begin{enumerate}
\item $A\cup B = \mathbb{Q}$\pause
\item Если $a \in A$, $x \in \mathbb{Q}$ и $x \le a$, то $x \in A$\pause
\item Если $b \in B$, $x \in \mathbb{Q}$ и $b \le x$, то $x \in B$\pause
\item $A$ не содержит наибольшего.\pause
\end{enumerate}

       $\mathbb{R}$ --- множество всех возможных дедекиндовых сечений. \pause

$\sqrt 2 = \{\{ x\in\mathbb{Q}\ |\ x^2 < 2 \}, \{ x\in\mathbb{Q}\ |\ x^2 > 2\}\}$
\end{enumerate}
\end{frame}

\begin{frame}{Целые числа тоже попробуем определить}

 $$\mathbb{Z}: \dots -3, -2, -1, 0, 1, 2, 3, \dots$$\pause\vspace{-0.5cm}
\begin{itemize}
\item     $Z = \{\langle x, y \rangle\ |\ x,y\in \mathbb{N}_0\}$ \pause
\item Интуиция: $\langle x,y\rangle = x-y$\pause
\item $$\begin{array}{rcl}
      \langle a, b \rangle + \langle c, d \rangle & = & \langle a + c, b + d \rangle \\ \pause
      \langle a, b \rangle - \langle c, d \rangle & = & \langle a + d, b + c \rangle 
  \end{array}$$\pause
\item     Пусть $\langle a, b \rangle \equiv \langle c,d\rangle$, если $a + d = b + c$. Тогда $\mathbb{Z} = Z/_\equiv$\pause
\item      $0 = [\langle 0,0 \rangle],\; 1 = [\langle 1,0\rangle],\; -7 = [\langle 0,7 \rangle]$

\end{itemize}
\end{frame}

\begin{frame}{Натуральные числа: аксиоматика Пеано, 1889}\vspace{-0.5cm}
 $$\mathbb{N}: 1, 2, \dots \mbox{ или } \mathbb{N}_0: 0, 1, 2, \dots$$\vspace{-1cm}\pause
\begin{dfn}
  $N$ (или, более точно, $\langle N, 0, (')\rangle$) \emph{соответствует} аксиоматике Пеано, 
  если следующее определено/выполнено:\pause
  \begin{enumerate}
     \item Операция <<штрих>> $('): N \to N$, причём нет $a,b \in N$, что $a \ne b$, но $a' = b'$.\pause
           
           Если $x = y'$, то $x$ назовём следующим за $y$, а $y$ --- предшествующим $x$.\pause
     \item Константа $0 \in N$: нет $x \in N$, что $x' = 0$.\pause
     \item Индукция. Каково бы ни было свойство (<<предикат>>) $P: N \to V$, если:
           \begin{enumerate}
           \item $P(0)$
           \item При любом $x\in N$ из $P(x)$ следует $P(x')$
           \end{enumerate}
           то при любом $x \in N$ выполнено $P(x)$.
  \end{enumerate}
\end{dfn}\pause
Как построить? Например, в стиле алгебры Линденбаума:\pause
\begin{enumerate}
\item $N$ --- язык, порождённый грамматикой $\nu ::= \texttt{0}\ |\ \nu \texttt{<<'>>}$\pause
\item $0$ --- это $\texttt{<<0>>}$, $x'$ --- это $x \doubleplus \texttt{<<'>>}$
\end{enumerate}
\end{frame}


\begin{frame}{Примеры: что не соответствует аксиомам Пеано}
\begin{enumerate}
\item $\mathbb{Z}$, где $x' = x^2$\\\pause

Функция <<штрих>> не инъективна: $-3^2 = 3^2 = 9$\pause

\item Кольцо вычетов $\mathbb{Z}/{7\mathbb{Z}}$, где $x' = x+1$\\\pause

$6' = 0$, что нарушает свойства $0$\pause

\item $\mathbb{R^+}\cup\{0\}$, где $x' = x+1$\\\pause

пусть $P(x)$ означает <<$x \in \mathbb{Z}$>>:\pause \begin{enumerate}
\item $P(0)$ выполнено: $0 \in \mathbb{Z}$.\pause
\item Если $P(x)$, то есть $x \in \mathbb{Z}$, то и $x+1 \in \mathbb{Z}$ --- так
что и $P(x')$ выполнено.\pause
\end{enumerate}
Однако $P(0.5)$ ложно.
\end{enumerate}
\end{frame}

\begin{frame}{Пример доказательства}
\begin{thm}0 единственен: если $t$ таков, что при любом $y$ 
выполнено $y' \ne t$, то $t = 0$.
\end{thm}\pause
\begin{proof}

\begin{itemize}
\item Определим $P(x)$ как <<либо $x = 0$, либо $x = y'$ для некоторого $y \in N$>>.\pause
\begin{enumerate}
\item $P(0)$ выполнено, так как $0 = 0$.\pause
\item Если $P(x)$ выполнено, то возьмём $x$ в качестве $y$: тогда для $P(x')$
будет выполнено $x' = y'$.\pause
\end{enumerate}
Значит, $P(x)$ для любого $x \in N$.\pause

\item Рассмотрим $P(t)$: <<либо $t = 0$, либо $t = y'$ для некоторого $y \in N$>>.
Но так как такого $y$ нет, то неизбежно $t = 0$.
\end{itemize}
\end{proof}
\end{frame}

\begin{frame}{Обозначения и определения}
\begin{dfn}
$1 = 0'$, $2 = 0''$, $3 = 0'''$, $4 = 0''''$, $5 = 0'''''$, $6 = 0''''''$,
$7 = 0'''''''$, $8 = 0''''''''$, $9 = 0'''''''''$
\end{dfn}\pause
\begin{dfn}\vspace{-0.3cm}
$$a + b = \left\{ \begin{array}{ll} a, & \mbox{если } b = 0\\
                                    (a + c)', & \mbox{если } b = c'
                  \end{array}\right.$$
\end{dfn}\pause\vspace{-0.3cm}
Например, $$2 + 2 = 0'' + 0'' = \pause (0'' + 0')' = \pause ((0'' + 0)')' = \pause ((0'')')' = 0'''' = 4$$\pause\vspace{-0.3cm}
\begin{dfn}\vspace{-0.3cm}
$$a \cdot b = \left\{ \begin{array}{ll} 0, & \mbox{если } b = 0\\
                                    a \cdot c + a, & \mbox{если } b = c'
                  \end{array}\right.$$
\end{dfn}
%\pause
%\begin{dfn}
%$$a^b = \left\{ \begin{array}{ll} 1, & \mbox{если } b = 0\\
%                                    a^c \cdot a, & \mbox{если } b = c'
%                  \end{array}\right.$$
%\end{dfn}
\end{frame}

\begin{frame}{Пример: коммутативность сложения (лемма 1)}

\begin{multicols}{2}
\begin{lmm}[1]
$a + 0 = 0 + a$
\end{lmm} \pause
{\color{gray}
$$a + b = \left\{ \begin{array}{ll} a, & \mbox{если } b = 0\\
                                    (a + c)', & \mbox{если } b = c'
                  \end{array}\right.$$} \end{multicols}\pause
\vspace{-1.5cm}\begin{proof} Пусть $P(x)$ --- это $x + 0 = 0 + x$.
\begin{enumerate}\pause
\item Покажем $P(0)$. $0 + 0 = 0 + 0$ \pause
\item Покажем, что если $P(x)$, то $P(x')$. Покажем $P(x')$, то есть $x' + 0 = \dots$ \pause

\begin{center}
  \begin{tabular}{lrl} %Равенство & обоснование \\\hline
                      $\dots = x'$ & $a=x',b=0$: & $x' + 0 \Rightarrow x'$ \\\pause
                      $\dots = (x)'$ & \\ \pause
                      $\dots = (x + 0)'$ & $a=x,b=0$: &$(x + 0) \Leftarrow (x)$ \\ \pause
                      $\dots = (0 + x)'$ & $P(x)$: &$(x + 0) \Rightarrow (0 + x)$ \\ \pause
                      $\dots = 0 + x'$ & $a=0,b=x'$: &$0 + x' \Leftarrow (0 + x)'$
   \end{tabular}
\end{center}
\end{enumerate}\pause
Значит, $P(a)$ выполнено для любого $a \in N$.
\end{proof}
\end{frame}

\begin{frame}{Пример: коммутативность сложения (завершение)}
\begin{lmm}[2]
$a + b' = a' + b$
\end{lmm}\pause
\begin{proof} $P(x)$ --- это $a + x' = a' + x$\pause
\begin{enumerate}
\item $a + 0' = (a + 0)' = (a)' = a' = a' + 0$\pause
\item Покажем, что $P(x')$ следует из $P(x)$: $a + x'' = (a + x')' = (a' + x)' = a' + x'$
\end{enumerate}
\end{proof}\pause

\begin{thm}
$a + b = b + a$
\end{thm}\pause
\begin{proof}[Доказательство индукцией по $b$: $P(x)$ --- это $a + x = x + a$]
\begin{enumerate}
\item $a + 0 = 0 + a$ (лемма 1)\pause
\item $a + x' = (a + x)' = (x + a)' = x + a' = x' + a$
\end{enumerate}
\end{proof}
\end{frame}

\begin{frame}{Уточнение исчисления предикатов}
\begin{itemize}
\item Пусть требуется доказывать утверждения про равенство. Введём $E(p,q)$ --- предикат <<равенство>>.\pause
\item Однако $\not\vdash E(p,q)\to E(q,p)$: если $D = \{0,1\}$ и $E(p,q) ::= (p>q)$,
то $\not\models E(p,q)\to E(q,p)$.\pause
\item Конечно, можем указывать $\forall p.\forall q.E(p,q)\to E(q,p) \vdash \varphi$.\pause
\item Но лучше добавим аксиому $\forall p.\forall q.E(p,q)\to E(q,p)$.\pause
\item Добавив необходимые аксиомы, получим \emph{теорию первого порядка}.
\end{itemize}
\end{frame}

\begin{frame}{Теория первого порядка}
\begin{dfn}
Теорией первого порядка назовём исчисление предикатов с дополнительными (<<нелогическими>>
или <<математическими>>):
\begin{itemize}
\item предикатными и функциональными символами;
\item аксиомами.
\end{itemize}

Сущности, взятые из исходного исчисления предикатов, назовём \emph{логическими}
\end{dfn}
\end{frame}

\begin{frame}{Порядок логики/теории}
\begin{tabular}{llll}
Порядок & Кванторы & Формализует суждения\dots & Пример\\\hline
нулевой & запрещены & об отдельных значениях & И.В.\\
первый & по предметным переменным & о множествах & И.П.\\
%    &   & $S = \{ t\ |\ \psi[x := t] \}$ \\
    &   \multicolumn{2}{l}{\color{olive}$\{2,3,5,7,\dots\} = \{ t\ |\ \forall p.\forall q.(p \ne 1 \with q \ne 1) \rightarrow (t \ne p\cdot q)\}$}\\
второй & по предикатным переменным & о множествах множеств & Типы\\
    &   \multicolumn{2}{l}{\color{olive}$S = \{ \{t\ |\ P(t)\}\ |\ \varphi[p := P] \}$}\\
 & \dots 
\end{tabular}
\pause\vspace{0.3cm}

\begin{exm}[логики 2 порядка]\upshape
\begin{tabular}{ll}
$\alpha\rightarrow\beta\rightarrow\alpha$ (сх. акс. 1) & $\forall a.\forall b.a \rightarrow b \rightarrow a$ \vspace{0.1cm}\\
\texttt{let rec map f l = match l with} & $map: \forall a.\forall b.(a \rightarrow b) \rightarrow a\texttt{ list} \rightarrow b\texttt{ list}$ \\
\texttt{| [] -> []} \\
\texttt{| l1::ls -> f l1 :: map f l1}\vspace{0.1cm}\\
\texttt{map ((+) 1) [1;2;3] = [2;3;4]}
\end{tabular}
\end{exm}

\end{frame}

\begin{frame}{Формальная арифметика}
\begin{dfn}
Формальная арифметика --- теория первого порядка, со следующими добавленными нелогическими \dots
\begin{itemize}
\item двухместными функциональными символами $(+)$, $(\cdot)$; одноместным функциональным символом $(')$, 
нульместным функциональным символом $0$;\pause
\item двухместным предикатным символом $(=)$;\pause
\item восемью нелогическими \emph{аксиомами}:\vspace{0.1cm}
\begin{tabular}{ll}
(A1) $a=b \to a=c \to b=c$             &(A5) $a+0 = a$                     \\
(A2) $a=b \to a'=b'$                   &(A6) $a+b' = (a+b)'$               \\
(A3) $a'=b' \to a=b$                   &(A7) $a\cdot 0 = 0$                \\
(A4) $\neg a' = 0$                     &(A8) $a\cdot b' = a \cdot b + a$
\end{tabular}\pause
\item нелогической схемой аксиом индукции $\psi[x:=0]\with(\forall x.\psi\to \psi[x:=x'])\to \psi$ с метапеременными $x$ и $\psi$.
\end{itemize}
\end{dfn}
\end{frame}

\begin{frame}{Докажем, что $a=a$}
\small
Пусть $\top ::= 0=0\to 0=0 \to 0=0$, тогда:\pause

\begin{tabular}{lll}
(1) & $a=b\to a=c \to b=c$ & (Акс. А1)\\
(2) & $(a=b\to a=c \to b=c) \to \top \to (a=b\to a=c \to b=c)$ & (Сх. акс. 1)\\
(3) & $\top \to (a=b\to a=c \to b=c)$ & (M.P. 1, 2)\\
(4) & $\top \to (\forall c.a = b\to a = c \to b = c)$ & (Введ. $\forall$)\\\pause
(5) & $\top \to (\forall b.\forall c.a = b\to a = c \to b = c)$ & (Введ. $\forall$)\\
(6) & $\top \to (\forall a.\forall b.\forall c.a = b\to a = c \to b = c)$ & (Введ. $\forall$)\\\pause
(7) & $\top$ & (Сх. акс 1)\\
(8) & $(\forall a.\forall b.\forall c.a = b\to a = c \to b = c)$ & (M.P. 7, 6)\\\pause
(9) & $(\forall a.\forall b.\forall c.a = b\to a = c \to b = c) \to $\\
    & $\to (\forall b.\forall c.a+0 = b\to a+0 = c \to b = c)$ & (Сх. акс. 11)\\\pause
(10) & $\forall b.\forall c.a+0 = b\to a+0 = c \to b = c$ & (M.P. 8, 9)\\\pause
(12) & $\forall c.a+0 = a\to a+0 = c \to a = c$ & (M.P. 10, 11)\\\pause
(14) & $a+0 = a\to a+0 = a \to a = a$ & (M.P. 12, 13)\\\pause
(15) & $a+0 = a$ & (Акс. А5)\\
(16) & $a+0 = a \to a = a$ & (M.P. 15, 14)\\
(17) & $a = a$ & (M.P. 15, 16)
\end{tabular}
\end{frame}

\end{document}