par 15, chapter 3, part 1 + deep revision of the bibliography

Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex

@@ -19,6 +19,8 @@
 \input{parts/part3-recursive_functions.tex}
 \input{parts/part4-mathematical_logic_additional_topics.tex}
 
+\nocite{bernays2020,hilbert2020,langford2020,quine2020,russell2020,veblen2020}
+
 \appendix
 \input{parts/translator_s_appendixes.tex}
 

bookvvmrus.bbx

@@ -24,93 +24,95 @@
 \newbibmacro*{finentry}{\finentry}
 
 \DeclareBibliographyDriver{article}{%
-  \usebibmacro{bibindex}%
-  \usebibmacro{begentry}%
-  \usebibmacro{author}\\*%
-  \printfield{labelyear}%
-  \ifkeyword{addedByTranslator}{\textdegree}{}.\space%
-  \setunit{\printdelim{nametitledelim}}\newblock
-  \usebibmacro{title}%
-  \newunit
-  \printlist{language}%
-  \newunit\newblock
-  \usebibmacro{byauthor}%
-  \newunit\newblock
-  \usebibmacro{bytranslator+others}%
-  \newunit\newblock
-  \printfield{version}%
-  \newunit\newblock
-  \usebibmacro{journal+issuetitle}%
-  \newunit
-  \usebibmacro{byeditor+others}%
-  \newunit
-  \usebibmacro{note+pages}%
-  \newunit\newblock
-  \iftoggle{bbx:isbn}
-    {\printfield{issn}}
-    {}%
-  \newunit\newblock
-  \usebibmacro{doi+eprint+url}%
-  \newunit\newblock
-  \usebibmacro{addendum}%
-  \setunit{\bibpagerefpunct}\newblock
-  \usebibmacro{pageref}%
-  \newunit\newblock
-  \iftoggle{bbx:related}
-    {\usebibmacro{related:init}%
-     \usebibmacro{related}}
-    {}%
-  \usebibmacro{finentry}}
+    \usebibmacro{bibindex}%
+    \usebibmacro{begentry}%
+    \usebibmacro{author}%
+    \printfield{labelyear}%
+    \ifkeyword{addedByTranslator}{\textdegree}{}%
+    \ifkeyword{addedByReTyper}{\textsuperscript{rt}}{}.\kern1ex%
+%    \setunit{\printdelim{nametitledelim}}\newblock
+    \usebibmacro{title}%
+    \newunit
+    \printlist{language}%
+    \newunit\newblock
+    \usebibmacro{byauthor}%
+    \newunit\newblock
+    \usebibmacro{bytranslator+others}%
+    \newunit\newblock
+    \printfield{version}%
+    \newunit\newblock
+    \usebibmacro{journal+issuetitle}%
+    \newunit
+    \usebibmacro{byeditor+others}%
+    \newunit
+    \usebibmacro{note+pages}%
+    \newunit\newblock
+    \iftoggle{bbx:isbn}
+        {\printfield{issn}}
+        {}%
+    \newunit\newblock
+    \usebibmacro{doi+eprint+url}%
+    \newunit\newblock
+    \usebibmacro{addendum}%
+    \setunit{\bibpagerefpunct}\newblock
+    \usebibmacro{pageref}%
+    \newunit\newblock
+    \iftoggle{bbx:related}
+        {\usebibmacro{related:init}%
+         \usebibmacro{related}}
+        {}%
+    \usebibmacro{finentry}}
 
 \DeclareBibliographyDriver{book}{%
-  \usebibmacro{bibindex}%
-  \usebibmacro{begentry}%
-  \usebibmacro{author}\\%
-  \printfield{labelyear}%
-  \ifkeyword{addedByTranslator}{\textdegree}{}.\space%
-  \setunit{}\newblock
-  \usebibmacro{maintitle+title}%
-  \newunit
-  \printlist{language}%
-  \newunit\newblock
-  \usebibmacro{byauthor}%
-  \newunit\newblock
-  \usebibmacro{byeditor+others}%
-  \newunit\newblock
-  \printfield{edition}%
-  \newunit
-  \iffieldundef{maintitle}
-    {\printfield{volume}%
-     \printfield{part}}
-    {}%
-  \newunit
-  \printfield{volumes}%
-  \newunit\newblock
-  \usebibmacro{series+number}%
-  \newunit\newblock
-  \printfield{note}%
-  \newunit\newblock
-  \usebibmacro{publisher+location+date}%
-  \newunit\newblock
-  \usebibmacro{chapter+pages}%
-  \newunit
-  \printfield{pagetotal}%
-  \newunit\newblock
-  \iftoggle{bbx:isbn}
-    {\printfield{isbn}}
-    {}%
-  \newunit\newblock
-  \usebibmacro{doi+eprint+url}%
-  \newunit\newblock
-  \usebibmacro{addendum}%
-  \setunit{\bibpagerefpunct}\newblock
-  \usebibmacro{pageref}%
-  \newunit\newblock
-  \iftoggle{bbx:related}
-    {\usebibmacro{related:init}%
-     \usebibmacro{related}}
-    {}%
-  \usebibmacro{finentry}}
+    \usebibmacro{bibindex}%
+    \usebibmacro{begentry}%
+    \usebibmacro{author}%
+    \printfield{labelyear}%
+    \ifkeyword{addedByTranslator}{\textdegree}{}%
+    \ifkeyword{addedByReTyper}{\textsuperscript{rt}}{}.\kern1ex%
+%    \setunit{}\newblock
+    \usebibmacro{maintitle+title}%
+    \newunit
+    \printlist{language}%
+    \newunit\newblock
+    \usebibmacro{byauthor}%
+    \newunit\newblock
+    \usebibmacro{byeditor+others}%
+    \newunit\newblock
+    \printfield{edition}%
+    \newunit
+    \iffieldundef{maintitle}
+        {\printfield{volume}%
+            \printfield{part}}
+        {}%
+    \newunit
+    \printfield{volumes}%
+    \newunit\newblock
+    \usebibmacro{series+number}%
+    \newunit\newblock
+    \printfield{note}%
+    \newunit\newblock
+    \usebibmacro{publisher+location+date}%
+    \newunit\newblock
+    \usebibmacro{chapter+pages}%
+    \newunit
+    \printfield{pagetotal}%
+    \newunit\newblock
+    \iftoggle{bbx:isbn}
+        {\printfield{isbn}}
+        {}%
+    \newunit\newblock
+    \usebibmacro{doi+eprint+url}%
+    \newunit\newblock
+    \usebibmacro{addendum}%
+    \setunit{\bibpagerefpunct}\newblock
+    \usebibmacro{pageref}%
+    \newunit\newblock
+    \iftoggle{bbx:related}
+        {\usebibmacro{related:init}%
+            \usebibmacro{related}}
+        {}%
+    \usebibmacro{finentry}}
 
 \DeclareBibliographyDriver{booklet}{%
   \usebibmacro{bibindex}%
@@ -1012,9 +1014,7 @@
     \newunit\newblock}
 
 \renewbibmacro*{author}{%
-    \ifboolexpr{
-        test \ifuseauthor and not test {\ifnameundef{author}}
-    }
+    \ifkeyword{firstItemOfTheAuthor}%
         {%
             {\sparseFnt
                 \printnames{author}\space\printfield{nameaddon}%
@@ -1022,20 +1022,16 @@
                     {}
                     {\setunit{\addcomma\space}%
                         \usebibmacro{authorstrg}}%
-            }
+            }\par\nopagebreak
+            \hskip-\bibYearPointWidth
         }
