\part{Математическая логика}
\label{part:II-mathematical_logic}

%% ======================= Страница 67 =======================

\chapter{Формальная система}
\label{chap:iv-a_formal_system}

\section{Формальные символы}
\label{sec:16-formal_symbols}

Введём теперь некоторую конкретную формальную систему. Система, описываемая в
этой главе, явится предметом рассмотрения в четырёх последующих главах и в части
дальнейших глав. Эта система представляет собой формализацию некоторой части
классической элементарной теории чисел и включает необходимую для этого логику.

При построении системы мы использовали следующие работы: Гильберт и
Аккерман~\cite{hilbert_and_ackerman1928}, Гильберт и
Бернайс~\cite{hilbert_and_bernays1934,hilbert_and_bernays1939},
Генцен~\cite{gentzen1934-1935}, Бернайс~\cite{bernays1936} и некоторые другие не
столь явные источники.

Возможны два аспекта нашей задачи. Либо должна быть описана и исследована сама
формальная система~---~финитными методами и без использования
какой\nobreakdash-нибудь её интерпретации~---~это будет метаматематика; либо
должна быть найдена интерпретация системы, в силу которой эта система окажется
формализацией арифметики.

Возможен подход, при котором подчёркивается второй аспект, а именно, можно
анализировать существующую неформальную математику, выбирая и фиксируя основные
концепции, предположения и дедуктивные связи, и таким образом прийти в конце
концов к формальной системе.

Здесь, однако, мы вместо этого будем с самого начала подчёркивать первый аспект.
Формальная система будет введена сразу во всей её законченной многосложности, и
в метаматематических исследованиях мы только при случае будем обращать внимание
на интерпретацию. Мы рекомендуем читателю сосредоточиться на внимательном
изучении того, что представляет собой формальная система и как она исследуется.
Интерпретация и основания, по которым при построении этой конкретной системы был
сделан тот или иной выбор, будут постепенно выявляться по мере дальнейшего
изложения.

Первый шаг при установлении формальной системы состоит в перечислении
\emph{формальных символов}. Перечень формальных символов структурно аналогичен
алфавиту языка, хотя при интерпретации многие из формальных символов
соответствуют скорее целым словам и фразам, чем отдельным буквам. Перечень
формальных символов таков:

\emph{Логические символы}:~$\OLimpl$~(влечёт), $\OLand$~(и), $\vee$~(или),
$\neg$~(не), $\forall$~(для всех), $\exists$~(существует). \emph{Символы
предикатов}:~$=$~(равняется). \emph{Символы функций}:~$+$~(плюс),
$\OLmult$~(умножить на), $'$~(следующее за).
\emph{Индивидуальные символы}:~$0$~(нуль).
\emph{Переменные}:~${\frml{a},\frml{b},\frml{c},\ldots}$.
\emph{Скобки}:~${(,)}$.

Слова, указанные в скобках, могут применяться при чтении этих символов и
предназначаются для предварительного указания интерпретаций, например,
интерпретации логических символов как ,,логических констант``. Переменные
считаются пробегающими натуральные числа. Предполагается, что
(потенциально,~ср.~\textsection~\ref{sec:13-intuitionism}) имеется налицо
бесконечный перечень или нумерация переменных.

%% ======================= Страница 68 =======================

Мы повторяем, что интерпретации не существенны при описании формальной системы
как таковой. Должна иметься возможность рассматривать формальные символы как
простые знаки, а не как символы, которые что\nobreakdash-либо означают.
Предполагается только, что мы умеем распознавать каждый формальный символ как
тот же самый при каждом из его вхождений и отличать его от всех других
формальных символов. В частности, предполагается, что мы умеем распознавать
переменные.

