|
|
@@ -1,17 +1,280 @@
|
|
|
\part{Математическая логика}
|
|
|
\label{part:II-mathematical_logic}
|
|
|
|
|
|
+%% ======================= Страница 67 =======================
|
|
|
+
|
|
|
\chapter{Формальная система}
|
|
|
\label{chap:iv-a_formal_system}
|
|
|
|
|
|
\section{Формальные символы}
|
|
|
\label{sec:16-formal_symbols}
|
|
|
|
|
|
-stub
|
|
|
-
|
|
|
-\section{Правила преобразования}
|
|
|
+Введём теперь некоторую конкретную формальную систему. Система, описываемая в
|
|
|
+этой главе, явится предметом рассмотрения в четырёх последующих главах и в части
|
|
|
+дальнейших глав. Эта система представляет собой формализацию некоторой части
|
|
|
+классической элементарной теории чисел и включает необходимую для этого логику.
|
|
|
+
|
|
|
+При построении системы мы использовали следующие работы: Гильберт и
|
|
|
+Аккерман~\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{Свободные и связанные переменные}
|
|
|
@@ -83,9 +346,11 @@ stub
|
|
|
|
|
|
stub
|
|
|
|
|
|
-\section{Разрешающая процедура, интерпретация}
|
|
|
+\itemlabel{secdbl:interpretation-0}{соответствующем пункте, посвящённом интерпретации (читатель заметит его по заголовку)}%
|
|
|
+\section{Разрешающая процедура, интерпретация}%
|
|
|
\label{sec:30-decision_procedure_interpretation}
|
|
|
|
|
|
+
|
|
|
stub
|
|
|
|
|
|
\chapter{Исчисление предикатов}
|