-        {}%
+        {\hskip\bibItemFirstLineIndent}%
 }
 
 \renewbibmacro*{title}{%
-    \ifboolexpr{
-        test {\iffieldundef{title}} and test {\iffieldundef{subtitle}}
-    }
+    \ifboolexpr{test {\iffieldundef{title}} and test {\iffieldundef{subtitle}}}
         {}
-        {   \printfield[titlecase]{title}%
-            \setunit{\subtitlepunct}%
-            \printfield[titlecase]{subtitle}%}%
-            \newunit}%
+        {\printfield{title}\newunit}%
     \printfield{titleaddon}}
 
 %%==============================================================================

bookvvmrus.cbx

@@ -10,23 +10,25 @@
 \newbool{cbx:parens}
 
 \newbibmacro*{cite}{%
-  \iffieldundef{shorthand}
-    {\ifthenelse{\ifnameundef{labelname}\OR\iffieldundef{labelyear}}
-       {\usebibmacro{cite:label}%
-        \setunit{\printdelim{nonameyeardelim}}}
-       %{\printnames{labelname}%
-       {\printnames{labelyear}%
-        \setunit{\printdelim{nameyeardelim}}}%
-     \usebibmacro{cite:labelyear+extrayear}}
-    {\usebibmacro{cite:shorthand}}%
-    \ifkeyword{starred}{*}{}\ifkeyword{addedByTranslator}{\textdegree}{}}
+    \iffieldundef{shorthand}
+        {\ifthenelse{\ifnameundef{labelname}\OR\iffieldundef{labelyear}}
+            {\usebibmacro{cite:label}%
+                \setunit{\printdelim{nonameyeardelim}}}
+            %{\printnames{labelname}%
+            {\printnames{labelyear}%
+                \setunit{\printdelim{nameyeardelim}}}%
+            \usebibmacro{cite:labelyear+extrayear}}
+        {\usebibmacro{cite:shorthand}}%
+    \ifkeyword{starred}{*}{}\ifkeyword{addedByTranslator}{\textdegree}{}%
+    \ifkeyword{addedByReTyper}{\textsuperscript{rt}}{}}
 
 \newbibmacro*{citeyear}{%
-  \iffieldundef{shorthand}
-    {\iffieldundef{labelyear}
-       {\usebibmacro{cite:label}}
-       {\usebibmacro{cite:labelyear+extrayear}}}
-    {\usebibmacro{cite:shorthand}}}
+    \iffieldundef{shorthand}
+        {\iffieldundef{labelyear}
+            {\usebibmacro{cite:label}}
+            {\usebibmacro{cite:labelyear+extrayear}}}
+        {\usebibmacro{cite:shorthand}}%
+    \ifkeyword{starred}{*}{}\ifkeyword{addedByTranslator}{\textdegree}{}}
 
 \newbibmacro*{textcite}{%
   \ifnameundef{labelname}
@@ -101,11 +103,10 @@
      \printfield{postnote}\bibcloseparen}}
 
 \DeclareCiteCommand{\cite}
