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}, формулой
является
%{\renewcommand{\theequation}{\Alph{equation}}%
\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 =======================

\end{SCEnvWLabel}






stub

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

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