Формальные символы образуют первую категорию формальных объектов. Исходя из них,
мы получаем вторую категорию путём построения конечных последовательностей
вхождений формальных символов. Эти последовательности мы будем называть
\itemlabel{def:p16-formal_expression}{def:p16-formal_expression}%
\emph{формальными выражениями}. Употреблённое только что слово <<вхождение>>
означает, что члены последовательности рассматриваются именно в качестве членов,
т.~е. подчёркивает то обстоятельство, что различные члены могут быть одним и тем
же символом (что согласуется с нашим прежним употреблением термина
,,последовательность``,
см.,~например,~\textsection\textsection~\ref{sec:1-enumerable_sets},~%
\ref{sec:2-cantor_s_diagonal_method}). К формальным выражениям относятся также
выражения, состоящие из единственного (вхождения) формального символа. Если не
оговорено противное, пустая последовательность (не имеющая членов) не будет
рассматриваться как формальное выражение. Например,
$0$,~${(\frml{a})+(\frml{b})}$‚ ${(\frml{a})=(0)}$ и~${((0\forall 00=}$~являются
формальными выражениями. Последнее из них состоит из семи (вхождений) символов,
т.~е. имеет семь членов; третье, пятое и шестое вхождения символов в это
формальное выражение являются каждое вхождением~$0$; различные входящие в него
символы~---~это~$($,~$0$,~$\forall$‚~$=$. Формальные выражения структурно
аналогичны словам языка, но при интерпретации некоторые из них соответствуют
целым предложениям, например~${(\frml{a})=(0)}$‚ а другие не имеют смысла,
например~${((0\forall 00=}$. Здесь снова наша терминология указывает на то
обстоятельство, что для формальной системы как таковой выражения ничего не
выражают, а являются только некоторыми распознаваемыми и различимыми объектами.
%%
%% исправлена опечатка в оригинале было
%% "третье, пятое и шестое вхождение символов"
%%

Мы будем также употреблять в качестве третьей категории формальных объектов
конечные последовательности (вхождений) формальных выражений.

В рассуждениях о формальных объектах мы часто будем не выписывать их, а
представлять (т.~е. обозначать) вводимыми для этой цели буквами или же
выражениями, содержащими уже введённые таким образом буквы. Например,
буква~<<$\infr{s}$>> может представлять формальное
выражение~${(\frml{a})+(\frml{b})}$‚ а
буква~<<$\infr{A}$>>~---~представлять~${(\frml{a})=(0)}$. Читатель очень
скоро встретит и другие примеры.

Употребляемые таким образом буквы и выражения являются не формальными символами
и выражениями, а содержательными, или метаматематическими, символами и
выражениями, которые играют роль названий формальных объектов. Здесь, по
сравнению с обычным неформальным употреблением символизма, имеется новая
черта~---~называемые объекты являются, в свою очередь, символами или объектами,
построенными из символов. Мы должны, таким образом, проводить различие между
символизмами двух родов~---~формальным символизмом, о котором мы говорим, и
интуитивным или метаматематическим символизмом, которым мы говорим о другом
символизме. Для каждого из этих символизмов мы будем пользоваться различными
шрифтами~(${\frml{a},\frml{b},\frml{t},\frml{x},\frml{A},\frml{B}}$
и~${\infr{a},\infr{b},\infr{t},\infr{x},\infr{A},\infr{B}}$), что
поможет нам непосредственно выражать это обстоятельство.

Использование символов и выражений в качестве названий предметов, о которых мы
говорим, не является чем\nobreakdash-либо новым; именно такова наша повседневная
практика построения фразы о каком\nobreakdash-либо предмете. Новым, однако,
является другой процесс, которым мы отчасти пользуемся в
метаматематике‚~---~вставление самого предмета, т.~е. экземпляра этого предмета,
непосредственно в предложение. Хотя этим и нарушаются обычные грамматические
каноны, в метаматематике это не приводит к недоразумениям, потому что в
метаматематике нам приходится рассматривать формальные символы как не имеющие
%% ======================= Страница 69 =======================
смысла, и потому формальные объекты не могут служить названиями для других
объектов, а предложение, содержащее экземпляр формального объекта, может
говорить только о самом этом формальном объекте.

Эти замечания относятся к нашей метаматематике. Далее
в~\ref{secdbl:interpretation-0}, мы сможем придать формальным символам
содержательное истолкование, рассматривая их как имеющие смысл.

При метаматематическом изучении формальных выражений мы будем пользоваться
операцией \emph{соединения} (или \emph{сочленения}), посредством которой две или
более последовательности формальных символов соединяются последовательно,
образуя новую последовательность. Например, сочленение двух формальных выражений
${((0\forall 00=}$~и~${(\frml{a})+(\frml{b})}$ в указанном порядке образует
новое формальное выражение~${((0\forall 00=(\frml{a})+(\frml{b})}$, а
сочленение семи формальных выражений~$($‚~${(\frml{a})+(\frml{b})}$‚~$)$,~%
$\OLmult$‚~$($‚~${(\frml{c})'}$‚~$)$ в указанном порядке образует новое
формальное выражение~${\left((\frml{a})+(\frml{b})\right)\OLmult%
                       \left((\frml{c})'\right)}$.

Если некоторые из подлежащих сочленению формальных выражений представлены
метаматематическими буквами или выражениями, то последние могут употребляться в
записи результата сочленения вместо представляемых ими формальных выражений.
Например, если буква <<$\infr{s}$>> представляет некоторое формальное
выражение, то результат сочленения семи формальных
выражений~$($‚~$\infr{s}$‚~$)$,~$\OLmult$‚~$($‚~${(\frml{c})'}$‚~$)$
записывается так:~<<${(\infr{s})\OLmult\left((\frml{c})'\right)}$>>. Здесь
<<${(\infr{s})\OLmult\left((\frml{c})'\right)}$>>~есть метаматематическое
выражение, представляющее формальное выражение, и это формальное выражение
зависит от того, какое формальное выражение представляет буква~<<$\infr{s}$>>.
В частности, если $\infr{s}$~есть~${(\frml{a})+(\frml{b})}$, то
${(\infr{s})\OLmult\left((\frml{c})'\right)}$~есть~%
${\left((\frml{a})+(\frml{b})\right)\OLmult\left((\frml{c})'\right)}$.

\section{Правила образования}
\label{sec:17-formation_rules}

Мы теперь определим некоторые подкатегории формальных выражений посредством
определений, аналогичных правилам синтаксиса в грамматике.

Сначала определим ,,терм``‚ который аналогичен существительному в грамматике.
Термы рассматриваемой системы все представляют натуральные числа, фиксированные
или переменные. Определение формулируется с помощью метаматематических
переменных <<$\infr{s}$>>~и~<<$\infr{t}$>> и описанной выше операции сочленения.
Оно имеет вид индуктивного определения, что позволяет нам переходить от уже
известных термов к дальнейшим.

1.\itemlabel{listItem:p17-list1-1}{1}~$0$~есть \emph{терм}.
2.\itemlabel{listItem:p17-list1-2}{2}~Каждая переменная есть \emph{терм}.
3--5.%
\itemlabel{listItem:p17-list1-3}{3}%
\itemlabel{listItem:p17-list1-4}{4}%
\itemlabel{listItem:p17-list1-5}{5}~Если
$\infr{s}$~и~$\infr{t}$~---~\emph{термы}, то
${(\infr{s})+(\infr{t})}$‚ ${(\infr{s})\OLmult(\infr{t})}$ и
${(\infr{s})'}$~---~\emph{термы}.
6.\itemlabel{listItem:p17-list1-6}{6}~ Никаких других \emph{термов}, кроме
определённых согласно~\ref{listItem:p17-list1-1}--\ref{listItem:p17-list1-5},
нет.

\begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p17-1}{exmpl:p17-1}
В силу \ref{listItem:p17-list1-1}~и~\ref{listItem:p17-list1-2}, термами
являются~$0$, $\frml{a}$, $\frml{b}$ и~$\frml{c}$. Поэтому, в
силу~\ref{listItem:p17-list1-5}, ${(0)'}$~и~${(\frml{c})'}$ являются термами.
Снова в силу~\ref{listItem:p17-list1-5}, ${\left((0)'\right)'}$~есть~терм, а в
силу~\ref{listItem:p17-list1-3},
${\left((\frml{c})'\right)+(\frml{a})}$~есть терм.
\end{SCEnvWLabel}

Теперь дадим определение ,,формулы``~---~аналога (повествовательного)
предложения в грамматике.

1.\itemlabel{listItem:p17-list2-1}{1}~Если
$\infr{s}$~и~$\infr{t}$~---~термы, то
${(\infr{s})=(\infr{t})}$~---~\emph{формула}.
2--5.%
\itemlabel{listItem:p17-list2-2}{2}%
\itemlabel{listItem:p17-list2-3}{3}%
\itemlabel{listItem:p17-list2-4}{4}%
\itemlabel{listItem:p17-list2-5}{5}~Если
$\infr{A}$~и~$\infr{B}$~---~\emph{формулы}, то
${(\infr{A})\OLimpl(\infr{B})}$,
${(\infr{A})\OLand(\infr{B})}$,
${(\infr{A})\vee(\infr{B})}$ и
${\neg(\infr{A})}$~---~\emph{формулы}.
6--7.%
\itemlabel{listItem:p17-list2-6}{6}%
\itemlabel{listItem:p17-list2-7}{7}~Если $\infr{x}$~---~переменная, а
$\infr{A}$~---~\emph{формула}, то
${\forall\infr{x}(\infr{A})}$~и~%
${\exists\infr{x}(\infr{A})}$~---~\emph{формулы}.
8.\itemlabel{listItem:p17-list2-8}{8}~Никаких \emph{формул}, кроме определённых
согласно~\ref{listItem:p17-list2-1}--\ref{listItem:p17-list2-7}, нет.

\begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p17-2}{exmpl:p17-2}
Используя~\ref{listItem:p17-list2-1} и уже полученные примеры термов, убеждаемся
в том, что ${(\frml{a})=(\frml{b})}$ и~%
${\left(\left(\left(\frml{c}\right)'\right)+\left(\frml{a}\right)\right)=%
  \left(\frml{b}\right)}$~---~формулы. Поэтому, в
силу~\ref{listItem:p17-list2-5}~и~\ref{listItem:p17-list2-7},
${\neg\left(\left(\frml{a}\right)=\left(\frml{b}\right)\right)}$ и %
${\exists\frml{c}%
\left(%
    \left(%
        \left(%
            \left(\frml{c}\right)'%
        \right)+%
        \left(\frml{a}\right)%
    \right)=%
    \left(\frml{b}\right)%
\right)}$~---~формулы. Наконец, в силу~\ref{listItem:p17-list2-2}, формулой
является
\begin{equation}\label{eq:p17-A}\tag{A}
\left(
    \exists\frml{c}
    \left(
        \left(
            \left(
                \left(\frml{c}\right)'
            \right)+
            \left(\frml{a}\right)
        \right)=
        \left(\frml{b}\right)
    \right)
\right)\OLimpl
\left(
    \neg
    \left(
        \left(\frml{a}\right)=\left(\frml{b}\right)
    \right)
\right)\text{.}
\end{equation}

%% ======================= Страница 70 =======================

Из индуктивных определений терма и формулы следует, что каждый терм и каждая
формула могут быть построены из $0$~и переменных посредством ряда шагов, каждый
из которых соответствует некоторому прямому пункту одного из этих
определений~(\textsection~\ref{sec:6-the_natural_numbers}) и может быть назван
\emph{применением} этого пункта.

Каждый шаг, за исключением применений
пунктов~\ref{listItem:p17-list1-1}~или~\ref{listItem:p17-list1-2} из определения
терма, производится следующим образом: вначале нам дано одно или два ранее
полученных выражения. Заключаем данное выражение или каждое из данных выражений
в скобки и вводим выражение одного из следующих десяти видов:
\begin{equation}\label{eq:p17-B}\tag{B}
\OLimpl,\;\;\;\OLand,\;\;\;\vee,\;\;\;\neg,\;\;\;\forall\infr{x},\;\;\;%
\exists\infr{x},\;\;\;=,\;\;\;+,\;\;\;\OLmult,\;\;\;'\text{,}
\end{equation}

\noindent%
где $\infr{x}$~---~переменная. Выражение каждого из этих десяти видов мы будем
называть \emph{оператором}. В частности,
$\OLimpl$,~$\OLand$,~$\vee$,~$\neg$~являются \emph{пропозициональными связками},
а операторы вида ${\forall\infr{x}}$~или~${\exists\infr{x}}$~суть
\emph{кванторы}, причём ${\forall\infr{x}}$~---~\emph{квантор общности}, а
${\exists\infr{x}}$~---~\emph{квантор существования}; операторы этих шести
видов называются \emph{логическими операторами}.

Данное выражение или пара выражений называются \emph{областью действия}
оператора в получающемся выражении. Прослеживая всё построение терма или
формулы, устанавливая очевидным образом соответствие между частями данного
выражения или пары выражений и частями выражения получающегося на каждом шаге
построения, мы приходим к определению \emph{области действия} не только для
оператора, введённого последним в законченный терм или формулу, но и для всякого
оператора в этом терме или формуле.
\end{SCEnvWLabel}

\begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p17-3}{exmpl:p17-3}
В формуле~\eqref{eq:p17-A} область действия первого вхождения оператора~$=$
состоит из
части~${\left(\left(\frml{c}\right)'\right)+\left(\frml{a}\right)}$ и
первого вхождения $\frml{b}$, а область действия ${\exists\frml{c}}$~есть
часть~${%
\left(
    \left(
        \left(\frml{c}\right)'
    \right)+
    \left(\frml{a}\right)
\right)=
\left(\frml{b}\right)}$.
\end{SCEnvWLabel}

Отметим теперь следующий факт, к строгому доказательству которого мы сейчас
перейдём. В данном терме или данной формуле области действия операторов можно
установить однозначно, исходя из расположения скобок. Другими словами, скобки
дают возможность, коль скоро дан терм или формула как конечная
последовательность формальных символов, восстановить все существенные детали его
(её) построения согласно индуктивным определениям терма и формулы.

Строгое доказательство этого факта даётся
леммой~\ref{lemma:p7-2}~(\textsection~\ref{sec:7-mathematical_induction},
пример~\ref{exmpl:p7-2}) вместе со следующей леммой, которую можно доказать по
индукции, исходя из индуктивных определений терма и формулы.

\begin{SCEnvWLabel}{Лемма\kern1ex4.}{lemma:p17-4}{4}
\emph{В каждом данном терме или формуле существует собственное спаривание
скобок} (\emph{число всех скобок равно}~${2n}$, \emph{из них} $n$~\emph{левых
скобок и} $n$~\emph{правых}), \emph{такое}, \emph{что область действия всякого
оператора входит следующим образом}:

(a)\kern1ex\emph{Для операторов}, \emph{область действия которых состоит только
из одного выражения}, \emph{эта область действия непосредственно заключается в
парные скобки и оператор ставится вне этой пары скобок вплотную к ней},
\emph{т}.~\emph{е}. \emph{непосредственно слева от левой скобки} (\emph{в
случае}~$\neg$,~${\forall\infr{x}}$,~${\exists\infr{x}}$) \emph{или
непосредственно справа от правой скобки} (\emph{в случае}~$'$).

(b)\kern1ex\emph{Для операторов}, \emph{область действия которых состоит из двух
выражений} (\emph{именно}~$\OLimpl$,~$\OLand$,~$\vee$,~$=$,~$+$,~$\OLmult$)‚
\emph{каждое из этих двух выражений непосредственно заключается в парные
скобки}, \emph{а оператор ставится непосредственно между правой скобкой пары},
\emph{в которую заключено левое выражение}, \emph{и левой скобкой пары}, \emph{в
которую заключено правое выражение}.
\end{SCEnvWLabel}

\begin{SCEnvWLabel}{Пример\kern1ex3\kern1ex\textup{(окончание)}.}%
{exmpl:p17-3-end}{exmpl:p17-3-end}
Рассмотренный пример формулы~\eqref{eq:p17-A} содержит 22 скобки. По
лемме~\ref{lemma:p17-4}, эти 22 скобки допускают собственное спаривание,
%% ======================= Страница 71 =======================
которое находится из процесса построения формулы согласно определениям терма и
формулы и которое указывает области действия операторов. Так как существует
собственное спаривание, то, по лемме~\ref{lemma:p7-2}, это спаривание однозначно
и поэтому может быть найдено посредством алгоритма
из~\textsection~\ref{sec:7-mathematical_induction}, без предварительного знания
построения формулы согласно определениям терма и формулы. Мы фактически уже
проделали это в конце~\textsection~\ref{sec:7-mathematical_induction}, где те же
самые 22 скобки рассматривались независимо от стоящих между ними символов.
Пользуясь полученным разбиением на пары для этих 22 скобок, входящих в полную
формулу~\eqref{eq:p17-A}, можно заметить, что область действия первого
вхождения~$=$ состоит из выражения, заключённого между
скобками~${\big(\vphantom{a}^{3}_{4}\;\:\big)\vphantom{a}^{10}_{4}}$, и
выражения, заключённого между
скобками~${\big(\vphantom{a}^{11}_{5}\;\:\big)\vphantom{a}^{12}_{5}}$. Это
согласуется с нашим прежним определением этой области действия. Аналогично,
область действия~${\exists\frml{c}}$ заключена между
скобками~${\big(\vphantom{a}^{2}_{6}\;\:\big)\vphantom{a}^{13}_{6}}$.
\end{SCEnvWLabel}

Лемма~\ref{lemma:p7-3} из~\textsection~\ref{sec:7-mathematical_induction}, хотя
она и не требуется для доказательства того, что области действия могут быть
найдены по распределению скобок, полезна при рассуждениях об областях действий в
частях и во всем выражении (терме или формуле). Например, если
$\infr{M}$,~$\infr{N}$~и~$\infr{A}$~---~формулы и $\infr{A}$~входит
в~${\left(\infr{M}\right)\OLimpl\left(\infr{N}\right)}$ как (связная) часть,
отличная от всей формулы, то можно заключить, что эта часть (или каждая такая
часть) является частью~$\infr{M}$ или частью~$\infr{N}$.

При выборе наших определений терма и формулы мы, конечно, вводили скобки ради
вышеизложенной цели, однозначного определения областей действия. Ясно, однако,
что обычно в определениях вводят больше скобок, чем строго необходимо для этой
цели. Ничего не меняя в определениях, мы можем согласиться опускать лишние
скобки для сокращения записи термов и формул или представляющих их
метаматематических выражений.

Возможности в этом направлении расширяются употреблением соглашений, аналогичных
тем, которые приняты в алгебре, где <<${a\OLmult b+c}$>> понимается в 
смысле~${\left(a\OLmult b\right)+c}$. Мы будем говорить в этом случае, что
$+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚ и припишем нашим операторам
ранги, понижающиеся в том порядке, в котором мы их перечислили выше
в~\eqref{eq:p17-B}. Чтобы восстановить любые скобки, опущенные при сокращении
терма или формулы, можно, выбирая последовательно каждый раз из всех
присутствующих операторов тот, который раньше других встречается в
списке~\eqref{eq:p17-B}, т.~е. оператор наивысшего ранга, придавать ему
наибольшую область действия, совместимую с требованием, чтобы всё выражение было
термом или формулой.
%%
%% исправлен шрифт в алгебраических формулах
%% надо отметить, что в оригинале присутсвует тот же недочёт, что и в переводе -
%% используется не подходящий по смыслу шрифт
%%

Мы не всегда будем опускать максимальное число скобок, допускаемое нашим
соглашением, стремясь обеспечить максимальное удобство для чтения. (С этой целью
мы будем также иногда заменять круглые скобки на квадратные или фигурные.)

\begin{SCEnvWLabel}{Пример\kern1ex4.}{exmpl:p17-4}{exmpl:p17-4}
Восстановление скобок
в~<<${\infr{A}\OLimpl\infr{B}\vee\infr{C}\OLand\infr{D}}$>> даёт
последовательно~%
<<${\infr{A}\OLimpl\left(\infr{B}\vee\infr{C}\OLand\infr{D}\right)}$>>,
<<${\infr{A}\OLimpl\left(
    \left(\infr{B}\vee\infr{C}\right)
    \OLand\infr{D}
\right)}$>>,
<<${\left(\infr{A}\right)\OLimpl
\left(
    \left(
        \left(\infr{B}\right)\vee\left(\infr{C}\right)
    \right)
    \OLand\left(\infr{D}\right)
\right)}$>>. Рассмотренный пример формулы~\eqref{eq:p17-A} сокращённо
записывается в виде
\begin{equation}\label{eq:p17-A-stroke}\tag{A$'$}
\exists\frml{c}
\left(\frml{c}'+\frml{a}=\frml{b}\right)
\OLimpl\neg\frml{a}=\frml{b}\text{.}
\end{equation}

Другого рода сокращения даёт нам введение нового символа вместе с методом
обратного перевода любого выражения, содержащего новый символ, в выражение, не
содержащее последнего. Например,
термы~${
\left(0\right)',
\left(\left(0\right)'\right)',
\left(\left(\left(0\right)'\right)'\right)'\ldots}$ мы сокращаем
соответственно в~<<$1$>>,~<<$2$>>,~<<$3$>>,~$\ldots\:$;
формулу~${\neg\frml{a}=\frml{b}}$ сокращаем в~<<${\frml{a}\neq\frml{b}}$>>, а
формулу~${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)}$
сокращаем в <<${\frml{a}<\frml{b}}$>>. Рассмотренная
формула~\eqref{eq:p17-A} может быть при этом записана так:
\begin{equation}\label{eq:p17-A-stroke-stroke}\tag{A$''$}
\frml{a}<\frml{b}\OLimpl\frml{a}\neq\frml{b}\text{.}
\end{equation}
\end{SCEnvWLabel}

%% ======================= Страница 72 =======================

Общее правило для сокращения <<$\neq$>> позволяет нам
писать~<<${\infr{s}\neq\infr{t}}$>> как сокращение
для~${\neg\infr{s}=\infr{t}}$‚ где $\infr{s}$~и~$\infr{t}$~---~термы. Общее
правило для сокращения~<<$<$>> позволяет нам
писать~<<${\infr{s}<\infr{t}}$>> как сокращение
для~${\exists\infr{x}\left(\infr{x}'+\infr{s}=\infr{t}\right)}$‚
где $\infr{x}$~---~переменная, а $\infr{s}$~и~$\infr{t}$~---~термы, не
содержащие~$\infr{x}$. При восстановлении сокращения, если оно было связано с
опусканием переменной, как в случае~<<$<$>>, имеется произвол в отношении выбора
подлежащей восстановлению переменной. Так, при
восстановлении~<<${\infr{s}<\infr{t}}$>> мы можем выбрать в
качестве~$\infr{x}$ любую переменную, не содержащуюся в~$\infr{s}$~и~$\infr{t}$.
Этот произвол является мало существенным, поскольку утверждения, которые мы
собираемся делать о сокращённой формуле, имеют место независимо от выбора
допустимой переменной.

Мы будем считать, что все эти сокращения относятся только к изложению
метаматематики. Это соответствует нашим целям, и таким путём мы сохраняем
теоретически более простые основные определения, посредством которых
устанавливается формальная система. Метаматематические утверждения о термах и
формулах системы должны поэтому рассматриваться как относящиеся к несокращённым
выражениям в буквальном смысле определений, какого бы рода стенографией мы ни
пользовались при записи этих утверждении.

\section{Свободные и связанные переменные}
\label{sec:18-free_and_bound_variables}

Вхождение переменной~$\infr{x}$ в формулу~$\infr{A}$ называется \emph{связанным}
(или вхождением в качестве \emph{связанной переменной}), если оно является
вхождением в квантор~${\forall\infr{x}}$ или~${\exists\infr{x}}$ или в область
действия квантора~${\forall\infr{x}}$ или~${\exists\infr{x}}$ (с тем же
самым~$\infr{x}$); в противном случае вхождение называется \emph{свободным} (или
вхождением в качестве \emph{свободной переменной}).

\begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p18-1}{exmpl:p18-1}
В~${
\exists\frml{c}
\left(\frml{c}'+\frml{a}=\frml{b}\right)
\OLimpl\neg\frml{a}=\frml{b}}$‚ оба вхождения~$\frml{a}$ и оба
вхождения~$\frml{b}$~---~свободные‚ а оба вхождения~$\frml{c}$~---~связанные.
В~${
\exists\frml{c}
\left(\frml{c}'+\frml{a}=\frml{b}\right)
\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$ первые два
вхождения~$\frml{c}$~---~связанные, а третье~---~свободное.
В~${
\exists\frml{c}\left(
    \exists\frml{c}\left(
        \frml{c}'+\frml{a}=\frml{b}
    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
\right)}$ все вхождения~$\frml{c}$~---~связанные.
\end{SCEnvWLabel}

Мы будем говорить также, что любое вхождение переменной~$\infr{x}$ в
терм~$\infr{t}$ является \emph{свободным}, как это будет следовать из
приведённого определения, если заменить в нем слова <<формула~$\infr{A}$>> на
<<терм~$\infr{t}$>>. Различие между свободным и связанным вхождением переменной
всегда связано с термом или формулой, для которых (в каждом случае)
рассматривается это вхождение.

\begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p18-2}{2}
Третье вхождение~$\frml{c}$ в~${
\exists\frml{c}\left(
    \exists\frml{c}\left(
        \frml{c}'+\frml{a}=\frml{b}
    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
\right)}$ является свободным, если его рассматривать как вхождение в саму эту
часть~$\frml{c}$, или в часть~${\frml{c}'}$, или в
часть~${\frml{c}'+\frml{a}}$‚ или в
часть~${\frml{c}'+\frml{a}=\frml{b}}$, и связанным, если его рассматривать как
вхождение в часть~${
\exists\frml{c}\left(
    \frml{c}'+\frml{a}=\frml{b}
\right)}$‚ или в часть~${
\exists\frml{c}\left(
    \frml{c}'+\frml{a}=\frml{b}
\right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$, или во всю формулу.
\end{SCEnvWLabel}

Если переменная~$\infr{x}$ входит в качестве свободной переменной (коротко:
входит свободно) в~$\infr{A}$, то говорят, что $\infr{x}$~является
\emph{свободной переменной} выражения~$\infr{A}$, или что
$\infr{A}$~\emph{содержит}~$\infr{x}$ \emph{в качестве свободной переменной}
(коротко: $\infr{A}$~\emph{содержит свободно}~$\infr{x}$); аналогично для
связанных переменных.

\begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p18-3}{exmpl:p18-3}
Свободные переменные в~${
\exists\frml{c}\left(
    \frml{c}'+\frml{a}=\frml{b}
\right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$
суть~$\frml{a}$,~$\frml{b}$~и~$\frml{c}$, а единственная связанная переменная
есть~$\frml{c}$.
\end{SCEnvWLabel}

Связанное вхождение переменной~$\infr{x}$ в формулу~$\infr{A}$ связано
\emph{тем} вхождением квантора~${\forall\infr{x}}$ или~${\exists\infr{x}}$ (с
тем же самым~$\infr{x}$), в области действия которого
%% ======================= Страница 73 =======================
оно встречается и которое имеет при этом наименьшую область действия (короче,
посредством самого внутреннего квантора, в области действия которого оно
встречается), или в случае, когда оно является вхождением в
квантор~${\forall\infr{x}}$ или~${\exists\infr{x}}$, самим этим квантором
(говорят также, что квантор \emph{связывает} эту переменную).

\begin{SCEnvWLabel}{Пример\kern1ex4.}{exmpl:p18-4}{4}
В~${
\exists\frml{c}\left(
    \exists\frml{c}\left(
        \frml{c}'+\frml{a}=\frml{b}
    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
\right)}$ первое и четвёртое вхождения~$\frml{c}$ связаны первым
квантором~${\exists\frml{c}}$, а второе и третье вхождения~$\frml{c}$~---~вторым
квантором~${\exists\frml{c}}$.
\end{SCEnvWLabel}

Связанное вхождение переменной в формулу связано тем квантором, введение
которого (при построении этой формулы, согласно определениям терма и формулы)
впервые превратило это вхождение из свободного в связанное (или, если это
переменная в кванторе,~---~тем квантором, в котором она вводится).

\begin{SCEnvWLabel}{Пример\kern1ex5.}{exmpl:p18-5}{exmpl:p18-5}
Сравните пример~\ref{exmpl:p18-4} с примером~\ref{exmpl:p18-2}.
\end{SCEnvWLabel}

Сделаем теперь несколько предварительных замечаний об интерпретации свободных и
связанных переменных (называемых иногда ,,действительными`` и ,,кажущимися``
переменными). Эти замечания, конечно, не являются частью метаматематики, но они
должны способствовать усвоению метаматематических различий. Выражение,
содержащее свободную переменную, представляет величину или предложение,
зависящее от значения этой переменной. Выражение, содержащее связанную
переменную, представляет результат операции, применённой к области изменения
этой переменной. Наши связанные переменные относятся к логическим операциям
квантификации, но имеются примеры с операциями другого рода, обычными в
математике. В следующих примерах $n$~и~$y$ свободны, а $i$~и~$x$ связаны:
\begin{equation}\label{eq:p18-A}\tag{A}
\sum_{i=1}^{n} a_{i},\;\;\;\;\;\;\;
\lim_{x\to 0} f(x,y),\;\;\;\;\;\;\;
\int\displaylimits_{-y}^{y}  f(x,y)dx\text{.}
\end{equation}

В следующем примере вхождение~$t$ в качестве верхнего предела интегрирования
свободно, а вхождения в подинтегральное выражение~---~связаны:
\begin{equation}\label{eq:p18-B}\tag{B}
\int\displaylimits_{0}^{t}  f(t)dt\text{.}
\end{equation}

Возвращаясь к интерпретации, можно отметить некоторые характерные различия,
которым она подвергает способ пользования обоими родами переменных в
неформальной математике. Связанная переменная является частью описания,
выражающего результат операции, выполненной над областью изменения переменной, и
поэтому можно (соблюдая некоторые предосторожности), не меняя смысла, заменить
эту переменную на любую другую, имеющую ту же самую область изменения. Например,
\begin{equation}\label{eq:p18-C}\tag{C}
\sum_{j=1}^{n} a_{j},\;\;\;\;\;\;\;
\lim_{z\to 0} f(z,y),\;\;\;\;\;\;\;
\int\displaylimits_{-y}^{y}  f(t,y)dt
\end{equation}

\noindent%
означают (обычно) то же самое, что и соответствующие выражения~\eqref{eq:p18-A},
приведённые выше (но ${\displaystyle{\lim_{y\to 0} f(y,y)}}$~не совпадает
(обычно) с~${\displaystyle{\lim_{x\to 0} f(x,y)}}$). Если в некоторое выражение
подставить вместо свободной переменной выражение, представляющее постоянный или
переменный предмет из области
%% ======================= Страница 74 =======================
её изменения, мы (обычно) получим осмысленный результат, но эта же подстановка,
применённая к связанной переменной, может привести к бессмыслице. Например
(подстановкой в~\eqref{eq:p18-A}), получаем (обычно) осмысленные выражения
\begin{equation}\label{eq:p18-D}\tag{D}
\sum_{i=1}^{5} a_{i},\;\;\;\;\;\;\;
\lim_{x\to 0} f(x,2),\;\;\;\;\;\;\;
\int\displaylimits_{-z}^{z}  f(x,z)dx\text{,}
\end{equation}

\noindent%
но этого нельзя сказать о
\begin{equation}\label{eq:p18-E}\tag{E}
\sum_{5=1}^{n} a_{5},\;\;\;\;\;\;\;
\lim_{2\to 0} f(2,y),\;\;\;\;\;\;\;
\int\displaylimits_{-z}^{z}  f(0,z)d0\text{.}
\end{equation}

\noindent%
Если одна и та же переменная входит в выражение и как свободная, и как
связанная, то представляемая этим выражением величина зависит только от значения
этой переменной в её свободных вхождениях. Таким образом,
интеграл~\eqref{eq:p18-B} является функцией от~$t$, значение которой для~${t=3}$
есть
\begin{equation}\label{eq:p18-F}\tag{F}
\int\displaylimits_{0}^{3}  f(t)dt\text{,}\;\;\;\;\;\;\;\text{но не}\;\;\;%
\int\displaylimits_{0}^{3}  f(3)d3\text{.}
\end{equation}

\begin{SCEnvWLabel}{Подстановка.}{spar:p18-substitution}{spar:p18-substitution}
При формулировке метаматематических определений следующего параграфа мы
используем операцию подстановки, которую мы определим следующим образом.
\emph{Подстановка} терма~$\infr{t}$ \emph{вместо} переменной~$\infr{x}$ \emph{в}
(или, иначе, \emph{повсюду в}) терм или формулу~$\infr{A}$ состоит в
одновременной замене каждого свободного вхождения~$\infr{x}$ в~$\infr{A}$
на вхождение~$\infr{t}$. Чтобы описать это в терминах сочленения, обозначим
через~$n$ число свободных вхождений~$\infr{x}$ в~$\infr{A}$~(${n\geqslant 0}$) и
запишем~$\infr{A}$ в виде~<<${\infr{A}_{0}\infr{x}\infr{A}_{1}\infr{x}\;\ldots\;
\infr{A}_{n-1}\infr{x}\infr{A}_{n}}$>>‚ указывающем эти вхождения
(где~${\infr{A}_{0},\infr{A}_{1}, \ldots,%
       \infr{A}_{n-1},\infr{A}_{n}}$~---~части‚ возможно пустые, не содержащие
вхождений~$\infr{x}$, свободных относительно всего~$\infr{A}$, и все указанные
$n$~вхождений~$\infr{x}$ свободны). Тогда результатом подстановки~$\infr{t}$
вместо~$\infr{x}$ в~$\infr{A}$
будет~${\infr{A}_{0}\infr{t}\infr{A}_{1}\infr{t}\;\ldots\;
\infr{A}_{n-1}\infr{t}\infr{A}_{n}}$.
%%
%% исправлено выделение в определении
%% оно приведено в семантическое соответствие с англоязычным оригиналом
%%

Для представления результата подстановки будет полезно одно компактное
метаматематическое обозначение. Если подстановка производится вместо~$\infr{x}$,
введём сначала для субституэнда\footnote{Т.~е. выражения, в которое производится
подстановка. Употребление термина <<субституэнд>> в данной книге отличается от
принятого у Гильберта и Бернайса~\cite{hilbert_and_bernays1939} дополнение~I,
где рассматриваются подстановки вместо формульных переменных (ср.~ниже
стр.~\pageref{spar:p37-predicate_calculus_with_a_postulated_substitution_rule})
и субституэндом называется выражение, которое подставляется вместо данной
переменной.~---~\textit{Прим.~перев.}} некоторое составное выражение,
например~<<${\infr{A}(\infr{x})}$>>, показывающее его зависимость от~$\infr{x}$,
согласно способу обозначения для функций в
математике~(\textsection~\ref{sec:10-functions}). Результат
подстановки~$\infr{t}$ вместо~$\infr{x}$ в~${\infr{A}(\infr{x})}$ записывается
тогда в виде~<<${\infr{A}(\infr{t})}$>>.
\end{SCEnvWLabel}

\begin{SCEnvWLabel}{Пример\kern1ex6.}{exmpl:p18-6}{exmpl:p18-6}
Пусть $\infr{x}$~есть~$\frml{c}$, а\\
{\setlength{\tabcolsep}{0pt}\begin{tabular}{llll}
${\infr{A}(\infr{x})}$, или\kern1ex&${\infr{A}(\frml{c})}$,\kern1ex&есть\kern1ex
&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
\neg\frml{a}=\frml{b}+\frml{c}}$.\\
Тогда&${\infr{A}(0)}$&есть%
&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
\neg\frml{a}=\frml{b}+\frml{0}}$,\\
а&${\infr{A}(\frml{a})}$&есть%
&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
\neg\frml{a}=\frml{b}+\frml{a}}$.
\end{tabular}}
%%
%% исправлено представление Примера 6
%% оно приведено в соответствие с представлением англоязычного оригинала,
%% что делает Пример 6 яснее
%%
\end{SCEnvWLabel}

\begin{SCEnvWLabel}{Пример\kern1ex7.}{exmpl:p18-7}{exmpl:p18-7}
Пусть $\infr{x}$~есть~$\frml{a}$, а $\infr{A}(\infr{x})$~есть~%
${\frml{a}+\frml{c}=\frml{a}}$. Тогда ${\infr{A}(0)}$~есть~%
${0+\frml{c}=0}$, а ${\infr{A}(\frml{b})}$~есть~${\frml{b}+\frml{c}=\frml{b}}$.
\end{SCEnvWLabel}


Подстановка, которая даёт~${\infr{A}(\infr{t})}$, всегда должна производиться
вместо первоначальной переменной~$\infr{x}$ в первоначальной
формуле~${\infr{A}(\infr{x})}$, т.~е. вместо той переменной и в ту формулу, для
которых предварительно было введено обозначение <<${\infr{A}(\infr{x})}$>>.

%% ======================= Страница 75 =======================

\begin{SCEnvWLabel}{Пример\kern1ex7\kern1ex\textup{(окончание)}.}%
{exmpl:p18-7-end}{exmpl:p18-7-end}
Для указанных выше~$\infr{x}$~и~${\infr{A}(\infr{x})}$‚ ${\infr{A}(\frml{c})}$
есть~${\frml{c}+\frml{c}=\frml{c}}$. Если подставить~$\frml{b}$
вместо~$\frml{c}$ в~${\infr{A}(\frml{c})}$, то
получится~${\frml{b}+\frml{b}=\frml{b}}$. Это не совпадает
с~${\infr{A}(\frml{b})}$, которое прежде мы правильно получили посредством
подстановки~$\frml{b}$ вместо~$\frml{a}$ в~${\infr{A}(\frml{a})}$, т.~е. вместо
первоначального~${\infr{x}}$ в первоначальное~${\infr{A}(\infr{x})}$. (Это же
затруднение может встретиться при неправильном употреблении обозначений для
функции в неформальной математике.)
\end{SCEnvWLabel}


Мы не потребовали, чтобы переменная~$\infr{x}$ действительно входила
в~${\infr{A}(\infr{x})}$ в качестве свободной переменной. Если $\infr{x}$~не
является свободной переменной~${\infr{A}(\infr{x})}$‚ то результат
подстановки~${\infr{A}(\infr{t})}$ есть само первоначальное
выражение~${\infr{A}(\infr{x})}$.

Аналогично мы определим подстановку, произведённую одновременно вместо
нескольких различных переменных; мы будем пользоваться при этом аналогичными
обозначениями, например <<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>>~для
субституэнда и <<${\infr{A}(\infr{t}_{1},\ldots,\infr{t}_{n})}$>>~для
результата.

В дальнейшем мы часто будем вводить составные обозначения, например
<<${\infr{A}(\infr{x})}$>>~или~%
<<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>> вместо~<<$\infr{A}$>>, когда
нас будет интересовать зависимость~$\infr{A}$ от переменной~$\infr{x}$ или
переменных~${\infr{x}_{1},\ldots,\infr{x}_{n}}$ независимо от того, надо ли нам
будет или нет делать подстановку. Например, обычно мы обозначаем
формулу~<<${\infr{A}(\infr{x})}$>> вместо~<<$\infr{A}$>>, если собираемся
употребить её в~${\forall\infr{x}\infr{A}(\infr{x})}$ (читается <<для
всех~$\infr{x}$, $\infr{A}$~от~$\infr{x}$>>) или
в~${\exists\infr{x}\infr{A}(\infr{x})}$ (читается <<существует
некоторое~$\infr{x}$, такое, что $\infr{A}$~от~$\infr{x}$>> или, кратко,
<<существует~$\infr{x}$, $\infr{A}$~от~$\infr{x}$>>). Подчеркнём, что при
обозначении~<<${\infr{A}(\infr{x})}$>> (или
<<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>>) не подразумевается, что
$\infr{x}$~(или каждое из~${\infr{x}_{1},\ldots,\infr{x}_{n}}$) обязательно
входит свободно в обозначенную формулу.

Предварительные замечания об интерпретации проливают свет на то, почему при
нашем выборе определения для метаматематической операции подстановки последняя
применяется только к свободным вхождениям переменных.

Далее, мы будем говорить, что терм~$\infr{t}$ \emph{свободен при свободных
вхождениях} переменной~$\infr{x}$ \emph{в} формулу~${\infr{A}(\infr{x})}$ (или,
что $\infr{t}$~\emph{свободен на местах подстановки вместо}~$\infr{x}$
\emph{в}~${\infr{A}(\infr{x})}$‚ или, короче, что
$\infr{t}$~\emph{свободен для}~$\infr{x}$ \emph{в}~${\infr{A}(\infr{x})}$)‚ если
никакое свободное вхождение~$\infr{x}$ в~${\infr{A}(\infr{x})}$ не входит в
область действия какого\nobreakdash-нибудь квантора~${\forall\infr{y}}$
или~${\exists\infr{y}}$, где $\infr{y}$~---~переменная из~$\infr{t}$ (т.~е.
входящая в~$\infr{t}$).
%%
%% исправлено выделение буквы "в"
%% в соответствии с семантикой и выделением в англоязычном оригинале
%%

\begin{SCEnvWLabel}{Пример\kern1ex8.}{exmpl:p18-8}{exmpl:p18-8}
Термы~${\frml{d}}$,~${\frml{d}+0'}$~и~${\frml{a}\OLmult\frml{d}}$ свободны
для~$\frml{a}$ в первой и не свободны во второй из следующих формул:
\begin{equation}\label{eq:p18-I}\tag{I}
\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLand
\neg\frml{d}=0\text{,}\;\;\;\;\;\;\;
\exists\frml{d}\left(\frml{d}'+\frml{a}=\frml{b}\right)\OLand
\neg\frml{d}=0\text{.}
\end{equation}
\end{SCEnvWLabel}

Согласно этому определению, если $\infr{t}$~свободен для~$\infr{x}$
в~${\infr{A}(\infr{x})}$~---~и только в этом случае~---~при
подстановке~$\infr{t}$ вместо~$\infr{x}$ в~${\infr{A}(\infr{x})}$
терм~$\infr{t}$ не возникнет в~${\infr{A}(\infr{x})}$ ни на каком месте, где
какая\nobreakdash-нибудь (свободная) переменная~$\infr{y}$ из~$\infr{t}$ вошла
бы в качестве связанной переменной в результат~$\infr{A}(\infr{t})$.

\begin{SCEnvWLabel}{Пример\kern1ex8\kern1ex\textup{(окончание)}.}%
{exmpl:p18-8-end}{exmpl:p18-8-end}
Подстановка~${\frml{d}+0'}$ вместо~$\frml{a}$ в~\eqref{eq:p18-I} даёт
\begin{equation}\label{eq:p18-II}\tag{II}
\exists\frml{c}\left(\frml{c}'+\left(\frml{d}+0'\right)=\frml{b}\right)\OLand
\neg\frml{d}=0\text{,}\;\;\;\;\;\;\;
\exists\frml{d}\left(\frml{d}'+\left(\frml{d}+0'\right)=\frml{b}\right)\OLand
\neg\frml{d}=0
\end{equation}

\noindent%
соответственно. В первом случае введённое подстановкой вхождение~$\frml{d}$
из~${\frml{d}+0'}$ остаётся свободным во всей формуле, а во втором случае это не
имеет места.
\end{SCEnvWLabel}

Мы будем говорить, что подстановка~$\infr{t}$ вместо~$\infr{x}$
в~${\infr{A}(\infr{x})}$ \emph{свободна}, если $\infr{t}$~свободно
для~$\infr{x}$ в~${\infr{A}(\infr{x})}$. Уже при поверхностном взгляде на
указанную выше интерпретацию видно, что подстановка не годится, если она не
свободна.

%% ======================= Страница 76 =======================

Обе формулы в~\eqref{eq:p18-I} означают одно и то же, но в~\eqref{eq:p18-II} это
не так.

В качестве содержательного примера рассмотрим второе выражение
из~\eqref{eq:p18-A} или~\eqref{eq:p18-C}. Оно означает некоторую функцию от~$y$,
назовём её
\begin{equation}\label{eq:p18-G}\tag{G}
f(y)=\lim_{x\to 0} f(x,y)=\lim_{z\to 0} f(z,y)\text{.}
\end{equation}

Значение~${f(y)}$ для~${y=z}$ правильно записывается в виде
\begin{equation}\label{eq:p18-H}\tag{H}
f(z)=\lim_{x\to 0} f(x,z)\text{,}
\end{equation}

\noindent%
но не в виде~${f(z)=\displaystyle{\lim_{z\to 0} f(z,z)}}$.

\begin{SCEnvWLabel}{Пример\kern1ex9.}{exmpl:p18-9}{exmpl:p18-9}
Для иллюстрации обращения с терминологией и обозначениями, введёнными в этом
параграфе, предположим, что $\infr{x}$~---~переменная (т.~е.
<<$\infr{x}$>>~обозначает переменную), ${\infr{A}(\infr{x})}$~---~формула (т.~е.
<<${\infr{A}(\infr{x})}$>> обозначает формулу), а $\infr{b}$~есть (т.~е.
<<$\infr{b}$>>~обозначает \ldots) такая переменная, что
(i)\itemlabel{listItem:p18-list1-i}{(i)}~$\infr{b}$~свободна для~$\infr{x}$
в~${\infr{A}(\infr{x})}$ и
(ii)\itemlabel{listItem:p18-list1-ii}{(ii)}~$\infr{b}$~не входит свободно
в~${\infr{A}(\infr{x})}$ (или $\infr{b}$~есть~$\infr{x}$). Согласно нашим
обозначениям для подстановки, поскольку обозначение~${\infr{A}(\infr{x})}$ было
введено для~<<$\infr{x}$>>~и~<<${\infr{A}(\infr{x})}$>>,
(iii)\itemlabel{listItem:p18-list1-iii}{(iii)}~${\infr{A}(\infr{b})}$~есть (по
определению) результат подстановки~$\infr{b}$ вместо (свободных
вхождений)~$\infr{x}$ в~${\infr{A}(\infr{x})}$. В
силу~\ref{listItem:p18-list1-i}, вхождения~$\infr{b}$ в~${\infr{A}(\infr{b})}$,
введённые этой подстановкой, являются свободными. В
силу~\ref{listItem:p18-list1-ii}, других свободных вхождений~$\infr{b}$
в~${\infr{A}(\infr{b})}$~нет. Итак, свободные вхождения~$\infr{b}$
в~${\infr{A}(\infr{b})}$~---~это в точности вхождения, введённые этой
подстановкой. Поэтому (обратно
к~\ref{listItem:p18-list1-i}--\ref{listItem:p18-list1-iii})
(iv)\itemlabel{listItem:p18-list1-iv}{(iv)}~$\infr{x}$~свободно для~$\infr{b}$
в~${\infr{A}(\infr{b})}$,
(v)\itemlabel{listItem:p18-list1-v}{(v)}~$\infr{x}$~не входит свободно
в~${\infr{A}(\infr{b})}$ (или $\infr{x}$~есть~$\infr{b}$), и, кроме того,
(vi)\itemlabel{listItem:p18-list1-vi}{(vi)}~${\infr{A}(\infr{x})}$~является
результатом подстановки~$\infr{x}$ вместо (свободных вхождений)~$\infr{b}$
в~${\infr{A}(\infr{b})}$. Например,
\begin{equation*}
\infr{x},\;\;\;\;\;\infr{A}(\infr{x}),\;\;\;\;\;
\infr{b},\;\;\;\;\;\infr{A}(\infr{b})
\end{equation*}

\noindent%
могут быть соответственно
\begin{equation*}
\frml{c},\;\;\;\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl
\neg\frml{a}=\frml{b}+\frml{c},\;\;\;
\frml{d},\;\;\;\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl
\neg\frml{a}=\frml{b}+\frml{d}
\end{equation*}
\end{SCEnvWLabel}

\section{Правила преобразования}
\label{sec:19-transformation_rules}
%
% TODO: отсюда и далее стоило бы выработать некоторую гибкую систему переноса
% формул, не уместившихся в строку. Текущее разбиение слишком жёсткое и
% сохранится даже при достаточном увеличении ширины страницы.
%

В этом параграфе мы введём дальнейшие метаматематические определения (называемые
\emph{дедуктивными правилами}, или \emph{правилами преобразования}), которые
превращают формальную систему в дедуктивную теорию. Чтобы подчеркнуть аналогию с
содержательной теорией, мы начнём с перечня <<постулатов>>; однако для
метаматематики они являются не постулатами в смысле допущений, каковыми они
действительно не могут быть, поскольку официально они не имеют смысла, а только
формулами и формами (или схемами), к которым мы будем прибегать, давая
определения.

Прежде чем приводить этот перечень постулатов, мы рассмотрим типы постулатов,
которые в нём встречаются. Простейший тип есть ,,аксиома``~---~примером этого
типа служит <<${\neg\frml{a}'=0}$>>. Это~---~формула нашей формальной системы.
Затем имеется ,,форма аксиом`` или ,,схема аксиом``, примером которой
служит~<<${\infr{B}\OLimpl\infr{A}\vee\infr{B}}$>>. Это~---~метаматематическое
выражение, которое даёт конкретную аксиому каждый раз, когда выбраны формулы,
представляемые метаматематическими буквами~<<$\infr{A}$>>~и~<<$\infr{B}$>>.
Например, если $\infr{A}$~есть~${\frml{a}'=0}$‚ а
$\infr{B}$~есть~${\neg\frml{a}'=0}$‚ получаем
аксиому~${\neg\frml{a}'=0\OLimpl\frml{a}'=0\vee\neg\frml{a}'=0}$. Таким образом,
эта схема аксиом является метаматематическим методом для описания бесконечного
класса аксиом, имеющих общую форму.

Нам нужны также постулаты другого рода, формализующие операции вывода дальнейших
теорем из аксиом. Это~---~,,правила вывода``, например:
\begin{equation*}
\frac{\infr{A},\infr{A}\OLimpl\infr{B}}{\infr{B}}\text{.}
\end{equation*}

%% ======================= Страница 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}

\section{Формальный вывод}
\label{sec:20-formal_deduction}

stub

\section{Теорема о дедукции}
\label{sec:21-the_deduction_theorem}

stub

\section{Теорема о дедукции (окончание)}
\label{sec:22-the_deduction_theorem_concluded}

stub

\section{Введение и удаление логических символов}
\label{sec:23-introduction_and_elimination_of_logical_symbols}

stub

\section{Зависимость формул и варьирование переменных}
\label{sec:24-dependence_and_variation}

stub

\chapter{Исчисление высказываний}
\label{chap:vi-the_propositional_calculus}

\section{Формулы исчисления высказываний}
\label{sec:25-proposition_letter_formulas}

stub

\section{Эквивалентность, замена}
\label{sec:26-equivalence_replacement}

stub

\section{Эквивалентности, двойственность}
\label{sec:27-equivalences_duality}

stub

\begin{SCEnvWLabel}{Замечание\kern1ex1.}{remark:p27-1}{1}
Таким образом, в формальной системе \ldots
\end{SCEnvWLabel}

stub

\section{Оценка, непротиворечивость}
\label{sec:28-valuation_consistency_vi}

stub

\section{Полнота, нормальная форма}
\label{sec:29-completness_normal_form}

stub

\itemlabel{secdbl:interpretation-0}{соответствующем пункте, посвящённом интерпретации (читатель заметит его по заголовку)}%
\section{Разрешающая процедура, интерпретация}%
\label{sec:30-decision_procedure_interpretation}


stub

\chapter{Исчисление предикатов}
\label{chap:vii-the_predicate_calculus}

\section{Предикатные формулы}
\label{sec:31-predicate_letter_formulas}

stub

\section{Выводимые правила, свободные переменные}
\label{sec:32-derived_rules_free_variables}

stub

\section{Замена}
\label{sec:33-replacement}

stub

\section{Подстановка}
\label{sec:34-substitution}

stub

\section{Эквивалентности, двойственность, предварённая форма}
\label{sec:35-equivalences_duality_prenex_form}

stub

\section{Оценка, непротиворечивость}
\label{sec:36-valuation_consistency_vii}

stub

\section{Теоретико-множественная логика предикатов, \texorpdfstring{\lowercase{$k$}}{k}-образы}
\label{sec:37-set-theoretic_predicate_logic_k_transforms}

stub

\begin{SCEnvWLabel}{Исчисление предикатов с постулированным правилом %
подстановки.}{spar:p37-predicate_calculus_with_a_postulated_substitution_rule}%
{spar:p37-predicate_calculus_with_a_postulated_substitution_rule}
Также, как исчисление
высказываний~(\textsection~\ref{sec:30-decision_procedure_interpretation}),
исчисление предикатов обычно \ldots
\end{SCEnvWLabel}

stub

\chapter{Формальная арифметика}
\label{chap:viii-formal_number_theory}

\section{Индукция, равенства, замена}
\label{sec:38-induction_equality_replacement}

stub

\section{Сложение, умножение, порядок}
\label{sec:39-addition_multiplication_order}

stub

\section{Дальнейшее построение арифметики}
\label{sec:40-the_further_development_of_number_theory}

stub

\section{Формализованные вычисления}
\label{sec:41-formal_calculations}

stub

\section{Теорема Гёделя}
\label{sec:42-goedel_s_theorem}

stub