-  {\lbrack\usebibmacro{prenote}}%
-  {\usebibmacro{citeindex}%
-   \usebibmacro{cite}}
-  {\multicitedelim}
-  {\usebibmacro{postnote}\rbrack}
+    {\lbrack\usebibmacro{prenote}}%
+    {\usebibmacro{citeindex}\usebibmacro{cite}}
+    {\multicitedelim}
+    {\usebibmacro{postnote}\rbrack}
 
 \DeclareCiteCommand*{\cite}
   {\usebibmacro{prenote}}%
@@ -173,6 +174,10 @@
     \field{urldate}
     \literal{nodate}
 }
-
+\DeclareCiteCommand{\citeref}
+    {\usebibmacro{prenote}}
+    {\printtext[bibhyperref]{\printnames{labelname}}}
+    {\multicitedelim}
+    {\usebibmacro{postnote}}
 %%==============================================================================
 \endinput

bookvvmrus.cls

@@ -59,14 +59,14 @@
 \DeclareOption{leqno}{\input{leqno.clo}}
 \DeclareOption{fleqn}{\input{fleqn.clo}}
 \DeclareOption{openbib}{%
-  \AtEndOfPackage{%
-   \renewcommand\@openbib@code{%
-      \advance\leftmargin\bibindent
-      \itemindent -\bibindent
-      \listparindent \itemindent
-      \parsep \z@
-      }%
-   \renewcommand\newblock{\par}}%
+    \AtEndOfPackage{%
+        \renewcommand\@openbib@code{%
+            \advance\leftmargin\bibindent
+            \itemindent -\bibindent
+            \listparindent \itemindent
+            \parsep \z@
+        }%
+        \renewcommand\newblock{\par}}%
 }
 \ExecuteOptions{letterpaper,10pt,twoside,onecolumn,final,openright}
 \ProcessOptions

build_script

@@ -1,19 +1,19 @@
 #!/bin/bash
-mkdir -p build
-ln -s build/Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.log Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.log
-cp bibliography.bib build/
-cp index_style_and_order.xdy build/
-xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex'
-xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex'
+mkdir -p build && \
+ln -s build/Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.log Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.log 
+cp bibliography.bib build/ && \
+cp index_style_and_order.xdy build/ && \
+xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex' && \
+xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex' && \
 
-cd build
-makeindex 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.idx'
-xindy -C utf8 -M texindy -L russian -M index_style_and_order 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.idx'
-biber 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian'
-cd ..
-xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex'
-
-cd build
-biber 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian'
-cd ..
-xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex'
+cd build && \
+makeindex 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.idx' && \
+xindy -C utf8 -M texindy -L russian -M index_style_and_order 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.idx' && \
+biber 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian' && \
+cd .. && \
+xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex' && \
+cd build && \
+biber 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian' && \
+cd .. && \
+xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex' && \
+xelatex -interaction=nonstopmode -output-directory build 'Kleene_S.K.-Vvedenie_v_metamatematiku[1957y]-russian.tex'

definitions.tex

@@ -92,6 +92,13 @@
             sorting        = vvm,
             labeldateparts = true
             ]{biblatex}
