|
|
@@ -74,6 +74,7 @@ $\OLmult$~(умножить на), $'$~(следующее за).
|
|
|
Формальные символы образуют первую категорию формальных объектов. Исходя из них,
|
|
|
мы получаем вторую категорию путём построения конечных последовательностей
|
|
|
вхождений формальных символов. Эти последовательности мы будем называть
|
|
|
+\itemlabel{def:p16-formal_expression}{def:p16-formal_expression}%
|
|
|
\emph{формальными выражениями}. Употреблённое только что слово <<вхождение>>
|
|
|
означает, что члены последовательности рассматриваются именно в качестве членов,
|
|
|
т.~е. подчёркивает то обстоятельство, что различные члены могут быть одним и тем
|
|
|
@@ -884,6 +885,11 @@ f(z)=\lim_{x\to 0} f(x,z)\text{,}
|
|
|
|
|
|
\section{Правила преобразования}
|
|
|
\label{sec:19-transformation_rules}
|
|
|
+%
|
|
|
+% TODO: отсюда и далее стоило бы выработать некоторую гибкую систему переноса
|
|
|
+% формул, не уместившихся в строку. Текущее разбиение слишком жёсткое и
|
|
|
+% сохранится даже при достаточном увеличении ширины страницы.
|
|
|
+%
|
|
|
|
|
|
В этом параграфе мы введём дальнейшие метаматематические определения (называемые
|
|
|
\emph{дедуктивными правилами}, или \emph{правилами преобразования}), которые
|
|
|
@@ -913,7 +919,507 @@ $\infr{B}$~есть~${\neg\frml{a}'=0}$‚ получаем
|
|
|
\frac{\infr{A},\infr{A}\OLimpl\infr{B}}{\infr{B}}\text{.}
|
|
|
\end{equation*}
|
|
|
|
|
|
-stub
|
|
|
+%% ======================= Страница 77 =======================
|
|
|
+
|
|
|
+Это~---~схема, содержащая три метаматематических выражения~<<$\infr{A}$>>,
|
|
|
+<<${\infr{A}\OLimpl\infr{B}}$>> и <<$\infr{B}$>>, которые представляют формулы,
|
|
|
+коль скоро выбраны формулы, представленные метаматематическими
|
|
|
+буквами~<<$\infr{A}$>>~и~<<$\infr{B}$>>. Смысл этого правила состоит в том, что
|
|
|
+формула, представленная выражением, написанным под чертой, может быть
|
|
|
+,,выведена`` из двух формул, представленных двумя выражениями, написанными над
|
|
|
+чертой. Например, если в качестве~$\infr{A}$ взята формула~${\neg\frml{a}'=0}$,
|
|
|
+а в качестве~$\infr{B}$~---~формула~${\frml{a}'=0\vee\neg\frml{a}'=0}$, то наше
|
|
|
+правило позволяет из
|
|
|
+${\neg\frml{a}'=0}$~и~${\neg\frml{a}'=0\OLimpl\frml{a}'=0\vee\neg\frml{a}'=0}$
|
|
|
+вывести~${\frml{a}'=0\vee\neg\frml{a}'=0}$. Так как
|
|
|
+${\neg\frml{a}'=0}$~и~${\neg\frml{a}'=0\OLimpl\frml{a}'=0\vee\neg\frml{a}'=0}$
|
|
|
+являются (как мы уже видели) аксиомами, то
|
|
|
+${\frml{a}'=0\vee\neg\frml{a}'=0}$~будет дальнейшей ,,формальной теоремой``. (По
|
|
|
+нашей терминологии аксиомы включаются в число теорем.)
|
|
|
+
|
|
|
+Мы рассмотрим теперь полный перечень постулатов, а затем дадим определения,
|
|
|
+устанавливающие дедуктивную структуру формальной системы с помощью ссылок на
|
|
|
+этот перечень. Читатель убедится в том, что в результате этого ряда определений
|
|
|
+будет определён подкласс формул, называемый классом ,,доказуемых формул`` или
|
|
|
+,,формальных теорем``.\medskip
|
|
|
+
|
|
|
+\centerline{\textsc{Постулаты формальной системы}}
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Dramatis\kern1ex personae\textup{\footnote{Действующие
|
|
|
+лица~(лат.).~---~\textit{Прим.~перев.}}}.}%
|
|
|
+{sspar:p19-dramatis_personae}{\textsc{Dramatis personae}}
|
|
|
+В постулатах~\ref{postulate:p19-1}--\ref{postulate:p19-8}
|
|
|
+$\infr{A}$,~$\infr{B}$~и~$\infr{C}$~---~формулы. В
|
|
|
+постулатах~\ref{postulate:p19-9}--\ref{postulate:p19-13}
|
|
|
+$\infr{x}$~---~переменная, ${\infr{A}(\infr{x})}$~---~формула,
|
|
|
+$\infr{C}$~---~формула‚ не содержащая свободно~$\infr{x}$, а
|
|
|
+$\infr{t}$~---~терм, свободный для~$\infr{x}$ в~${\infr{A}(\infr{x})}$.
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Группа\kern1exA.}{ssspar:p19-group-A}{ssspar:p19-group-A}
|
|
|
+Постулаты исчисления предикатов.
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Группа\kern1exA1.}%
|
|
|
+{sssspar:p19-group-A1}{sssspar:p19-group-A1}
|
|
|
+Постулаты исчисления высказываний.\par\nopagebreak\medskip\nopagebreak%
|
|
|
+%%
|
|
|
+%% Замечание: может показаться странным решение выделить под разделитель
|
|
|
+%% отдельный столбец таблицы. И это странно, так как более очевидное решение -
|
|
|
+%% - определить разделитель между столбцами в один-экс-керн, НО
|
|
|
+%% по неясной причине введение такого разделителя сдвигает якоря ссылок на одну
|
|
|
+%% строку вниз. Полагаю это какая-то особенность окружения tabular.
|
|
|
+%%
|
|
|
+{\SetLenVarWithWidth{\colAw}{77.}%
|
|
|
+\SetLenVarWithWidth{\kernLen}{\kern1ex}%
|
|
|
+\SetLenVarWithVal{\colBw}{0.5\linewidth-\colAw-\kernLen}%
|
|
|
+\SetLenVarWithWidth{\tempLongestLen}{${\left(\infr{A}\OLimpl\infr{B}\right)\OLimpl\left(
|
|
|
+ \left(\infr{A}\OLimpl\left(\infr{B}\OLimpl\infr{C}\right)\right)
|
|
|
+ \OLimpl\left(\infr{A}\OLimpl\infr{C}\right)
|
|
|
+\right)}$.\kern5ex}%
|
|
|
+\ifthenelse{\lengthtest{\tempLongestLen <\colBw}}
|
|
|
+ {\SetLenVarWithVal{\colOneBw}{\colBw}}%
|
|
|
+ {\SetLenVarWithVal{\colOneBw}{\tempLongestLen}}%
|
|
|
+\SetLenVarWithVal{\colOneDw}{\linewidth-2\colAw-2\kernLen-\colOneBw}%
|
|
|
+\noindent\setlength{\tabcolsep}{0pt}%
|
|
|
+\begin{tabular}{p{\colAw}p{\kernLen}p{\colOneBw}>{\hfill}p{\colAw}p{\kernLen}p{\colOneDw}}
|
|
|
+1a.\itemlabel{postulate:p19-1}{1}\itemlabel{postulate:p19-1a}{1a}&&
|
|
|
+${\infr{A}\OLimpl\left(\infr{B}\OLimpl\infr{A}\right)}$.&
|
|
|
+\multirow{2}{*}{2.\itemlabel{postulate:p19-2}{2}}&&
|
|
|
+\multirow{2}{*}{${\displaystyle{\frac{\infr{A},\infr{A}\OLimpl%
|
|
|
+\infr{B}}{\infr{B}}}}$.}\\
|
|
|
+1b.\itemlabel{postulate:p19-1b}{1b}&&
|
|
|
+${\left(\infr{A}\OLimpl\infr{B}\right)\OLimpl\left(
|
|
|
+ \left(\infr{A}\OLimpl\left(\infr{B}\OLimpl\infr{C}\right)\right)
|
|
|
+ \OLimpl\left(\infr{A}\OLimpl\infr{C}\right)
|
|
|
+\right)}$.&&&
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+\multirow{2}{*}{3.\itemlabel{postulate:p19-3}{3}}&&
|
|
|
+\multirow{2}{*}{${\infr{A}\OLimpl%
|
|
|
+\left(\infr{B}\OLimpl\infr{A}\OLand\infr{B}\right)}$.}&
|
|
|
+4a.\itemlabel{postulate:p19-4a}{postulate:p19-4a}&&
|
|
|
+${\infr{A}\OLand\infr{B}\OLimpl\infr{A}}$.\\
|
|
|
+&&&4b.\itemlabel{postulate:p19-4b}{postulate:p19-4b}&&
|
|
|
+${\infr{A}\OLand\infr{B}\OLimpl\infr{B}}$.
|
|
|
+\end{tabular}%
|
|
|
+\SetLenVarWithWidth{\tempLongestLen}{${\left(\infr{A}\OLimpl%
|
|
|
+\infr{C}\right)\OLimpl
|
|
|
+\left(
|
|
|
+ \left(\infr{B}\OLimpl\infr{C}\right)\OLimpl
|
|
|
+ \left(\infr{A}\vee\infr{B}\OLimpl\infr{C}\right)
|
|
|
+\right)
|
|
|
+}$.}%
|
|
|
+\ifthenelse{\lengthtest{\tempLongestLen<\colBw}}%
|
|
|
+ {\SetLenVarWithVal{\colThreeDw}{\colBw}}%
|
|
|
+ {\SetLenVarWithVal{\colThreeDw}{\tempLongestLen}}%
|
|
|
+\SetLenVarWithVal{\colThreeBw}{\linewidth-2\colAw-2\kernLen-\colThreeDw}%
|
|
|
+\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{p{\colAw}p{\kernLen}p{\colThreeBw}>{\hfill}p{\colAw}p{\kernLen}p{\colThreeDw}}
|
|
|
+5a.\itemlabel{postulate:p19-5a}{postulate:p19-5a}&&
|
|
|
+${\infr{A}}\OLimpl\infr{A}\vee\infr{B}$.&
|
|
|
+\multirow{2}{*}{6.\itemlabel{postulate:p19-6}{postulate:p19-6}}&&
|
|
|
+\multirow{2}{*}{${\left(\infr{A}\OLimpl\infr{C}\right)\OLimpl
|
|
|
+\left(
|
|
|
+ \left(\infr{B}\OLimpl\infr{C}\right)\OLimpl
|
|
|
+ \left(\infr{A}\vee\infr{B}\OLimpl\infr{C}\right)
|
|
|
+\right)
|
|
|
+}$.}\\
|
|
|
+5b.\itemlabel{postulate:p19-5b}{postulate:p19-5b}&&
|
|
|
+${\infr{B}\OLimpl\infr{A}\vee\infr{B}}$.&&&
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+7.\itemlabel{postulate:p19-7}{postulate:p19-7}&&
|
|
|
+${\left(\infr{A}\OLimpl\infr{B}\right)\OLimpl
|
|
|
+\left(\left(\infr{A}\OLimpl\neg\infr{B}\right)\OLimpl\neg\infr{A}\right)}$.&
|
|
|
+8\textdegree.\itemlabel{postulate:p19-8}{8}&&
|
|
|
+${\neg\neg\infr{A}\OLimpl\infr{A}}$.
|
|
|
+\end{tabular}}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Группа\kern1exA2.}%
|
|
|
+{sssspar:p19-group-A2}{sssspar:p19-group-A2}
|
|
|
+(Дополнительные) Постулаты исчисления предикатов.%
|
|
|
+\par\nopagebreak\medskip\nopagebreak%
|
|
|
+{\SetLenVarWithWidth{\colAw}{77.}%
|
|
|
+\SetLenVarWithWidth{\kernLen}{\kern1ex}%
|
|
|
+\SetLenVarWithVal{\colBw}{0.5\linewidth-\colAw-\kernLen}%
|
|
|
+\noindent\setlength{\tabcolsep}{0pt}%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+9.\itemlabel{postulate:p19-9}{9}&&
|
|
|
+${\displaystyle{\frac{\infr{C}\OLimpl\infr{A}(\infr{x})}%
|
|
|
+{\infr{C}\OLimpl\forall\infr{x}\infr{A}(\infr{x})}}}$.&
|
|
|
+10.\itemlabel{postulate:p19-10}{10}&&
|
|
|
+${\forall\infr{x}\infr{A}(\infr{x})\OLimpl\infr{A}(\infr{t})}$.
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+11.\itemlabel{postulate:p19-11}{11}&&
|
|
|
+${\infr{A}(\infr{t})\OLimpl\exists\infr{x}\infr{A}(\infr{x})}$.&
|
|
|
+12.\itemlabel{postulate:p19-12}{12}&&
|
|
|
+${\displaystyle{\frac{\infr{A}(\infr{x})\OLimpl\infr{C}}%
|
|
|
+{\exists\infr{x}\infr{A}(\infr{x})\OLimpl\infr{C}}}}$.
|
|
|
+\end{tabular}}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Группа\kern1exB.}{ssspar:p19-group-B}{ssspar:p19-group-B}
|
|
|
+(Дополнительные) Постулаты арифметики.%
|
|
|
+\par\nopagebreak\medskip\nopagebreak%
|
|
|
+{\SetLenVarWithWidth{\colAw}{77.}%
|
|
|
+\SetLenVarWithWidth{\kernLen}{\kern1ex}%
|
|
|
+\SetLenVarWithVal{\colBw}{0.5\linewidth-\colAw-\kernLen}%
|
|
|
+\noindent\setlength{\tabcolsep}{0pt}%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}l}
|
|
|
+13.\itemlabel{postulate:p19-13}{13}&&
|
|
|
+${\infr{A}(0)\OLand
|
|
|
+\forall\infr{x}\left(\infr{A}(\infr{x})\OLimpl\infr{A}(\infr{x}')\right)\OLimpl
|
|
|
+\infr{A}(\infr{x})}$.
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+14.\itemlabel{postulate:p19-14}{14}&&
|
|
|
+${\frml{a}'=\frml{b}'\OLimpl\frml{a}=\frml{b}}$.&
|
|
|
+15.\itemlabel{postulate:p19-15}{postulate:p19-15}&&
|
|
|
+${\neg\frml{a}'=0}$.
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+16.\itemlabel{postulate:p19-16}{16}&&
|
|
|
+${\frml{a}=\frml{b}\OLimpl\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)}$.&
|
|
|
+17.\itemlabel{postulate:p19-17}{postulate:p19-17}&&
|
|
|
+${\frml{a}=\frml{b}\OLimpl\frml{a}'=\frml{b}'}$.
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+18.\itemlabel{postulate:p19-18}{18}&&
|
|
|
+${\frml{a}+0=\frml{a}}$.&
|
|
|
+19.\itemlabel{postulate:p19-19}{postulate:p19-19}&&
|
|
|
+${\frml{a}+\frml{b}'=\left(\frml{a}+\frml{b}\right)'}$.
|
|
|
+\end{tabular}\par\nopagebreak\medskip\nopagebreak\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+20.\itemlabel{postulate:p19-20}{postulate:p19-20}&&
|
|
|
+${\frml{a}\OLmult 0=0}$.&
|
|
|
+21.\itemlabel{postulate:p19-21}{21}&&
|
|
|
+${\frml{a}\OLmult\frml{b}'=\frml{a}\OLmult\frml{b}+\frml{a}}$.
|
|
|
+\end{tabular}}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+\noindent%
|
|
|
+(Причина, по которой при постулате~\ref{postulate:p19-8} поставлен
|
|
|
+<<\textdegree>>, будет выяснена
|
|
|
+в~\textsection~\ref{sec:23-introduction_and_elimination_of_logical_symbols}.)
|
|
|
+
|
|
|
+%% ======================= Страница 78 =======================
|
|
|
+
|
|
|
+Легко проверить, что \ref{postulate:p19-14}--\ref{postulate:p19-21}~являются
|
|
|
+формулами и что~\ref{postulate:p19-1}--\ref{postulate:p19-13}~(или в
|
|
|
+случаях~\ref{postulate:p19-2},~\ref{postulate:p19-9}~и~\ref{postulate:p19-12}
|
|
|
+выражения\footnote{Термин <<выражение>> означает здесь <<формальное выражение>>
|
|
|
+в смысле стр.~\pageref{def:p16-formal_expression}, и так как запятая не является
|
|
|
+формальным символом, то <<${\infr{A},\infr{A}\OLimpl\infr{B}}$>>~ни при каком
|
|
|
+выборе формул для букв~$\infr{A}$~и~$\infr{B}$ не является выражением; значит
|
|
|
+оборот <<выражение, стоящее в~\ref{postulate:p19-2} над чертой>> может
|
|
|
+относиться только к~$\infr{A}$~и~${\infr{A}\OLimpl\infr{B}}$ (молчаливо
|
|
|
+предполагается, что этот оборот не относится к другим частям только что
|
|
|
+названных выражений).~---~\textit{Прим.~перев.}}, стоящие над и под чертой,
|
|
|
+являются формулами для каждого выбора~$\infr{A}$,~$\infr{B}$,~$\infr{C}$,
|
|
|
+или~$\infr{x}$,~${\infr{A}(\infr{x})}$,~$\infr{C}$,~$\infr{t}$, подчинённого
|
|
|
+условиям, приведённым в~\ref{sspar:p19-dramatis_personae}.
|
|
|
+%%
|
|
|
+%% исправление
|
|
|
+%% восстановлено примечание, в оригинале оно пропущено
|
|
|
+%%
|
|
|
+
|
|
|
+Класс ,,аксиом`` определяется следующим образом. Формула является
|
|
|
+\emph{аксиомой}, если она имеет одну из форм~\ref{postulate:p19-1a},%
|
|
|
+~\ref{postulate:p19-1b},~\ref{postulate:p19-3}--\ref{postulate:p19-8},%
|
|
|
+~\ref{postulate:p19-10},~\ref{postulate:p19-11},~\ref{postulate:p19-13} или
|
|
|
+если она есть одна из формул~\ref{postulate:p19-14}--\ref{postulate:p19-21}.
|
|
|
+
|
|
|
+Отношение ,,непосредственного следования`` определяется следующим образом.
|
|
|
+Формула является \emph{непосредственным следствием} (из) одной или двух других
|
|
|
+формул, если она имеет форму, указанную под чертой, тогда как другая(ие)
|
|
|
+имеет(ют) форму(ы), указанную(ые) над чертой
|
|
|
+в~\ref{postulate:p19-2},~\ref{postulate:p19-9}~или~\ref{postulate:p19-12}.
|
|
|
+
|
|
|
+Это~---~основное метаматематическое определение, соответствующее
|
|
|
+постулатам~\ref{postulate:p19-2},~\ref{postulate:p19-9}%
|
|
|
+~и~\ref{postulate:p19-12}, но мы сформулируем его ещё в расширенной
|
|
|
+терминологии, учитывающей процесс его применения.
|
|
|
+Постулаты~\ref{postulate:p19-2},~\ref{postulate:p19-9}%
|
|
|
+~и~\ref{postulate:p19-12} мы называем \emph{правилами вывода}. Для любого
|
|
|
+(фиксированного) выбора~$\infr{A}$~и~$\infr{B}$~или~$\infr{x}$,%
|
|
|
+~${\infr{A}(\infr{x})}$~и~$\infr{C}$, подчинённого отмеченным выше условиям,
|
|
|
+формула(ы), указанная(ые) над чертой, является \emph{посылкой} (являются
|
|
|
+\emph{первой} и \emph{второй посылкой} соответственно), а формула, указанная под
|
|
|
+чертой, является \emph{заключением} (для) \emph{применения} правила (или
|
|
|
+(\emph{формального}) \emph{вывода} по этому правилу). Заключение является
|
|
|
+\emph{непосредственным следствием} из посылки (посылок) (по рассматриваемому
|
|
|
+правилу).
|
|
|
+
|
|
|
+Карнап~\cite{carnap1934} объединяет оба рода постулатов под общим названием
|
|
|
+,,правил преобразования``, рассматривая аксиомы как результат преобразования с
|
|
|
+числом посылок, равным нулю.
|
|
|
+
|
|
|
+Определение ,,(формально) доказуемой формулы`` или ,,(формальной) теоремы``
|
|
|
+может быть теперь дано индуктивно следующим образом:
|
|
|
+
|
|
|
+1.\itemlabel{listItem:p19-list1-1}{1}~Если $\infr{D}$~---~аксиома, то
|
|
|
+$\infr{D}$~\emph{доказуема}.
|
|
|
+2.\itemlabel{listItem:p19-list1-2}{listItem:p19-list1-2}~Если
|
|
|
+$\infr{E}$~\emph{доказуема}, а $\infr{D}$~---~непосредственное следствие
|
|
|
+из~$\infr{E}$, то $\infr{D}$~\emph{доказуема}.
|
|
|
+3.\itemlabel{listItem:p19-list1-3}{3}~Если
|
|
|
+$\infr{E}$~и~$\infr{F}$~\emph{доказуемы}, а $\infr{D}$~---~непосредственное
|
|
|
+следствие из~$\infr{E}$~и~$\infr{F}$, то $\infr{D}$~\emph{доказуема}.
|
|
|
+4.\itemlabel{listItem:p19-list1-4}{listItem:p19-list1-4}~Формула является
|
|
|
+\emph{доказуемой} только в
|
|
|
+силу~\ref{listItem:p19-list1-1}--\ref{listItem:p19-list1-3}.
|
|
|
+
|
|
|
+Это понятие может быть получено также с помощью промежуточной концепции
|
|
|
+,,формального доказательства`` следующим образом. (\emph{Формальное})
|
|
|
+\emph{доказательство} есть (непустая) конечная последовательность (вхождений)
|
|
|
+формул такая, что каждая формула этой последовательности является или аксиомой
|
|
|
+или непосредственным следствием из предыдущих формул последовательности.
|
|
|
+Доказательство называется доказательством \emph{своей последней формулы}, и эта
|
|
|
+формула называется (\emph{формально}) \emph{доказуемой}, или (\emph{формальной})
|
|
|
+\emph{теоремой}.
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p19-1}{exmpl:p19-1}
|
|
|
+Приведённая ниже последовательность из 17 формул является доказательством
|
|
|
+формулы~${\frml{a}=\frml{a}}$. Формула~\ref{formulaeList:p19-list0-1} есть
|
|
|
+аксиома~\ref{postulate:p19-16}. Формула~\ref{formulaeList:p19-list0-2} есть аксиома в
|
|
|
+силу применения схемы аксиомы~\ref{postulate:p19-1a}, при котором
|
|
|
+$\infr{A}$~и~$\infr{B}$~схемы оба являются ${0=0}$; а
|
|
|
+формула~\ref{formulaeList:p19-list0-3}~---~в силу применения, при котором
|
|
|
+$\infr{A}$~есть~${\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)}$ и $\infr{B}$~есть~%
|
|
|
+${0=0\OLimpl\left(0=0\OLimpl 0=0\right)}$.
|
|
|
+Формула~\ref{formulaeList:p19-list0-4} есть непосредственное следствие из
|
|
|
+формул~\ref{formulaeList:p19-list0-1}~и~\ref{formulaeList:p19-list0-3} как
|
|
|
+первой и второй посылки соответственно, в силу применения
|
|
|
+правила~\ref{postulate:p19-2}, при котором
|
|
|
+$\infr{A}$~есть~${\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{b}\OLimpl\frml{b}=\frml{c}\right)}$‚ а $\infr{B}$~есть~%
|
|
|
+${\left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl%
|
|
|
+\left[\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$. Фор%
|
|
|
+%% ======================= Страница 79 =======================
|
|
|
+мула~\ref{formulaeList:p19-list0-5} есть непосредственное следствие из
|
|
|
+формулы~\ref{formulaeList:p19-list0-4} в силу применения
|
|
|
+правила~\ref{postulate:p19-9}
|
|
|
+(причем $\infr{x}$~есть~$\frml{c}$),
|
|
|
+${\infr{A}(\infr{x})}$~есть~${\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)}$, а
|
|
|
+$\infr{C}$~есть~${0=0\OLimpl\left(0=0\OLimpl 0=0\right)}$ (заметим, что
|
|
|
+последняя формула не содержит свободно~$\infr{x}$).
|
|
|
+Формула~\ref{formulaeList:p19-list0-9} есть аксиома в силу применения схемы
|
|
|
+аксиом~\ref{postulate:p19-10}, при котором $\infr{x}$~есть~$\frml{a}$,
|
|
|
+${\infr{A}(\infr{x})}$~есть~%
|
|
|
+${\forall\frml{b}\forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$, а
|
|
|
+$\infr{t}$~есть терм~${\frml{a}+0}$ (который, заметим, свободен для~$\infr{x}$
|
|
|
+в~${\infr{A}(\infr{x})}$). ${\infr{A}(\infr{t})}$,~в силу нашего обозначения для
|
|
|
+подстановки~(\textsection~\ref{sec:18-free_and_bound_variables}), есть результат
|
|
|
+подстановки~$\infr{t}$ вместо (свободных вхождений)~$\infr{x}$
|
|
|
+в~${\infr{A}(\infr{x})}$, т.~е. в данном случае ${\infr{A}(\infr{t})}$~есть
|
|
|
+${\forall\frml{b}\forall\frml{c}%
|
|
|
+\left[\frml{a}+0=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$.
|
|
|
+
|
|
|
+{\SetLenVarWithWidth{\colAw}{17.}%
|
|
|
+\SetLenVarWithWidth{\kernLen}{\kern1ex}%
|
|
|
+\SetLenVarWithVal{\colBw}{\linewidth-\colAw-\kernLen}%
|
|
|
+\SetLenVarWithVal{\tabcolsep}{0em}%
|
|
|
+\SetLenVarWithVal{\tempShiftIndent}{\parindent}%
|
|
|
+\noindent%
|
|
|
+\begin{longtable}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+1.\itemlabel{formulaeList:p19-list0-1}{1}&&
|
|
|
+${\frml{a}=\frml{b}\OLimpl%
|
|
|
+\left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)}$%
|
|
|
+~---~аксиома~\ref{postulate:p19-16}.\\
|
|
|
+2.\itemlabel{formulaeList:p19-list0-2}{2}&&
|
|
|
+${0=0\OLimpl\left(0=0\OLimpl 0=0\right)}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-1a}.\\
|
|
|
+3.\itemlabel{formulaeList:p19-list0-3}{3}&&
|
|
|
+${\left\lbrace\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)
|
|
|
+\right\rbrace\OLimpl\left\lbrace
|
|
|
+ \left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl\right.
|
|
|
+ }$\newline\hspace*{\fill}${\left.\OLimpl
|
|
|
+ \left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]
|
|
|
+\right\rbrace}$%
|
|
|
+%%
|
|
|
+%% исправление
|
|
|
+%% удалена лишняя скобка, в оригинале было
|
|
|
+%% "[a=b=>(a=c)=>b=c)]}"
|
|
|
+%%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-1a}.\\
|
|
|
+4.\itemlabel{formulaeList:p19-list0-4}{4}&&
|
|
|
+${\left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-1},~\ref{formulaeList:p19-list0-3}.\\
|
|
|
+5.\itemlabel{formulaeList:p19-list0-5}{5}&&
|
|
|
+${\left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-9},~\ref{formulaeList:p19-list0-4}.\\
|
|
|
+6.\itemlabel{formulaeList:p19-list0-6}{6}&&
|
|
|
+${\left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \forall\frml{b}\forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-9},~\ref{formulaeList:p19-list0-5}.\\
|
|
|
+7.\itemlabel{formulaeList:p19-list0-7}{7}&&
|
|
|
+${\left[0=0\OLimpl\left(0=0\OLimpl 0=0\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \forall\frml{a}\forall\frml{b}\forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-9},~\ref{formulaeList:p19-list0-6}.\\
|
|
|
+8.\itemlabel{formulaeList:p19-list0-8}{8}&&
|
|
|
+${\forall\frml{a}\forall\frml{b}\forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-2},~\ref{formulaeList:p19-list0-7}.\\
|
|
|
+9.\itemlabel{formulaeList:p19-list0-9}{9}&&
|
|
|
+${\forall\frml{a}\forall\frml{b}\forall\frml{c}\left[\frml{a}=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \forall\frml{b}\forall\frml{c}\left[\frml{a}+0=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-10}.\\
|
|
|
+10.\itemlabel{formulaeList:p19-list0-10}{10}&&
|
|
|
+${\forall\frml{b}\forall\frml{c}\left[\frml{a}+0=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-8},~\ref{formulaeList:p19-list0-9}.\\
|
|
|
+11.\itemlabel{formulaeList:p19-list0-11}{11}&&
|
|
|
+${\forall\frml{b}\forall\frml{c}\left[\frml{a}+0=\frml{b}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{b}=\frml{c}\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \forall\frml{c}\left[\frml{a}+0=\frml{a}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{a}=\frml{c}\right)\right]}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-10}.\\
|
|
|
+12.\itemlabel{formulaeList:p19-list0-12}{12}&&
|
|
|
+${\forall\frml{c}\left[\frml{a}+0=\frml{a}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{a}=\frml{c}\right)\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-10},~\ref{formulaeList:p19-list0-11}.\\
|
|
|
+13.\itemlabel{formulaeList:p19-list0-13}{13}&&
|
|
|
+${\forall\frml{c}\left[\frml{a}+0=\frml{a}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{c}\OLimpl\frml{a}=\frml{c}\right)\right]\OLimpl
|
|
|
+ }$\newline\hspace*{\fill}${\OLimpl
|
|
|
+ \left[\frml{a}+0=\frml{a}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{a}\OLimpl\frml{a}=\frml{a}\right)\right]}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-10}.\\
|
|
|
+14.\itemlabel{formulaeList:p19-list0-14}{14}&&
|
|
|
+${\frml{a}+0=\frml{a}\OLimpl
|
|
|
+ \left(\frml{a}+0=\frml{a}\OLimpl\frml{a}=\frml{a}\right)}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-12},~\ref{formulaeList:p19-list0-13}.\\
|
|
|
+15.\itemlabel{formulaeList:p19-list0-15}{15}&&
|
|
|
+${\frml{a}+0=\frml{a}}$~---~аксиома~\ref{postulate:p19-18}.\\
|
|
|
+16.\itemlabel{formulaeList:p19-list0-16}{16}&&
|
|
|
+${\frml{a}+0=\frml{a}\OLimpl\frml{a}=\frml{a}}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-15},~\ref{formulaeList:p19-list0-14}.\\
|
|
|
+17.\itemlabel{formulaeList:p19-list0-17}{17}&&
|
|
|
+${\frml{a}=\frml{a}}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list0-15},~\ref{formulaeList:p19-list0-16}.
|
|
|
+\end{longtable}}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p19-2}{exmpl:p19-2}
|
|
|
+Пусть $\infr{A}$~---~любая формула. Тогда приведённая ниже последовательность из
|
|
|
+пяти формул является доказательством формулы~${\infr{A}\OLimpl\infr{A}}$.
|
|
|
+(Другими словами, то, что мы выпишем ниже, является ,,схемой доказательств``,
|
|
|
+которая превращается в конкретное доказательство при подстановке любой
|
|
|
+конкретной формулы, например~${0=0}$, вместо метаматематической
|
|
|
+буквы~<<$\infr{A}$>>, а последнее выражение~${\infr{A}\OLimpl\infr{A}}$ этой
|
|
|
+схемы является соответственно ,,схемой теорем``.)
|
|
|
+Формула~\ref{formulaeList:p19-list1-1} есть аксиома в силу применения схемы
|
|
|
+аксиом~\ref{postulate:p19-1a}, при котором в качестве
|
|
|
+букв~$\infr{A}$~и~$\infr{B}$ схемы берётся формула~$\infr{A}$ данного примера.
|
|
|
+Формула~\ref{formulaeList:p19-list1-2} есть аксиома в силу применения схемы
|
|
|
+аксиом~\ref{postulate:p19-1b}, при котором в качестве
|
|
|
+букв~$\infr{A}$~и~$\infr{C}$ схемы берётся формула~$\infr{A}$ этого примера, а в
|
|
|
+качестве~$\infr{B}$ схемы~---~${\infr{A}\OLimpl\infr{A}}$ данного примера.
|
|
|
+Формула~\ref{formulaeList:p19-list1-3} есть непосредственное следствие из
|
|
|
+формул~\ref{formulaeList:p19-list1-1}~и~~\ref{formulaeList:p19-list1-2} как
|
|
|
+первой и второй посылки соответственно в силу применения
|
|
|
+правила~\ref{postulate:p19-2}, при котором в качестве~$\infr{A}$ правила
|
|
|
+берётся~${\infr{A}\OLimpl\left(\infr{A}\OLimpl\infr{A}\right)}$ данного примера,
|
|
|
+а в качестве~$\infr{B}$ правила~---~${\left[\infr{A}\OLimpl
|
|
|
+ \left(\left(\infr{A}\OLimpl\infr{A}\right)\OLimpl\infr{A}\right)
|
|
|
+\right]\OLimpl\left[\infr{A}\OLimpl\infr{A}\right]}$ данного примера.
|
|
|
+\medskip
|
|
|
+
|
|
|
+{\SetLenVarWithVal{\tabcolsep}{0em}\noindent%
|
|
|
+\begin{tabular}{p{\widthof{(1)\kern1ex}}p{\linewidth-\widthof{(1)\kern1ex}}}
|
|
|
+(1)\itemlabel{formulaeList:p19-list1}{(1)}&
|
|
|
+{\SetLenVarWithWidth{\colAw}{17.}%
|
|
|
+\SetLenVarWithWidth{\kernLen}{\kern1ex}%
|
|
|
+\SetLenVarWithVal{\colBw}{\linewidth-\colAw-\kernLen}%
|
|
|
+\noindent%
|
|
|
+\begin{tabular}{>{\hfill}p{\colAw}p{\kernLen}p{\colBw}}
|
|
|
+1.\itemlabel{formulaeList:p19-list1-1}{1}&&
|
|
|
+${\infr{A}\OLimpl\left(\infr{A}\OLimpl\infr{A}\right)}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-1a}.\\
|
|
|
+2.\itemlabel{formulaeList:p19-list1-2}{2}&&
|
|
|
+${\left\lbrace
|
|
|
+ \infr{A}\OLimpl\left(\infr{A}\OLimpl\infr{A}\right)
|
|
|
+\right\rbrace\OLimpl
|
|
|
+}$\newline\hspace*{\fill}${\OLimpl
|
|
|
+\left\lbrace
|
|
|
+ \left[
|
|
|
+ \infr{A}\OLimpl
|
|
|
+ \left(\left(\infr{A}\OLimpl\infr{A}\right)\OLimpl\infr{A}\right)
|
|
|
+ \right]\OLimpl\left[\infr{A}\OLimpl\infr{A}\right]
|
|
|
+\right\rbrace}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-1b}.\\
|
|
|
+3.\itemlabel{formulaeList:p19-list1-3}{3}&&
|
|
|
+${\left[
|
|
|
+ \infr{A}\OLimpl
|
|
|
+ \left(\left(\infr{A}\OLimpl\infr{A}\right)\OLimpl\infr{A}\right)
|
|
|
+\right]\OLimpl\left[\infr{A}\OLimpl\infr{A}\right]}$%
|
|
|
+~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list1-1},~\ref{formulaeList:p19-list1-2}.\\
|
|
|
+4.\itemlabel{formulaeList:p19-list1-4}{4}&&
|
|
|
+${\infr{A}\OLimpl
|
|
|
+ \left(\left(\infr{A}\OLimpl\infr{A}\right)\OLimpl\infr{A}\right)}$%
|
|
|
+~---~схема аксиом~\ref{postulate:p19-1a}.\\
|
|
|
+5.\itemlabel{formulaeList:p19-list1-5}{5}&&
|
|
|
+${\infr{A}\OLimpl\infr{A}}$~---~правило~\ref{postulate:p19-2},%
|
|
|
+~\ref{formulaeList:p19-list1-4},~\ref{formulaeList:p19-list1-3}.\\
|
|
|
+\end{tabular}}%
|
|
|
+\end{tabular}}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+%% ======================= Страница 80 =======================
|
|
|
+
|
|
|
+Термины: \emph{доказательство}, \emph{теорема} и т.~п., определённые для
|
|
|
+формальной системы (т.~е. формальное доказательство, формальная теорема
|
|
|
+и~т.~п.), следует чётко отличать от этих терминов в их обычном содержательном
|
|
|
+смысле, которым мы пользуемся при изложении метаматематики. Формальная
|
|
|
+теорема~---~это формула (т.~е. определённого рода конечная последовательность
|
|
|
+знаков), и её формальное доказательство~---~это определённого рода конечная
|
|
|
+последовательность формул. А метаматематическая теорема~---~это осмысленное
|
|
|
+утверждение о формальных объектах, и её доказательство~---~это интуитивное
|
|
|
+обоснование истинности этого утверждения.
|
|
|
+
|
|
|
+Мы рассмотрели три категории формальных
|
|
|
+объектов~(\textsection~\ref{sec:16-formal_symbols}), но, если понадобится, мы
|
|
|
+будем вводить при их изучении и другие, коль скоро мы будем иметь дело с
|
|
|
+финитными методами. Помимо этого, несколько иное расширение нашего предмета
|
|
|
+изучения имеет место, когда мы переходим к исследованию вида метаматематических
|
|
|
+определений и теорем. Если бы мы пожелали при этом быть пунктуальными, то
|
|
|
+пришлось бы построить метаметаматематику. Однако такое положение дел является
|
|
|
+обычным в других областях неформальной математики, и мы будем рассматривать
|
|
|
+такие исследования как случайные объяснения, иногда помогающие быстро понять,
|
|
|
+что делается в метаматематике, а иногда позволяющие нам сократить формулировки
|
|
|
+метаматематических теорем, которые могли бы быть сформулированы и без них.
|
|
|
|
|
|
\chapter{Формальный вывод}
|
|
|
\label{chap:v-formal_deduction}
|
|
|
@@ -961,6 +1467,12 @@ stub
|
|
|
|
|
|
stub
|
|
|
|
|
|
+\begin{SCEnvWLabel}{Замечание\kern1ex1.}{remark:p27-1}{1}
|
|
|
+Таким образом, в формальной системе \ldots
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+stub
|
|
|
+
|
|
|
\section{Оценка, непротиворечивость}
|
|
|
\label{sec:28-valuation_consistency_vi}
|
|
|
|
