rt-g0_73c250c9-Kleene_VVM-russian/parts/part2-mathematical_logic.tex

\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{Переменные}:~${\mathit{a},\mathit{b},\mathit{c},\ldots}$.
\emph{Скобки}:~${(,)}$.

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

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

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

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

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

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

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

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

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

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

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

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

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

Сначала определим ,,терм``‚ который аналогичен существительному в грамматике.
Термы рассматриваемой системы все представляют натуральные числа, фиксированные
или переменные. Определение формулируется с помощью метаматематических
переменных <<$\mathrm{s}$>>~и~<<$\mathrm{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}~Если
$\mathrm{s}$~и~$\mathrm{t}$~---~\emph{термы}, то
${(\mathrm{s})+(\mathrm{t})}$‚ ${(\mathrm{s})\OLmult(\mathrm{t})}$ и
${(\mathrm{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$, $\mathit{a}$, $\mathit{b}$ и~$\mathit{c}$. Поэтому, в
силу~\ref{listItem:p17-list1-5}, ${(0)'}$~и~${(\mathit{c})'}$ являются термами.
Снова в силу~\ref{listItem:p17-list1-5}, ${\left((0)'\right)'}$~есть~терм, а в
силу~\ref{listItem:p17-list1-3},
${\left((\textit{c})'\right)+(\mathit{a})}$~есть терм.
\end{SCEnvWLabel}

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

1.\itemlabel{listItem:p17-list2-1}{1}~Если
$\mathrm{s}$~и~$\mathrm{t}$~---~термы, то
${(\mathrm{s})=(\mathrm{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}~Если
$\mathrm{A}$~и~$\mathrm{B}$~---~\emph{формулы}, то
${(\mathrm{A})\OLimpl(\mathrm{B})}$,
${(\mathrm{A})\OLand(\mathrm{B})}$,
${(\mathrm{A})\vee(\mathrm{B})}$ и
${\neg(\mathrm{A})}$~---~\emph{формулы}.
6--7.%
\itemlabel{listItem:p17-list2-6}{6}%
\itemlabel{listItem:p17-list2-7}{7}~Если $\mathrm{x}$~---~переменная, а
$\mathrm{A}$~---~\emph{формула}, то
${\forall\mathrm{x}(\mathrm{A})}$~и~%
${\exists\mathrm{x}(\mathrm{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} и уже полученные примеры термов, убеждаемся
в том, что ${(\mathit{a})=(\mathit{b})}$ и~%
${\left(\left(\left(\mathit{c}\right)'\right)+\left(\mathit{a}\right)\right)=%
  \left(\mathit{b}\right)}$~---~формулы. Поэтому, в
силу~\ref{listItem:p17-list2-5}~и~\ref{listItem:p17-list2-7},
${\neg\left(\left(\mathit{a}\right)=\left(\mathit{b}\right)\right)}$ и %
${\exists\mathit{c}%
\left(%
    \left(%
        \left(%
            \left(\mathit{c}\right)'%
        \right)+%
        \left(\mathit{a}\right)%
    \right)=%
    \left(\mathit{b}\right)%
\right)}$~---~формулы. Наконец, в силу~\ref{listItem:p17-list2-2}, формулой
является
\begin{equation}\label{eq:p17-A}\tag{A}
\left(
    \exists\mathit{c}
    \left(
        \left(
            \left(
                \left(\mathit{c}\right)'
            \right)+
            \left(\mathit{a}\right)
        \right)=
        \left(\mathit{b}\right)
    \right)
\right)\OLimpl
\left(
    \neg
    \left(
        \left(\mathit{a}\right)=\left(\mathit{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\mathrm{x},\;\;\;%
\exists\mathrm{x},\;\;\;=,\;\;\;+,\;\;\;\OLmult,\;\;\;'\text{,}
\end{equation}

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

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

\begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p17-3}{exmpl:p17-3}
В формуле~(\ref{eq:p17-A}) область действия первого вхождения оператора~$=$
состоит из
части~${\left(\left(\mathit{c}\right)'\right)+\left(\mathit{a}\right)}$ и
первого вхождения $\mathit{b}$, а область действия ${\exists\mathit{c}}$~есть
часть~${%
\left(
    \left(
        \left(\mathit{c}\right)'
    \right)+
    \left(\mathit{a}\right)
\right)=
\left(\mathit{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\mathrm{x}}$,~${\exists\mathrm{x}}$) \emph{или
непосредственно справа от правой скобки} (\emph{в случае}~$'$).

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

\begin{SCEnvWLabel}{Пример\kern1ex3~\textup{(окончание)}.}%
{exmpl:p17-3-end}{exmpl:p17-3-end}
Рассмотренный пример формулы~(\ref{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 скобок, входящих в полную
формулу~(\ref{eq:p17-A}), можно заметить, что область действия первого
вхождения~$=$ состоит из выражения, заключённого между
скобками~${\big(\vphantom{a}^{3}_{4}\;\:\big)\vphantom{a}^{10}_{4}}$, и
выражения, заключённого между
скобками~${\big(\vphantom{a}^{11}_{5}\;\:\big)\vphantom{a}^{12}_{5}}$. Это
согласуется с нашим прежним определением этой области действия. Аналогично,
область действия~${\exists\mathit{c}}$ заключена между
скобками~${\big(\vphantom{a}^{2}_{6}\;\:\big)\vphantom{a}^{13}_{6}}$.
\end{SCEnvWLabel}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


stub

\section{Правила преобразования}
\label{sec:19-transformation_rules}

stub




\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

\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

\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