+\renewcommand*{\bibfont}{\footnotesize}
+\newlength{\bibItemFirstLineIndent}
+\settowidth{\bibItemFirstLineIndent}{\bibfont7777.}
+\newlength{\bibYearPointWidth}
+\settowidth{\bibYearPointWidth}{\bibfont7777.\kern1ex}
+\setlength\bibhang{\bibItemFirstLineIndent}
+\addtolength{\bibhang}{\bibYearPointWidth}
 \addbibresource{bibliography.bib}
 %
 % оглавление

notation_defs.tex

@@ -52,6 +52,7 @@
 \newcommand{\OLsuccB}{\olNt{\boldsymbol{>}}{\boldsymbol{\succ}}}%
 \newcommand{\OLsucceqB}%
     {\olNt{\boldsymbol{\geqslant}}{\boldsymbol{\succcurlyeq}}}%
+\newcommand{\OLand}{\olNt{\&}{\wedge}}%              логическое И
 
 %
 % устаревшее обозначение кардинального числа (мощности множества)

parts/part1-the_problems_of_foundations.tex

@@ -3268,7 +3268,7 @@ ${a\text{\textsf{\#}}b}$~влечёт~${a\neq b}$. Но имеются пары
 геометрия. (Клейн~(1871) достиг той же цели другим методом, пользуясь плоской
 проективной геометрией с метрикой Кэли~(1859), а для этой последней можно
 построить модель в эвклидовой плоскости.~(См.~Юнг~\cite{young1911},
-лекции~II~и~III.)
+лекции~II~и~III).)
 %%
 %% исправлена опечатка в примечании
 %% удалена лишняя запятая в обороте "именно, оно даёт возможность наложить"
@@ -3538,7 +3538,8 @@ consistency (согласованность, совместность).~---~\tex
 метаматематика многим обязана логицистическим и интуиционистским исследованиям.)
 В дальнейших частях этой книги наша цель будет состоять не в вынесении
 окончательного решения, утверждающего или отвергающего формалистскую точку
-зрения в какой\nobreakdash-либо принятой версии, а в рассмотрении существа метаматематического метода и в изучении некоторых результатов, которые были
+зрения в какой\nobreakdash-либо принятой версии, а в рассмотрении существа
+метаматематического метода и в изучении некоторых результатов, которые были
 открыты на пути следования этому методу.
 
 \section{Формализация теории}
@@ -3546,9 +3547,333 @@ consistency (согласованность, совместность).~---~\tex
 
 Мы собираемся теперь заняться программой, которая превращает саму математическую
 теорию в объект точного математического изучения. В математической теории мы
-изучаем систему математических объектов. Как может математическая теория сама
-служить объектом математического изучения?
+изучаем систему математических объектов. Как
+%% ======================= Страница 59 =======================
+может математическая теория сама служить объектом математического изучения?
+
+Результат творчества математиков воплощается в предложениях~---~доказанных
+предложениях или теоремах данной математической теории. Невозможно в точных
+терминах изучить, что происходит в уме математика, но можно рассматривать
+систему этих предложений.
+
+Система этих предложений должна быть высказана полностью. Их нельзя всех
+выписать, но изучающему должны быть известны все условия, определяющие, какие
+предложения имеют место в теории.
+
+Прежде всего, предложения теории следует распределить, принимая во внимание их
+дедуктивные взаимоотношения; те предложения, из которых остальные логически
+выводимы, следует принять за аксиомы (или постулаты).
+
+Этот первый шаг будет выполнен только после того, как посредством аксиом будут
+выражены все свойства неопределяемых или технических терминов, существенные для
+вывода теорем. Тогда можно будет, производя выводы, рассматривать технические
+термины как слова, сами по себе не имеющие смысла. Ибо утверждение, что они
+имеют значения, необходимые для вывода теорем и отличные от тех, которые можно
+вывести из аксиом, регулирующих употребление этих терминов, сводится к
+утверждению, что не все их свойства, существенные для выводов, выражены
+посредством аксиом. После того как таким образом исключены из рассмотрения
+значения технических терминов, мы пришли к точке зрения формальной
+аксиоматики~(\textsection~\ref{sec:8-system_of_objects}).
+
+Технические термины всё ещё обладают грамматическими свойствами: они являются
+существительными, прилагательными, глаголами и~т.~д. Кроме того, остаются ещё
+обычные, или логические, термины, значения которых используются в выводах.
+Пункт, на котором формальная аксиоматизация должна остановиться, фактически не
+определён, потому что не существует никакой абсолютной основы для различения
+технических и обычных терминов.
+
+Во всяком случае, мы ещё не достигли нашей цели~---~высказать явно все условия,
+определяющие, какие предложения имеют место в теории. В самом деле, мы не
+установили, какими логическими принципами надлежит пользоваться при выводах. Как
+нам теперь хорошо известно, эти принципы различны для различных
+теорий~(\textsection~\ref{sec:13-intuitionism}).
+
+Чтобы выразить их явно, необходим второй шаг, который дополняет предыдущий для
+так называемых технических терминов по отношению к неграмматической стороне их
+значений. Все значения всех слов исключены из рассмотрения, и все условия,
+регулирующие употребление этих слов в теории, явно высказаны. Логические
+принципы, прежде входившие неявно через значение обычных терминов, теперь будут
+введены в действие~---~отчасти, может быть, при помощи новых аксиом, но во
+всяком случае, хотя бы частично, посредством правил, позволяющих вывести одну
+фразу из другой или других. Так как мы полностью абстрагировались от содержания
+или сущности, сохранив только форму, то мы будем говорить, что данная теория
+\emph{формализована}. Будучи формализованной, теория по своей структуре является
+уже не системой осмысленных предложений, а системой фраз, рассматриваемых как
+последовательность слов, которые, в свою очередь, являются последовательностями
+букв. Только по форме будем мы судить о том, какие сочетания слов являются
+фразами, какие фразы~---~аксиомами и когда фразы вытекают в качестве
+непосредственных следствий из других.
+
+Возможна ли такая формализация? В какой мере может быть формализована данная
+теория, это мы узнаем только после попытки формализации и изучения
+результатов~(например,~\textsection\textsection~%
+\ref{sec:29-completness_normal_form},~\ref{sec:42-goedel_s_theorem},~%
+\ref{sec:60-church_s_theorem_the_generalized_goedel_s_theorem},~%
+\ref{sec:72-goedel_s_completeness_theorem}).
+
+То, что для математических теорий формализация возможна, во всяком случае, в
+весьма значительной мере,~---~это открытие, полученное в итоге длительного
+периода истории развития человеческого интеллекта.
+
+%% ======================= Страница 60 =======================
+
+Открытие аксиоматико\nobreakdash-дедуктивного метода в математике, по
+древнегреческой традиции, приписывается Пифагору~(шестое столетие до~н.~э.); оно
+дошло до нас благодаря Эвклиду~(365?--275?~гг. до~н.~э.), <<Начала>> которого,
+говорят, были некогда самой распространённой книгой после Библии. Эвклид не
+сумел явно выразить все постулаты, которые требуются для вывода теорем. В новое
+время были обнаружены другие постулаты, например те, которые регулируют порядок
+точек на прямой~(Паш~\cite{pasch1882}).
+
+Открытие формального рассмотрения логики, т.~е. открытие того, что дедуктивные
+рассуждения можно описывать через форму их фраз, принадлежит, повидимому,
+Аристотелю~(384--322~гг. до~н.~э.). И здесь новое время внесло
+усовершенствования.
+
+При формализации математических теорий мы пользуемся обоими открытиями. Для
+строгого выполнения этой задачи практически необходимо заново построить
+рассматриваемую теорию в особом символическом языке, т.~е.
+\emph{символизировать} её. Вместо того, чтобы описанные выше шаги выполнять над
+теорией в том виде, как она дана нам в некотором обычном разговорном языке,
+например греческом или русском, мы построим новый символический язык специально
+с целью выразить в нём эту теорию. Обычные разговорные языки слишком
+обременительны, слишком нерегулярны по своему построению и слишком расплывчаты,
+чтобы мы могли им следовать. (В символическом языке символы будут обычно
+соответствовать целым словам, а не буквам, а последовательности символов,
+соответствующие фразам, будут называться <<формулами>>.)
+
+Этот новый язык будет носить тот общий характер символизма, с которым мы
+встречаемся в математике. В алгебре мы производим выводы как формальные
+манипуляции с уравнениями, которые чрезвычайно утомительно было бы производить в
+обычном языке, как это делалось до того, как Виет~(1591) и другие изобрели
+современные алгебраические обозначения. Открытие простых символических
+обозначений, которые сами приводят к манипуляциям по формальным правилам,
+явилось одним из путей, на которых развивалась мощь современной математики.
+Однако в обычной математической практике мы имеем дело только с частичной
+символизацией и формализацией, так как часть предложений остаётся выраженной
+словами и часть выводов производится в терминах значений слов, а не по
+формальным правилам.
+%%
+%% исправлена опечатка
+%% в оригинале "Виета"
+%%
 
+После того как Лейбниц~\cite{leibniz1666} пришёл к мысли об ,,универсальной
+характеристике``, в трудах де~Моргана~\cite{morgan1847,morgan1864},
+Буля~\cite{boole1847,boole1854}, Пирса~\cite{peirce1867,peirce1880},
+Шрёдера~\cite{schroeder1877,schroeder1890-1905} и других для формальной логики
+также был получен символический способ обращения с помощью математической
+техники.
+
+Эти совпадающие по духу исследования в конечном счёте привели к строгим
+формализациям различных разделов математики~---~Фреге\cite{frege1893,frege1903},
+Пеано~\cite{peano1894-1908} и
+Уайтхед и Рассел~\cite{whitehead_and_russell1910-1913}. (Описанный метод явного
+изложения теории часто называется \emph{логистическим} методом.)
+
+Гильберту принадлежит, во\nobreakdash-первых, подчёркивание того, что строгая
+формализация теории предполагает полную абстракцию от смысла~---~результат такой
+формализации называется \emph{формальной системой}, или
+\emph{формализмом}\footnote{Не путать с формализмом как направлением в философии
+математики.~---~\textit{Прим.~ред.}} (или иногда \emph{формальной теорией}, или
+\emph{формальной математикой}); во\nobreakdash-вторых, ему принадлежит метод,
+делающий формальную систему в целом предметом изучения математической
+дисциплины, называемой \emph{метаматематикой} или \emph{теорией доказательств}.
+
+Метаматематика содержит в себе описание или определение формальных систем, а
+также исследование свойств формальных систем. При рассмотрении конкретной
+формальной системы мы будем называть эту систему \emph{предметной теорией}, а
+относящуюся к ней метаматематику~---~её \emph{метатеорией}.
+
+%% ======================= Страница 61 =======================
+
+С точки зрения метатеории, предметная теория является вовсе не теорией в прежнем
+смысле этого слова, а системой бессодержательных предметов, аналогичных позициям
+в шахматной игре, над которыми проделываются механические манипуляции,
+аналогичные шахматным ходам. Предметная теория описывается и изучается как
+система символов и предметов, построенных из символов. Символы рассматриваются
+просто как типы распознаваемых объектов\footnote{Т.~е. таких объектов, любые два
+из которых могут быть распознаны либо как одинаковые, либо как
+различные.~---~\textit{Прим.~ред.}}. Для определённости мы можем представлять
+себе их конкретно как знаки на бумаге, или, точнее, как абстракции от нашего
+обращения со знаками на бумаге. (Теория доказательств должна быть в известной
+мере абстрактна, потому что она предполагает выполнимыми построения произвольно
+длинных последовательностей символов, хотя количество бумаги и чернил во всем
+мире ограничено.) Остальные предметы системы рассматриваются только в связи со
+способом их построения из символов\footnote{См.~об этом у
+{\renewcommand*{\multicitedelim}{~или~}%
+А.~А.~Маркова~%
+\brackettext{\cites*[с~(пп.~5--15)]{markov1951}[(гл.~I)]{markov1954}}}.%
+~---~\textit{Прим.~ред.}}. По определению, этим
+исчерпывается роль формальной системы как предмета изучения метаматематики.
+
+Метатеория принадлежит интуитивной, неформальной математике (если только
+метатеория не формализуется, в свою очередь, в некоторой метаметатеории, чего мы
+здесь рассматривать не будем). Метатеория будет выражаться на обычном языке с
+математическими символами, например метаматематическими переменными, вводимыми
+по мере надобности. Утверждения метатеории должны быть понимаемы. Её выводы
+должны убеждать. Они должны состоять в интуитивных умозаключениях‚ а не в
+применении установленных правил, как выводы в формальной теории. Чтобы
+формализовать предметную теорию, были установлены правила, но теперь без всяких
+правил мы должны понимать, как эти правила действуют. Интуитивная математика
+необходима даже для определения формальной.
+
+(Мы будем понимать это в том смысле, что для обоснования метаматематического
+умозаключения приходится обращаться в конечном счёте к смыслу и очевидности, а
+не к какому\nobreakdash-либо множеству условно принятых правил. На практике это
+не помешает нам систематизировать наши метаматематические результаты как теоремы
+или правила, которые можно будет затем применять квазиформально для сокращения
+содержательных рассуждений. Это~---~обычный процесс в содержательной математике.
+Иногда мы будем ссылаться даже на формально установленные принципы
+(интуиционистской) логики, причём формальные выводы этих принципов будут
+указывать метод, посредством которого рассуждение может быть проведено
+содержательно.)
+
+В метатеории мы будем применять только те методы, которые формалисты
+называют \emph{финитными}~(finitary) и которые используют только интуитивно
+представляемые предметы и осуществимые процессы. (Мы переводим немецкое
+<<finit>> словом <<финитный>>\footnote{В
+подлиннике~---~<<finitary>>.~---~\textit{Прим.~ред.}}; русское
+<<конечный>>\footnote{В
+подлиннике~---~английское <<finite>>.~---~\textit{Прим.~ред.}} соответствует
+немецкому <<endlich>>.) Мы никогда не будем рассматривать бесконечный класс как
+завершённое целое. Каждое доказательство существования будет давать, хотя бы
+неявно, метод для построения предмета, существование которого
+доказывается~(ср.~\textsection~\ref{sec:13-intuitionism})\footnote{
+\itemlabel{footnote:p15-1}{предыдущее подстрочное примечание} Такая точка
+зрения не является единственно возможной. Метаматематику (теорию доказательств)
+можно рассматривать и как содержательную математическую дисциплину (подобную,
+например, алгебре или топологии), на методы которой не налагается никаких
+специфических ограничений (см.~по этому поводу~\ref{par:p15-starred}).~%
+---~\textit{Прим.~ред.}}.
+%%
+%% в сноске исправлена некорректная ссылка (зависящая от представления)
+%% в оригинале вместо
+%% "см.~по этому поводу~\ref{par:p15-starred}"
+%% было
+%% "см. по этому поводу четвёртый абзац следующей страницы"
+%%
 
+Это ограничение требуется для той цели, с которой Гильберт ввёл метаматематику.
+Предложения данной математической теории могут не иметь ясного смысла, а её
+умозаключения могут не иметь в себе несомненной очевидности.
+%% ======================= Страница 62 =======================
+Формализация сводит развитие теории к форме и правилу. Она устраняет всякую
+неопределённость в отношении того, чт{\'o} такое предложение теории или чт{\'o}
+такое доказательство в ней. И вопрос о том, не приводят ли к противоречию те
+методы, которые были формализованы, а также другие вопросы о действии этих
+методов должны изучаться в метатеории посредством методов, не подверженных тем
+же сомнениям, что и методы первоначальной теории.
+
+Финитные методы имеют ту же природу, что и методы интуиционистской элементарной
+арифметики. Некоторые формалисты пытаются ограничить их ещё
+{\'y}же~(Гильберт и Бернайс~\cite[стр.~43]{hilbert_and_bernays1934} и
+Бернайс~\cite{bernays1935,bernays1938}).
+
+Рассмотрение последнего обстоятельства мы отложим
+до~\textsection~\ref{sec:81-reduction_of_classical_to_intuitionistic_systems}.
+Чтобы защитить классическую математику от интуиционистов‚ нет надобности
+стремиться пользоваться меньшим, чем они разрешают. Но естественно
+придерживаться строго элементарных методов до тех пор, пока они достаточны. Все
+приведённые в~\textsection~\ref{sec:13-intuitionism} примеры интуиционистских
+арифметических рассуждений мы будем считать финитными. Мы увидим, что вплоть до
+одной отдалённой стадии наших метаматематических исследований будет достаточно
+интуиционистских методов совсем элементарного рода. Окончательным критерием
+допустимости некоторого метода в метаматематике должна быть, конечно, его
+интуитивная убедительность.
+
+(*)\itemlabel{par:p15-starred}{абзац, помеченный звездочкой~(*)} (Некоторые
+авторы пользуются приставкой <<мета>> для обозначения языка или теории‚ в
+которой другой язык или теория делаются предметом изучения, не ограниченного
+финитными методами. В этой связи в противовес
+<<предметному языку>>~(<<object language>>) употребляется также
+термин <<синтаксис>>~(<<syntax language>>).~Ср.~Карнап~\cite{carnap1934};
+ср.~также~\textsection~\ref{sec:37-set-theoretic_predicate_logic_k_transforms}.
+В этой книге мы пользуемся приставкой <<мета>> только тогда, когда методы
+финитны.)
+%%
+%% исправлена опечатка
+%% в оригинале было
+%% "употребляется также термин <<синтаксис <<syntax language>>)."
+%%
 
-stub
+Формальные системы, изучаемые в метаматематике, выбираются (обычно) так, что они
+служат моделями для частей содержательной математики и логики, с которыми мы уже
+более или менее знакомы, и получаются из этих частей путём формализации.
+Значения, которые связываются с символами, формулами и другими объектами данной
+формальной системы при рассмотрении её как формализации содержательной теории,
+мы будем называть (\emph{подразумеваемой}) \emph{интерпретацией} этой системы
+(или её символов, формул и~т.~п.). Другими словами, интерпретации символов,
+формул и~т.~п.~---~это предметы, предложения и~т.~п. содержательной теории,
+сопоставленные с ними посредством того метода, в силу которого система образует
+модель содержательной теории.
+
+В случае формулы, представляющей идеальное предложение классической
+математики~(\textsection~\ref{sec:14-formalism}), интерпретация не может быть
+совершенно интуитивной (или финитной), а должна состоять в чем\nobreakdash-либо
+таком, что классически настроенный математик мыслит в терминах неформального
+(или не строго формализованного) построения классической математики, т.~е.
+построения, возникшего исторически и общепринятого всюду, где процесс не
+формализуется сознательно в строгом смысле теории доказательств.
+
+Интерпретация побуждает метаматематика выбрать ту или иную формальную систему,
+которая вводится посредством определений. Она руководит им при выборе
+относящихся к этой системе проблем, которыми он будет заниматься. Она может даже
+доставить ему ключи, существенные для решения этих проблем. Только в
+окончательных формулировках и доказательствах он (как метаматематик) должен
+отказаться от пользования интерпретацией.
+
+Насколько стеснительно это ограничение? Метаматематика должна изучать формальную
+систему как систему символов и~т.~п., которые рассматриваются совершенно
+объективно. Это означает попросту, что символы и~т.~п. сами по себе являются
+окончательными предметами и не должны использоваться для обозначения
+чего\nobreakdash-либо отличного от них самих. Метаматематик смотрит на них, а не
+через них и не на то, что за ними; таким образом, они являются предметами без
+интерпретации или значения.
+
+%% ======================= Страница 63 =======================
+
+Изучая эти предметы, метаматематика должна пользоваться своими собственными
+методами и орудиями. Последние можно выбирать как угодно, лишь бы они были
+финитны. Например, метаматематика может финитным способом употреблять
+натуральные числа. Если речь идёт о формулах, допускающих (за пределами
+метаматематики) финитную интерпретацию, то можно внутри метаматематики
+определить свойства таких формальных объектов, которые (с точки зрения, внешней
+по отношению к метаматематике) эквивалентны интерпретациям этих формул. Таким
+образом, финитные интерпретации можно протащить через чёрный ход. Но
+метаматематика никоим образом не может иметь дело с нефинитными интерпретациями
+идеальных предложений классической математики.%
+\footnote{См.~\ref{footnote:p15-1}.~---~\textit{Прим.~ред.}}
+
+Чтобы в дальнейшем всюду было ясно, почему мы интересуемся формальными
+системами, которые мы рассматриваем, и каким образом они представляют собой
+формализации тех разделов логики и математики, с которыми содержательно мы уже
+знакомы, мы в этой книге будем указывать возможные интерпретации и пользоваться
+естественной терминологией, например, выражением <<доказательство>> для
+формальных выводов и <<и>> как названием символа~$\OLand$. Это необходимо для
+полного достижения нашей цели, хотя интерпретация сама по себе чужда
+метаматематике.
+
+Подведём итоги. Если рассматривать картину полностью, то имеются три отдельные и
+отличные друг от друга <<теории>>:
+(a)\itemlabel{listItem:p4-a}{(a)}~содержательная~(informal) теория,
+формализацией которой служит формальная система,
+(b)\itemlabel{listItem:p4-b}{(b)}~формальная система или предметная теория и
+(c)\itemlabel{listItem:p4-c}{(c)}~метатеория, в которой описывается и изучается
+эта формальная система.
+
+Здесь~\ref{listItem:p4-b}, являющаяся формальной, служит не теорией в обычном
+смысле, а системой символов и предметов, построенных из символов (описанных
+в~\ref{listItem:p4-c}), причём эта система является своего рода условным
+образом, или моделью, для~\ref{listItem:p4-a}. С другой стороны,
+\ref{listItem:p4-a}~и~\ref{listItem:p4-c}, являющиеся содержательными, не имеют
+точно определённой структуры, какую имеет~\ref{listItem:p4-b}.
+
+Далее, \ref{listItem:p4-c}~---~это теория, изучающая~\ref{listItem:p4-b}, и она
+должна применяться к~\ref{listItem:p4-b}, не взирая на~\ref{listItem:p4-a}, или,
+точнее, не взирая на интерпретацию~\ref{listItem:p4-b} в
+терминах~\ref{listItem:p4-a}.
+
+Кроме того, \ref{listItem:p4-c}~ограничена употреблением только финитных
+методов, тогда как для~\ref{listItem:p4-a}, вообще говоря, не имеется такого
+ограничения.