par 18, chapter 4, part 2

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

@@ -1,6 +1,7 @@
 \documentclass[10pt,a5paper%,showframe
 ]{bookvvmrus}
 \input{definitions.tex}
+\input{notation_defs.tex}
 
 \title{Введение в метаматематику}
 \author{Стефен Коул Клини}

definitions.tex

@@ -118,7 +118,6 @@
 \addtolength{\TotlWoLongestSect}{\AsterixLen}%
 \addtolength{\TotlWoLongestSect}{\ParagrLen}%
 %===============================================================================
-\input{notation_defs.tex}
 %
 % окружение для примеров, теорем, лемм, доказательств и следствий
 %     Первый аргумент - заголовок
@@ -133,10 +132,6 @@
 %          }%
      \itemlabel{#2}{#3}\textsc{#1}\enskip}{\medskip}%
 %
-% технический макрос для учета старой и новой нотации
-%
-\newcommand{\olNt}[2]{\ifx\LaterNotation\undefined #1\else #2\fi}%
-%
 % технический макрос для переноса знака между строк
 %
 \newcommand*{\hm}[1]%

notation_defs.tex

@@ -4,7 +4,27 @@
 %     * для использования более поздней (современной) нотации расскомментируйте
 %       строку
 %
-%%%%% \def\LaterNotation{1}
+%% \def\LaterNotation{1}
+%
+% технический макрос для учета старой и новой нотации
+%
+\newcommand{\olNt}[2]{\ifx\LaterNotation\undefined #1\else #2\fi}%
+%
+% шрифты для формальных и содержательных переменных
+%
+\newcommand{\frml}[1]{%
+\ifthenelse{%
+\equal{A}{#1}\or\equal{B}{#1}\or\equal{C}{#1}\or\equal{D}{#1}\or%
+\equal{E}{#1}\or\equal{F}{#1}\or\equal{G}{#1}\or\equal{H}{#1}\or%
+\equal{I}{#1}\or\equal{J}{#1}\or\equal{K}{#1}\or\equal{L}{#1}\or%
+\equal{M}{#1}\or\equal{N}{#1}\or\equal{O}{#1}\or\equal{P}{#1}\or%
+\equal{Q}{#1}\or\equal{R}{#1}\or\equal{S}{#1}\or\equal{T}{#1}\or%
+\equal{U}{#1}\or\equal{V}{#1}\or\equal{W}{#1}\or\equal{X}{#1}\or%
+\equal{Y}{#1}\or\equal{Z}{#1}}%
+{\mathcal{#1}}{\mathit{#1}}}
+\olNt{\newcommand{\infr}[1]{\mathrm{#1}}}%
+     {\newcommand{\infr}[1]{\mathtt{#1}}}
+
 %
 % некоторые часто встречающиеся символы и обозначения
 %

parts/part1-the_problems_of_foundations.tex

@@ -753,7 +753,7 @@ P\OLcup\{a_{0},b_{0},a_{1},b_{1},\ldots\}\text{.}
 \label{sec:5-higher_transfinite_cardinals}
 
 %
-% TODO: для следующах двух абзацев рассмотреть возможность добавления ссылок
+% TODO: для следующих двух абзацев рассмотреть возможность добавления ссылок
 % к прописным ссылкам:
 % "в последнем примере"
 % "эту теорему"
@@ -827,7 +827,7 @@ $T$~принадлежит~$\setOfSets{S}$. Выберем тот элемент
 соотношение}~${\OLcard{M}<\OLcard{\OLpowerset{M}}}$ (теорема Кантора).
 \end{SCEnvWLabel}
 
-\begin{SCEnvWLabel}{Доказательство.}{theorem:p5-C-proof}{C-proof}
+\begin{SCEnvWLabel}{Доказательство.}{theorem:p5-C-proof}{p5-C-proof}
 Если $N_{1}$~---~совокупность единичных подмножеств множества~$M$‚
 то~${M\sim N_{1}\subset\OLpowerset{M}}$. Значит, по
 следствию~\ref{theorem:p4-A-corollary-A} из теоремы~\ref{theorem:p4-A},%
@@ -1748,7 +1748,7 @@ L3.\itemlabel{axiom:p8-l3}{L3}~Имеет место по крайней мер
 
 Эти определения мы привели для разъяснения нашей терминологии. Иногда
 термин <<арифметика>> употребляется и по отношению к теории операций
-$+$~и~$\cdot$ для несчётных систем чисел (например, ,,арифметика трансфинитных
+$+$~и~$\OLmult$ для несчётных систем чисел (например, ,,арифметика трансфинитных
 кардинальных чисел``).
 
 В то время как арифметика, или теория чисел, изучает системы
@@ -3439,7 +3439,7 @@ consistency (согласованность, совместность).~---~\tex
 содействует изучению <<техники нашего мышления>>.~См.~{\sparseFnt Гильберт},
 Основания геометрии, М.,~1948, стр.~382--383.~---~\textit{Прим.~перев.}}.
 
-Согласно Брауэру~\cite{brouwer1928} и 
+Согласно Брауэру~\cite{brouwer1928} и
 Гейтингу~\cite{heyting1931-1932,heyting1934}, возможно соглашение между
 интуиционизмом и формализмом при условии (по Нейману~\cite{neumann1931-1932})‚
 что формалисты не станут приписывать неинтуиционистской классической математике

parts/part2-mathematical_logic.tex

@@ -51,7 +51,7 @@ $\neg$~(не), $\forall$~(для всех), $\exists$~(существует). \e
 предикатов}:~$=$~(равняется). \emph{Символы функций}:~$+$~(плюс),
 $\OLmult$~(умножить на), $'$~(следующее за).
 \emph{Индивидуальные символы}:~$0$~(нуль).
-\emph{Переменные}:~${\mathit{a},\mathit{b},\mathit{c},\ldots}$.
+\emph{Переменные}:~${\frml{a},\frml{b},\frml{c},\ldots}$.
 \emph{Скобки}:~${(,)}$.
 
 Слова, указанные в скобках, могут применяться при чтении этих символов и
@@ -84,17 +84,16 @@ $\OLmult$~(умножить на), $'$~(следующее за).
 выражения, состоящие из единственного (вхождения) формального символа. Если не
 оговорено противное, пустая последовательность (не имеющая членов) не будет
 рассматриваться как формальное выражение. Например,
-$0$,~${(\mathit{a})+(\mathit{b})}$‚ ${(\mathit{a})=(0)}$
-и~${((0\forall 00=}$~являются формальными выражениями. Последнее из них состоит
-из семи (вхождений) символов, т.~е. имеет семь членов; третье, пятое и шестое
-вхождения символов в это формальное выражение являются каждое вхождением~$0$;
-различные входящие в него символы~---~это~$($,~$0$,~$\forall$‚~$=$. Формальные
-выражения структурно аналогичны словам языка, но при интерпретации некоторые из
-них соответствуют целым предложениям, например~${(\mathit{a})=(0)}$‚ а другие не
-имеют смысла, например~${((0\forall 00=}$. Здесь снова наша терминология
-указывает на то обстоятельство, что для формальной системы как таковой выражения
-ничего не выражают, а являются только некоторыми распознаваемыми и различимыми
-объектами.
+$0$,~${(\frml{a})+(\frml{b})}$‚ ${(\frml{a})=(0)}$ и~${((0\forall 00=}$~являются
+формальными выражениями. Последнее из них состоит из семи (вхождений) символов,
+т.~е. имеет семь членов; третье, пятое и шестое вхождения символов в это
+формальное выражение являются каждое вхождением~$0$; различные входящие в него
+символы~---~это~$($,~$0$,~$\forall$‚~$=$. Формальные выражения структурно
+аналогичны словам языка, но при интерпретации некоторые из них соответствуют
+целым предложениям, например~${(\frml{a})=(0)}$‚ а другие не имеют смысла,
+например~${((0\forall 00=}$. Здесь снова наша терминология указывает на то
+обстоятельство, что для формальной системы как таковой выражения ничего не
+выражают, а являются только некоторыми распознаваемыми и различимыми объектами.
 %%
 %% исправлена опечатка в оригинале было
 %% "третье, пятое и шестое вхождение символов"
@@ -106,9 +105,9 @@ $0$,~${(\mathit{a})+(\mathit{b})}$‚ ${(\mathit{a})=(0)}$
 В рассуждениях о формальных объектах мы часто будем не выписывать их, а
 представлять (т.~е. обозначать) вводимыми для этой цели буквами или же
 выражениями, содержащими уже введённые таким образом буквы. Например,
-буква~<<$\mathrm{s}$>> может представлять формальное
-выражение~${(\mathit{a})+(\mathit{b})}$‚ а
-буква~<<$\mathrm{A}$>>~---~представлять~${(\mathit{a})=(0)}$. Читатель очень
+буква~<<$\infr{s}$>> может представлять формальное
+выражение~${(\frml{a})+(\frml{b})}$‚ а
+буква~<<$\infr{A}$>>~---~представлять~${(\frml{a})=(0)}$. Читатель очень
 скоро встретит и другие примеры.
 
 Употребляемые таким образом буквы и выражения являются не формальными символами
@@ -120,8 +119,8 @@ $0$,~${(\mathit{a})+(\mathit{b})}$‚ ${(\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}}$), что
+шрифтами~(${\frml{a},\frml{b},\frml{t},\frml{x},\frml{A},\frml{B}}$
+и~${\infr{a},\infr{b},\infr{t},\infr{x},\infr{A},\infr{B}}$), что
 поможет нам непосредственно выражать это обстоятельство.
 
 Использование символов и выражений в качестве названий предметов, о которых мы
@@ -145,26 +144,26 @@ $0$,~${(\mathit{a})+(\mathit{b})}$‚ ${(\mathit{a})=(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)}$.
+${((0\forall 00=}$~и~${(\frml{a})+(\frml{b})}$ в указанном порядке образует
+новое формальное выражение~${((0\forall 00=(\frml{a})+(\frml{b})}$, а
+сочленение семи формальных выражений~$($‚~${(\frml{a})+(\frml{b})}$‚~$)$,~%
+$\OLmult$‚~$($‚~${(\frml{c})'}$‚~$)$ в указанном порядке образует новое
+формальное выражение~${\left((\frml{a})+(\frml{b})\right)\OLmult%
+                       \left((\frml{c})'\right)}$.
 
 Если некоторые из подлежащих сочленению формальных выражений представлены
 метаматематическими буквами или выражениями, то последние могут употребляться в
 записи результата сочленения вместо представляемых ими формальных выражений.
-Например, если буква <<$\mathrm{s}$>> представляет некоторое формальное
+Например, если буква <<$\infr{s}$>> представляет некоторое формальное
 выражение, то результат сочленения семи формальных
-выражений~$($‚~$\mathrm{s}$‚~$)$,~$\OLmult$‚~$($‚~${(\mathit{c})'}$‚~$)$
-записывается так:~<<${(\mathrm{s})\OLmult\left((\mathit{c})'\right)}$>>. Здесь
-<<${(\mathrm{s})\OLmult\left((\mathit{c})'\right)}$>>~есть метаматематическое
+выражений~$($‚~$\infr{s}$‚~$)$,~$\OLmult$‚~$($‚~${(\frml{c})'}$‚~$)$
+записывается так:~<<${(\infr{s})\OLmult\left((\frml{c})'\right)}$>>. Здесь
+<<${(\infr{s})\OLmult\left((\frml{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)}$.
+зависит от того, какое формальное выражение представляет буква~<<$\infr{s}$>>.
+В частности, если $\infr{s}$~есть~${(\frml{a})+(\frml{b})}$, то
+${(\infr{s})\OLmult\left((\frml{c})'\right)}$~есть~%
+${\left((\frml{a})+(\frml{b})\right)\OLmult\left((\frml{c})'\right)}$.
 
 \section{Правила образования}
 \label{sec:17-formation_rules}
@@ -175,9 +174,9 @@ ${\left((\mathit{a})+(\mathit{b})\right)\OLmult\left((\mathit{c})'\right)}$.
 Сначала определим ,,терм``‚ который аналогичен существительному в грамматике.
 Термы рассматриваемой системы все представляют натуральные числа, фиксированные
 или переменные. Определение формулируется с помощью метаматематических
-переменных <<$\mathrm{s}$>>~и~<<$\mathrm{t}$>> и описанной выше операции
-сочленения. Оно имеет вид индуктивного определения, что позволяет нам переходить
-от уже известных термов к дальнейшим.
+переменных <<$\infr{s}$>>~и~<<$\infr{t}$>> и описанной выше операции сочленения.
+Оно имеет вид индуктивного определения, что позволяет нам переходить от уже
+известных термов к дальнейшим.
 
 1.\itemlabel{listItem:p17-list1-1}{1}~$0$~есть \emph{терм}.
 2.\itemlabel{listItem:p17-list1-2}{2}~Каждая переменная есть \emph{терм}.
@@ -185,82 +184,82 @@ ${\left((\mathit{a})+(\mathit{b})\right)\OLmult\left((\mathit{c})'\right)}$.
 \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{термы}.
+$\infr{s}$~и~$\infr{t}$~---~\emph{термы}, то
+${(\infr{s})+(\infr{t})}$‚ ${(\infr{s})\OLmult(\infr{t})}$ и
+${(\infr{s})'}$~---~\emph{термы}.
 6.\itemlabel{listItem:p17-list1-6}{6}~ Никаких других \emph{термов}, кроме
 определённых согласно~\ref{listItem:p17-list1-1}--\ref{listItem:p17-list1-5},
 нет.
 
 \begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p17-1}{exmpl:p17-1}
 В силу \ref{listItem:p17-list1-1}~и~\ref{listItem:p17-list1-2}, термами
-являются~$0$, $\mathit{a}$, $\mathit{b}$ и~$\mathit{c}$. Поэтому, в
-силу~\ref{listItem:p17-list1-5}, ${(0)'}$~и~${(\mathit{c})'}$ являются термами.
+являются~$0$, $\frml{a}$, $\frml{b}$ и~$\frml{c}$. Поэтому, в
+силу~\ref{listItem:p17-list1-5}, ${(0)'}$~и~${(\frml{c})'}$ являются термами.
 Снова в силу~\ref{listItem:p17-list1-5}, ${\left((0)'\right)'}$~есть~терм, а в
 силу~\ref{listItem:p17-list1-3},
-${\left((\textit{c})'\right)+(\mathit{a})}$~есть терм.
+${\left((\frml{c})'\right)+(\frml{a})}$~есть терм.
 \end{SCEnvWLabel}
 
 Теперь дадим определение ,,формулы``~---~аналога (повествовательного)
 предложения в грамматике.
 
 1.\itemlabel{listItem:p17-list2-1}{1}~Если
-$\mathrm{s}$~и~$\mathrm{t}$~---~термы, то
-${(\mathrm{s})=(\mathrm{t})}$~---~\emph{формула}.
+$\infr{s}$~и~$\infr{t}$~---~термы, то
+${(\infr{s})=(\infr{t})}$~---~\emph{формула}.
 2--5.%
 \itemlabel{listItem:p17-list2-2}{2}%
 \itemlabel{listItem:p17-list2-3}{3}%
 \itemlabel{listItem:p17-list2-4}{4}%
 \itemlabel{listItem:p17-list2-5}{5}~Если
-$\mathrm{A}$~и~$\mathrm{B}$~---~\emph{формулы}, то
-${(\mathrm{A})\OLimpl(\mathrm{B})}$,
-${(\mathrm{A})\OLand(\mathrm{B})}$,
-${(\mathrm{A})\vee(\mathrm{B})}$ и
-${\neg(\mathrm{A})}$~---~\emph{формулы}.
+$\infr{A}$~и~$\infr{B}$~---~\emph{формулы}, то
+${(\infr{A})\OLimpl(\infr{B})}$,
+${(\infr{A})\OLand(\infr{B})}$,
+${(\infr{A})\vee(\infr{B})}$ и
+${\neg(\infr{A})}$~---~\emph{формулы}.
 6--7.%
 \itemlabel{listItem:p17-list2-6}{6}%
-\itemlabel{listItem:p17-list2-7}{7}~Если $\mathrm{x}$~---~переменная, а
-$\mathrm{A}$~---~\emph{формула}, то
-${\forall\mathrm{x}(\mathrm{A})}$~и~%
-${\exists\mathrm{x}(\mathrm{A})}$~---~\emph{формулы}.
+\itemlabel{listItem:p17-list2-7}{7}~Если $\infr{x}$~---~переменная, а
+$\infr{A}$~---~\emph{формула}, то
+${\forall\infr{x}(\infr{A})}$~и~%
+${\exists\infr{x}(\infr{A})}$~---~\emph{формулы}.
 8.\itemlabel{listItem:p17-list2-8}{8}~Никаких \emph{формул}, кроме определённых
 согласно~\ref{listItem:p17-list2-1}--\ref{listItem:p17-list2-7}, нет.
 
 \begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p17-2}{exmpl:p17-2}
 Используя~\ref{listItem:p17-list2-1} и уже полученные примеры термов, убеждаемся
-в том, что ${(\mathit{a})=(\mathit{b})}$ и~%
-${\left(\left(\left(\mathit{c}\right)'\right)+\left(\mathit{a}\right)\right)=%
-  \left(\mathit{b}\right)}$~---~формулы. Поэтому, в
+в том, что ${(\frml{a})=(\frml{b})}$ и~%
+${\left(\left(\left(\frml{c}\right)'\right)+\left(\frml{a}\right)\right)=%
+  \left(\frml{b}\right)}$~---~формулы. Поэтому, в
 силу~\ref{listItem:p17-list2-5}~и~\ref{listItem:p17-list2-7},
-${\neg\left(\left(\mathit{a}\right)=\left(\mathit{b}\right)\right)}$ и %
-${\exists\mathit{c}%
+${\neg\left(\left(\frml{a}\right)=\left(\frml{b}\right)\right)}$ и %
+${\exists\frml{c}%
 \left(%
     \left(%
         \left(%
-            \left(\mathit{c}\right)'%
+            \left(\frml{c}\right)'%
         \right)+%
-        \left(\mathit{a}\right)%
+        \left(\frml{a}\right)%
     \right)=%
-    \left(\mathit{b}\right)%
+    \left(\frml{b}\right)%
 \right)}$~---~формулы. Наконец, в силу~\ref{listItem:p17-list2-2}, формулой
 является
 \begin{equation}\label{eq:p17-A}\tag{A}
 \left(
-    \exists\mathit{c}
+    \exists\frml{c}
     \left(
         \left(
             \left(
-                \left(\mathit{c}\right)'
+                \left(\frml{c}\right)'
             \right)+
-            \left(\mathit{a}\right)
+            \left(\frml{a}\right)
         \right)=
-        \left(\mathit{b}\right)
+        \left(\frml{b}\right)
     \right)
 \right)\OLimpl
 \left(
     \neg
     \left(
-        \left(\mathit{a}\right)=\left(\mathit{b}\right)
+        \left(\frml{a}\right)=\left(\frml{b}\right)
     \right)
 \right)\text{.}
 \end{equation}
@@ -279,17 +278,17 @@ ${\exists\mathit{c}%
 полученных выражения. Заключаем данное выражение или каждое из данных выражений
 в скобки и вводим выражение одного из следующих десяти видов:
 \begin{equation}\label{eq:p17-B}\tag{B}
-\OLimpl,\;\;\;\OLand,\;\;\;\vee,\;\;\;\neg,\;\;\;\forall\mathrm{x},\;\;\;%
-\exists\mathrm{x},\;\;\;=,\;\;\;+,\;\;\;\OLmult,\;\;\;'\text{,}
+\OLimpl,\;\;\;\OLand,\;\;\;\vee,\;\;\;\neg,\;\;\;\forall\infr{x},\;\;\;%
+\exists\infr{x},\;\;\;=,\;\;\;+,\;\;\;\OLmult,\;\;\;'\text{,}
 \end{equation}
 
 \noindent%
-где $\mathrm{x}$~---~переменная. Выражение каждого из этих десяти видов мы будем
+где $\infr{x}$~---~переменная. Выражение каждого из этих десяти видов мы будем
 называть \emph{оператором}. В частности,
 $\OLimpl$,~$\OLand$,~$\vee$,~$\neg$~являются \emph{пропозициональными связками},
-а операторы вида ${\forall\mathrm{x}}$~или~${\exists\mathrm{x}}$~суть
-\emph{кванторы}, причём ${\forall\mathrm{x}}$~---~\emph{квантор общности}, а
-${\exists\mathrm{x}}$~---~\emph{квантор существования}; операторы этих шести
+а операторы вида ${\forall\infr{x}}$~или~${\exists\infr{x}}$~суть
+\emph{кванторы}, причём ${\forall\infr{x}}$~---~\emph{квантор общности}, а
+${\exists\infr{x}}$~---~\emph{квантор существования}; операторы этих шести
 видов называются \emph{логическими операторами}.
 
 Данное выражение или пара выражений называются \emph{областью действия}
@@ -302,18 +301,18 @@ ${\exists\mathrm{x}}$~---~\emph{квантор существования}; оп
 \end{SCEnvWLabel}
 
 \begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p17-3}{exmpl:p17-3}
-В формуле~(\ref{eq:p17-A}) область действия первого вхождения оператора~$=$
+В формуле~\eqref{eq:p17-A} область действия первого вхождения оператора~$=$
 состоит из
-части~${\left(\left(\mathit{c}\right)'\right)+\left(\mathit{a}\right)}$ и
-первого вхождения $\mathit{b}$, а область действия ${\exists\mathit{c}}$~есть
+части~${\left(\left(\frml{c}\right)'\right)+\left(\frml{a}\right)}$ и
+первого вхождения $\frml{b}$, а область действия ${\exists\frml{c}}$~есть
 часть~${%
 \left(
     \left(
-        \left(\mathit{c}\right)'
+        \left(\frml{c}\right)'
     \right)+
-    \left(\mathit{a}\right)
+    \left(\frml{a}\right)
 \right)=
-\left(\mathit{b}\right)}$.
+\left(\frml{b}\right)}$.
 \end{SCEnvWLabel}
 
 Отметим теперь следующий факт, к строгому доказательству которого мы сейчас
@@ -338,7 +337,7 @@ ${\exists\mathrm{x}}$~---~\emph{квантор существования}; оп
 из одного выражения}, \emph{эта область действия непосредственно заключается в
 парные скобки и оператор ставится вне этой пары скобок вплотную к ней},
 \emph{т}.~\emph{е}. \emph{непосредственно слева от левой скобки} (\emph{в
-случае}~$\neg$,~${\forall\mathrm{x}}$,~${\exists\mathrm{x}}$) \emph{или
+случае}~$\neg$,~${\forall\infr{x}}$,~${\exists\infr{x}}$) \emph{или
 непосредственно справа от правой скобки} (\emph{в случае}~$'$).
 
 (b)\kern1ex\emph{Для операторов}, \emph{область действия которых состоит из двух
@@ -349,9 +348,9 @@ ${\exists\mathrm{x}}$~---~\emph{квантор существования}; оп
 которую заключено правое выражение}.
 \end{SCEnvWLabel}
 
-\begin{SCEnvWLabel}{Пример\kern1ex3~\textup{(окончание)}.}%
+\begin{SCEnvWLabel}{Пример\kern1ex3\kern1ex\textup{(окончание)}.}%
 {exmpl:p17-3-end}{exmpl:p17-3-end}
-Рассмотренный пример формулы~(\ref{eq:p17-A}) содержит 22 скобки. По
+Рассмотренный пример формулы~\eqref{eq:p17-A} содержит 22 скобки. По
 лемме~\ref{lemma:p17-4}, эти 22 скобки допускают собственное спаривание,
 %% ======================= Страница 71 =======================
 которое находится из процесса построения формулы согласно определениям терма и
@@ -363,13 +362,13 @@ ${\exists\mathrm{x}}$~---~\emph{квантор существования}; оп
 проделали это в конце~\textsection~\ref{sec:7-mathematical_induction}, где те же
 самые 22 скобки рассматривались независимо от стоящих между ними символов.
 Пользуясь полученным разбиением на пары для этих 22 скобок, входящих в полную
-формулу~(\ref{eq:p17-A}), можно заметить, что область действия первого
+формулу~\eqref{eq:p17-A}, можно заметить, что область действия первого
 вхождения~$=$ состоит из выражения, заключённого между
 скобками~${\big(\vphantom{a}^{3}_{4}\;\:\big)\vphantom{a}^{10}_{4}}$, и
 выражения, заключённого между
 скобками~${\big(\vphantom{a}^{11}_{5}\;\:\big)\vphantom{a}^{12}_{5}}$. Это
 согласуется с нашим прежним определением этой области действия. Аналогично,
-область действия~${\exists\mathit{c}}$ заключена между
+область действия~${\exists\frml{c}}$ заключена между
 скобками~${\big(\vphantom{a}^{2}_{6}\;\:\big)\vphantom{a}^{13}_{6}}$.
 \end{SCEnvWLabel}
 
@@ -377,10 +376,10 @@ ${\exists\mathrm{x}}$~---~\emph{квантор существования}; оп
 она и не требуется для доказательства того, что области действия могут быть
 найдены по распределению скобок, полезна при рассуждениях об областях действий в
 частях и во всем выражении (терме или формуле). Например, если
-$\mathrm{М}$,~$\mathrm{N}$~и~$\mathrm{A}$~---~формулы и $\mathrm{A}$~входит
-в~${\left(\mathrm{M}\right)\OLimpl\left(\mathrm{N}\right)}$ как (связная) часть,
+$\infr{M}$,~$\infr{N}$~и~$\infr{A}$~---~формулы и $\infr{A}$~входит
+в~${\left(\infr{M}\right)\OLimpl\left(\infr{N}\right)}$ как (связная) часть,
 отличная от всей формулы, то можно заключить, что эта часть (или каждая такая
-часть) является частью~$\mathrm{М}$ или частью~$\mathrm{N}$.
+часть) является частью~$\infr{M}$ или частью~$\infr{N}$.
 
 При выборе наших определений терма и формулы мы, конечно, вводили скобки ради
 вышеизложенной цели, однозначного определения областей действия. Ясно, однако,
@@ -394,10 +393,10 @@ $\mathrm{М}$,~$\mathrm{N}$~и~$\mathrm{A}$~---~формулы и $\mathrm{A}$~
 смысле~${\left(a\OLmult b\right)+c}$. Мы будем говорить в этом случае, что
 $+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚ и припишем нашим операторам
 ранги, понижающиеся в том порядке, в котором мы их перечислили выше
-в~(\ref{eq:p17-B}). Чтобы восстановить любые скобки, опущенные при сокращении
+в~\eqref{eq:p17-B}. Чтобы восстановить любые скобки, опущенные при сокращении
 терма или формулы, можно, выбирая последовательно каждый раз из всех
 присутствующих операторов тот, который раньше других встречается в
-списке~(\ref{eq:p17-B}), т.~е. оператор наивысшего ранга, придавать ему
+списке~\eqref{eq:p17-B}, т.~е. оператор наивысшего ранга, придавать ему
 наибольшую область действия, совместимую с требованием, чтобы всё выражение было
 термом или формулой.
 %%
@@ -412,31 +411,25 @@ $+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚
 
 \begin{SCEnvWLabel}{Пример\kern1ex4.}{exmpl:p17-4}{exmpl:p17-4}
 Восстановление скобок
-в~<<${\mathrm{A}\OLimpl\mathrm{B}\vee\mathrm{C}\OLand\mathrm{D}}$>> даёт
+в~<<${\infr{A}\OLimpl\infr{B}\vee\infr{C}\OLand\infr{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}
+<<${\infr{A}\OLimpl\left(\infr{B}\vee\infr{C}\OLand\infr{D}\right)}$>>,
+<<${\infr{A}\OLimpl\left(
+    \left(\infr{B}\vee\infr{C}\right)
+    \OLand\infr{D}
 \right)}$>>,
-<<${\left(\mathrm{A}\right)\OLimpl
+<<${\left(\infr{A}\right)\OLimpl
 \left(
     \left(
-        \left(\mathrm{B}\right)\vee\left(\mathrm{C}\right)
+        \left(\infr{B}\right)\vee\left(\infr{C}\right)
     \right)
-    \OLand\left(\mathrm{D}\right)
-\right)}$>>. Рассмотренный пример формулы~(\ref{eq:p17-A}) сокращённо
+    \OLand\left(\infr{D}\right)
+\right)}$>>. Рассмотренный пример формулы~\eqref{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{.}
+\exists\frml{c}
+\left(\frml{c}'+\frml{a}=\frml{b}\right)
+\OLimpl\neg\frml{a}=\frml{b}\text{.}
 \end{equation}
 
 Другого рода сокращения даёт нам введение нового символа вместе с методом
@@ -447,33 +440,32 @@ $+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚
 \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}) может быть при этом записана так:
+формулу~${\neg\frml{a}=\frml{b}}$ сокращаем в~<<${\frml{a}\neq\frml{b}}$>>, а
+формулу~${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)}$
+сокращаем в <<${\frml{a}<\frml{b}}$>>. Рассмотренная
+формула~\eqref{eq:p17-A} может быть при этом записана так:
 \begin{equation}\label{eq:p17-A-stroke-stroke}\tag{A$''$}
-\mathit{a}<\mathit{b}\OLimpl\mathit{a}\neq\mathit{b}\text{.}
+\frml{a}<\frml{b}\OLimpl\frml{a}\neq\frml{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}$. При восстановлении сокращения, если оно было связано с
+писать~<<${\infr{s}\neq\infr{t}}$>> как сокращение
+для~${\neg\infr{s}=\infr{t}}$‚ где $\infr{s}$~и~$\infr{t}$~---~термы. Общее
+правило для сокращения~<<$<$>> позволяет нам
+писать~<<${\infr{s}<\infr{t}}$>> как сокращение
+для~${\exists\infr{x}\left(\infr{x}'+\infr{s}=\infr{t}\right)}$‚
+где $\infr{x}$~---~переменная, а $\infr{s}$~и~$\infr{t}$~---~термы, не
+содержащие~$\infr{x}$. При восстановлении сокращения, если оно было связано с
 опусканием переменной, как в случае~<<$<$>>, имеется произвол в отношении выбора
 подлежащей восстановлению переменной. Так, при
-восстановлении~<<${\mathrm{s}<\mathrm{t}}$>> мы можем выбрать в
-качестве~$\mathrm{x}$ любую переменную, не содержащуюся
-в~$\mathrm{s}$~и~$\mathrm{t}$. Этот произвол является мало существенным,
-поскольку утверждения, которые мы собираемся делать о сокращённой формуле, имеют
-место независимо от выбора допустимой переменной.
+восстановлении~<<${\infr{s}<\infr{t}}$>> мы можем выбрать в
+качестве~$\infr{x}$ любую переменную, не содержащуюся в~$\infr{s}$~и~$\infr{t}$.
+Этот произвол является мало существенным, поскольку утверждения, которые мы
+собираемся делать о сокращённой формуле, имеют место независимо от выбора
+допустимой переменной.
 
 Мы будем считать, что все эти сокращения относятся только к изложению
 метаматематики. Это соответствует нашим целям, и таким путём мы сохраняем
@@ -486,90 +478,442 @@ $+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚
 \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{свободной переменной}).
+Вхождение переменной~$\infr{x}$ в формулу~$\infr{A}$ называется \emph{связанным}
+(или вхождением в качестве \emph{связанной переменной}), если оно является
+вхождением в квантор~${\forall\infr{x}}$ или~${\exists\infr{x}}$ или в область
+действия квантора~${\forall\infr{x}}$ или~${\exists\infr{x}}$ (с тем же
+самым~$\infr{x}$); в противном случае вхождение называется \emph{свободным} (или
+вхождением в качестве \emph{свободной переменной}).
 
 \begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p18-1}{exmpl:p18-1}
 В~${
-\exists\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\frml{c}
+\left(\frml{c}'+\frml{a}=\frml{b}\right)
+\OLimpl\neg\frml{a}=\frml{b}}$‚ оба вхождения~$\frml{a}$ и оба
+вхождения~$\frml{b}$~---~свободные‚ а оба вхождения~$\frml{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}$~---~связанные.
+\exists\frml{c}
+\left(\frml{c}'+\frml{a}=\frml{b}\right)
+\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$ первые два
+вхождения~$\frml{c}$~---~связанные, а третье~---~свободное.
+В~${
+\exists\frml{c}\left(
+    \exists\frml{c}\left(
+        \frml{c}'+\frml{a}=\frml{b}
+    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
+\right)}$ все вхождения~$\frml{c}$~---~связанные.
 \end{SCEnvWLabel}
 
-Мы будем говорить также, что любое вхождение переменной~$\mathrm{x}$ в
-терм~$\mathrm{t}$ является \emph{свободным}, как это будет следовать из
-приведённого определения, если заменить в нем слова <<формула~$\mathrm{A}$>>
-на <<терм~$\mathrm{t}$>>. Различие между свободным и связанным вхождением
-переменной всегда связано с термом или формулой, для которых (в каждом случае)
+Мы будем говорить также, что любое вхождение переменной~$\infr{x}$ в
+терм~$\infr{t}$ является \emph{свободным}, как это будет следовать из
+приведённого определения, если заменить в нем слова <<формула~$\infr{A}$>> на
+<<терм~$\infr{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}
+\begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p18-2}{2}
+Третье вхождение~$\frml{c}$ в~${
+\exists\frml{c}\left(
+    \exists\frml{c}\left(
+        \frml{c}'+\frml{a}=\frml{b}
+    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
 \right)}$ является свободным, если его рассматривать как вхождение в саму эту
-часть~$\mathit{c}$, или в часть~${\mathit{c}'}$, или в
-часть~${\mathit{c}'+\mathit{a}}$‚ или в
-часть~${\mathit{c}'+\mathit{a}=\mathit{b}}$, и связанным, если его рассматривать
-как вхождение в часть~${
-\exists\mathit{c}\left(
-    \mathit{c}'+\mathit{a}=\mathit{b}
+часть~$\frml{c}$, или в часть~${\frml{c}'}$, или в
+часть~${\frml{c}'+\frml{a}}$‚ или в
+часть~${\frml{c}'+\frml{a}=\frml{b}}$, и связанным, если его рассматривать как
+вхождение в часть~${
+\exists\frml{c}\left(
+    \frml{c}'+\frml{a}=\frml{b}
 \right)}$‚ или в часть~${
-\exists\mathit{c}\left(
-    \mathit{c}'+\mathit{a}=\mathit{b}
-\right)\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}}$, или во всю формулу.
+\exists\frml{c}\left(
+    \frml{c}'+\frml{a}=\frml{b}
+\right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$, или во всю формулу.
 \end{SCEnvWLabel}
 
-Если переменная~$\mathrm{x}$ входит в качестве свободной переменной (коротко:
-входит свободно) в~$\mathrm{A}$, то говорят, что $\mathrm{x}$~является
-\emph{свободной переменной} выражения~$\mathrm{A}$, или что
-$\mathrm{A}$~\emph{содержит}~$\mathrm{x}$ \emph{в качестве свободной
-переменной} (коротко: $\mathrm{A}$~\emph{содержит свободно}~$\mathrm{x}$);
-аналогично для связанных переменных.
+Если переменная~$\infr{x}$ входит в качестве свободной переменной (коротко:
+входит свободно) в~$\infr{A}$, то говорят, что $\infr{x}$~является
+\emph{свободной переменной} выражения~$\infr{A}$, или что
+$\infr{A}$~\emph{содержит}~$\infr{x}$ \emph{в качестве свободной переменной}
+(коротко: $\infr{A}$~\emph{содержит свободно}~$\infr{x}$); аналогично для
+связанных переменных.
 
 \begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p18-3}{exmpl:p18-3}
 Свободные переменные в~${
-\exists\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}$.
+\exists\frml{c}\left(
+    \frml{c}'+\frml{a}=\frml{b}
+\right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}}$
+суть~$\frml{a}$,~$\frml{b}$~и~$\frml{c}$, а единственная связанная переменная
+есть~$\frml{c}$.
 \end{SCEnvWLabel}
 
-Связанное вхождение переменной~$\mathrm{x}$ в формулу~$\mathrm{A}$ связано
-\emph{тем} вхождением квантора~${\forall\mathrm{x}}$ или~~${\exists\mathrm{x}}$
-(с тем же самым~$\mathrm{x}$), в области действия которого
+Связанное вхождение переменной~$\infr{x}$ в формулу~$\infr{A}$ связано
+\emph{тем} вхождением квантора~${\forall\infr{x}}$ или~${\exists\infr{x}}$ (с
+тем же самым~$\infr{x}$), в области действия которого
 %% ======================= Страница 73 =======================
+оно встречается и которое имеет при этом наименьшую область действия (короче,
+посредством самого внутреннего квантора, в области действия которого оно
+встречается), или в случае, когда оно является вхождением в
+квантор~${\forall\infr{x}}$ или~${\exists\infr{x}}$, самим этим квантором
+(говорят также, что квантор \emph{связывает} эту переменную).
 
+\begin{SCEnvWLabel}{Пример\kern1ex4.}{exmpl:p18-4}{4}
+В~${
+\exists\frml{c}\left(
+    \exists\frml{c}\left(
+        \frml{c}'+\frml{a}=\frml{b}
+    \right)\OLimpl\neg\frml{a}=\frml{b}+\frml{c}
+\right)}$ первое и четвёртое вхождения~$\frml{c}$ связаны первым
+квантором~${\exists\frml{c}}$, а второе и третье вхождения~$\frml{c}$~---~вторым
+квантором~${\exists\frml{c}}$.
+\end{SCEnvWLabel}
 
-stub
+Связанное вхождение переменной в формулу связано тем квантором, введение
+которого (при построении этой формулы, согласно определениям терма и формулы)
+впервые превратило это вхождение из свободного в связанное (или, если это
+переменная в кванторе,~---~тем квантором, в котором она вводится).
 
-\section{Правила преобразования}
-\label{sec:19-transformation_rules}
+\begin{SCEnvWLabel}{Пример\kern1ex5.}{exmpl:p18-5}{exmpl:p18-5}
+Сравните пример~\ref{exmpl:p18-4} с примером~\ref{exmpl:p18-2}.
+\end{SCEnvWLabel}
 
-stub
+Сделаем теперь несколько предварительных замечаний об интерпретации свободных и
+связанных переменных (называемых иногда ,,действительными`` и ,,кажущимися``
+переменными). Эти замечания, конечно, не являются частью метаматематики, но они
+должны способствовать усвоению метаматематических различий. Выражение,
+содержащее свободную переменную, представляет величину или предложение,
+зависящее от значения этой переменной. Выражение, содержащее связанную
+переменную, представляет результат операции, применённой к области изменения
+этой переменной. Наши связанные переменные относятся к логическим операциям
+квантификации, но имеются примеры с операциями другого рода, обычными в
+математике. В следующих примерах $n$~и~$y$ свободны, а $i$~и~$x$ связаны:
+\begin{equation}\label{eq:p18-A}\tag{A}
+\sum_{i=1}^{n} a_{i},\;\;\;\;\;\;\;
+\lim_{x\to 0} f(x,y),\;\;\;\;\;\;\;
+\int\displaylimits_{-y}^{y}  f(x,y)dx\text{.}
+\end{equation}
+
+В следующем примере вхождение~$t$ в качестве верхнего предела интегрирования
+свободно, а вхождения в подинтегральное выражение~---~связаны:
+\begin{equation}\label{eq:p18-B}\tag{B}
+\int\displaylimits_{0}^{t}  f(t)dt\text{.}
+\end{equation}
+
+Возвращаясь к интерпретации, можно отметить некоторые характерные различия,
+которым она подвергает способ пользования обоими родами переменных в
+неформальной математике. Связанная переменная является частью описания,
+выражающего результат операции, выполненной над областью изменения переменной, и
+поэтому можно (соблюдая некоторые предосторожности), не меняя смысла, заменить
+эту переменную на любую другую, имеющую ту же самую область изменения. Например,
+\begin{equation}\label{eq:p18-C}\tag{C}
+\sum_{j=1}^{n} a_{j},\;\;\;\;\;\;\;
+\lim_{z\to 0} f(z,y),\;\;\;\;\;\;\;
+\int\displaylimits_{-y}^{y}  f(t,y)dt
+\end{equation}
+
+\noindent%
+означают (обычно) то же самое, что и соответствующие выражения~\eqref{eq:p18-A},
+приведённые выше (но ${\displaystyle{\lim_{y\to 0} f(y,y)}}$~не совпадает
+(обычно) с~${\displaystyle{\lim_{x\to 0} f(x,y)}}$). Если в некоторое выражение
+подставить вместо свободной переменной выражение, представляющее постоянный или
+переменный предмет из области
+%% ======================= Страница 74 =======================
+её изменения, мы (обычно) получим осмысленный результат, но эта же подстановка,
+применённая к связанной переменной, может привести к бессмыслице. Например
+(подстановкой в~\eqref{eq:p18-A}), получаем (обычно) осмысленные выражения
+\begin{equation}\label{eq:p18-D}\tag{D}
+\sum_{i=1}^{5} a_{i},\;\;\;\;\;\;\;
+\lim_{x\to 0} f(x,2),\;\;\;\;\;\;\;
+\int\displaylimits_{-z}^{z}  f(x,z)dx\text{,}
+\end{equation}
+
+\noindent%
+но этого нельзя сказать о
+\begin{equation}\label{eq:p18-E}\tag{E}
+\sum_{5=1}^{n} a_{5},\;\;\;\;\;\;\;
+\lim_{2\to 0} f(2,y),\;\;\;\;\;\;\;
+\int\displaylimits_{-z}^{z}  f(0,z)d0\text{.}
+\end{equation}
+
+\noindent%
+Если одна и та же переменная входит в выражение и как свободная, и как
+связанная, то представляемая этим выражением величина зависит только от значения
+этой переменной в её свободных вхождениях. Таким образом,
+интеграл~\eqref{eq:p18-B} является функцией от~$t$, значение которой для~${t=3}$
+есть
+\begin{equation}\label{eq:p18-F}\tag{F}
+\int\displaylimits_{0}^{3}  f(t)dt\text{,}\;\;\;\;\;\;\;\text{но не}\;\;\;%
+\int\displaylimits_{0}^{3}  f(3)d3\text{.}
+\end{equation}
+
+\begin{SCEnvWLabel}{Подстановка.}{spar:p18-substitution}{spar:p18-substitution}
+При формулировке метаматематических определений следующего параграфа мы
+используем операцию подстановки, которую мы определим следующим образом.
+\emph{Подстановка} терма~$\infr{t}$ \emph{вместо} переменной~$\infr{x}$ \emph{в}
+(или, иначе, \emph{повсюду в}) терм или формулу~$\infr{A}$ состоит в
+одновременной замене каждого свободного вхождения~$\infr{x}$ в~$\infr{A}$
+на вхождение~$\infr{t}$. Чтобы описать это в терминах сочленения, обозначим
+через~$n$ число свободных вхождений~$\infr{x}$ в~$\infr{A}$~(${n\geqslant 0}$) и
+запишем~$\infr{A}$ в виде~<<${\infr{A}_{0}\infr{x}\infr{A}_{1}\infr{x}\;\ldots\;
+\infr{A}_{n-1}\infr{x}\infr{A}_{n}}$>>‚ указывающем эти вхождения
+(где~${\infr{A}_{0},\infr{A}_{1}, \ldots,%
+       \infr{A}_{n-1},\infr{A}_{n}}$~---~части‚ возможно пустые, не содержащие
+вхождений~$\infr{x}$, свободных относительно всего~$\infr{A}$, и все указанные
+$n$~вхождений~$\infr{x}$ свободны). Тогда результатом подстановки~$\infr{t}$
+вместо~$\infr{x}$ в~$\infr{A}$
+будет~${\infr{A}_{0}\infr{t}\infr{A}_{1}\infr{t}\;\ldots\;
+\infr{A}_{n-1}\infr{t}\infr{A}_{n}}$.
+%%
+%% исправлено выделение в определении
+%% оно приведено в семантическое соответствие с англоязычным оригиналом
+%%
+
+Для представления результата подстановки будет полезно одно компактное
+метаматематическое обозначение. Если подстановка производится вместо~$\infr{x}$,
+введём сначала для субституэнда\footnote{Т.~е. выражения, в которое производится
+подстановка. Употребление термина <<субституэнд>> в данной книге отличается от
+принятого у Гильберта и Бернайса~\cite{hilbert_and_bernays1939} дополнение~I,
+где рассматриваются подстановки вместо формульных переменных (ср.~ниже
+стр.~\pageref{spar:p37-predicate_calculus_with_a_postulated_substitution_rule})
+и субституэндом называется выражение, которое подставляется вместо данной
+переменной.~---~\textit{Прим.~перев.}} некоторое составное выражение,
+например~<<${\infr{A}(\infr{x})}$>>, показывающее его зависимость от~$\infr{x}$,
+согласно способу обозначения для функций в
+математике~(\textsection~\ref{sec:10-functions}). Результат
+подстановки~$\infr{t}$ вместо~$\infr{x}$ в~${\infr{A}(\infr{x})}$ записывается
+тогда в виде~<<${\infr{A}(\infr{t})}$>>.
+\end{SCEnvWLabel}
+
+\begin{SCEnvWLabel}{Пример\kern1ex6.}{exmpl:p18-6}{exmpl:p18-6}
+Пусть $\infr{x}$~есть~$\frml{c}$, а\\
+{\setlength{\tabcolsep}{0pt}\begin{tabular}{llll}
+${\infr{A}(\infr{x})}$, или\kern1ex&${\infr{A}(\frml{c})}$,\kern1ex&есть\kern1ex
+&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
+\neg\frml{a}=\frml{b}+\frml{c}}$.\\
+Тогда&${\infr{A}(0)}$&есть%
+&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
+\neg\frml{a}=\frml{b}+\frml{0}}$,\\
+а&${\infr{A}(\frml{a})}$&есть%
+&${\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl%
+\neg\frml{a}=\frml{b}+\frml{a}}$.
+\end{tabular}}
+%%
+%% исправлено представление Примера 6
+%% оно приведено в соответствие с представлением англоязычного оригинала,
+%% что делает Пример 6 яснее
+%%
+\end{SCEnvWLabel}
 
+\begin{SCEnvWLabel}{Пример\kern1ex7.}{exmpl:p18-7}{exmpl:p18-7}
+Пусть $\infr{x}$~есть~$\frml{a}$, а $\infr{A}(\infr{x})$~есть~%
+${\frml{a}+\frml{c}=\frml{a}}$. Тогда ${\infr{A}(0)}$~есть~%
+${0+\frml{c}=0}$, а ${\infr{A}(\frml{b})}$~есть~${\frml{b}+\frml{c}=\frml{b}}$.
+\end{SCEnvWLabel}
+
+
+Подстановка, которая даёт~${\infr{A}(\infr{t})}$, всегда должна производиться
+вместо первоначальной переменной~$\infr{x}$ в первоначальной
+формуле~${\infr{A}(\infr{x})}$, т.~е. вместо той переменной и в ту формулу, для
+которых предварительно было введено обозначение <<${\infr{A}(\infr{x})}$>>.
+
+%% ======================= Страница 75 =======================
+
+\begin{SCEnvWLabel}{Пример\kern1ex7\kern1ex\textup{(окончание)}.}%
+{exmpl:p18-7-end}{exmpl:p18-7-end}
+Для указанных выше~$\infr{x}$~и~${\infr{A}(\infr{x})}$‚ ${\infr{A}(\frml{c})}$
+есть~${\frml{c}+\frml{c}=\frml{c}}$. Если подставить~$\frml{b}$
+вместо~$\frml{c}$ в~${\infr{A}(\frml{c})}$, то
+получится~${\frml{b}+\frml{b}=\frml{b}}$. Это не совпадает
+с~${\infr{A}(\frml{b})}$, которое прежде мы правильно получили посредством
+подстановки~$\frml{b}$ вместо~$\frml{a}$ в~${\infr{A}(\frml{a})}$, т.~е. вместо
+первоначального~${\infr{x}}$ в первоначальное~${\infr{A}(\infr{x})}$. (Это же
+затруднение может встретиться при неправильном употреблении обозначений для
+функции в неформальной математике.)
+\end{SCEnvWLabel}
+
+
+Мы не потребовали, чтобы переменная~$\infr{x}$ действительно входила
+в~${\infr{A}(\infr{x})}$ в качестве свободной переменной. Если $\infr{x}$~не
+является свободной переменной~${\infr{A}(\infr{x})}$‚ то результат
+подстановки~${\infr{A}(\infr{t})}$ есть само первоначальное
+выражение~${\infr{A}(\infr{x})}$.
+
+Аналогично мы определим подстановку, произведённую одновременно вместо
+нескольких различных переменных; мы будем пользоваться при этом аналогичными
+обозначениями, например <<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>>~для
+субституэнда и <<${\infr{A}(\infr{t}_{1},\ldots,\infr{t}_{n})}$>>~для
+результата.
+
+В дальнейшем мы часто будем вводить составные обозначения, например
+<<${\infr{A}(\infr{x})}$>>~или~%
+<<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>> вместо~<<$\infr{A}$>>, когда
+нас будет интересовать зависимость~$\infr{A}$ от переменной~$\infr{x}$ или
+переменных~${\infr{x}_{1},\ldots,\infr{x}_{n}}$ независимо от того, надо ли нам
+будет или нет делать подстановку. Например, обычно мы обозначаем
+формулу~<<${\infr{A}(\infr{x})}$>> вместо~<<$\infr{A}$>>, если собираемся
+употребить её в~${\forall\infr{x}\infr{A}(\infr{x})}$ (читается <<для
+всех~$\infr{x}$, $\infr{A}$~от~$\infr{x}$>>) или
+в~${\exists\infr{x}\infr{A}(\infr{x})}$ (читается <<существует
+некоторое~$\infr{x}$, такое, что $\infr{A}$~от~$\infr{x}$>> или, кратко,
+<<существует~$\infr{x}$, $\infr{A}$~от~$\infr{x}$>>). Подчеркнём, что при
+обозначении~<<${\infr{A}(\infr{x})}$>> (или
+<<${\infr{A}(\infr{x}_{1},\ldots,\infr{x}_{n})}$>>) не подразумевается, что
+$\infr{x}$~(или каждое из~${\infr{x}_{1},\ldots,\infr{x}_{n}}$) обязательно
+входит свободно в обозначенную формулу.
+
+Предварительные замечания об интерпретации проливают свет на то, почему при
+нашем выборе определения для метаматематической операции подстановки последняя
+применяется только к свободным вхождениям переменных.
+
+Далее, мы будем говорить, что терм~$\infr{t}$ \emph{свободен при свободных
+вхождениях} переменной~$\infr{x}$ \emph{в} формулу~${\infr{A}(\infr{x})}$ (или,
+что $\infr{t}$~\emph{свободен на местах подстановки вместо}~$\infr{x}$
+\emph{в}~${\infr{A}(\infr{x})}$‚ или, короче, что
+$\infr{t}$~\emph{свободен для}~$\infr{x}$ \emph{в}~${\infr{A}(\infr{x})}$)‚ если
+никакое свободное вхождение~$\infr{x}$ в~${\infr{A}(\infr{x})}$ не входит в
+область действия какого\nobreakdash-нибудь квантора~${\forall\infr{y}}$
+или~${\exists\infr{y}}$, где $\infr{y}$~---~переменная из~$\infr{t}$ (т.~е.
+входящая в~$\infr{t}$).
+%%
+%% исправлено выделение буквы "в"
+%% в соответствии с семантикой и выделением в англоязычном оригинале
+%%
+
+\begin{SCEnvWLabel}{Пример\kern1ex8.}{exmpl:p18-8}{exmpl:p18-8}
+Термы~${\frml{d}}$,~${\frml{d}+0'}$~и~${\frml{a}\OLmult\frml{d}}$ свободны
+для~$\frml{a}$ в первой и не свободны во второй из следующих формул:
+\begin{equation}\label{eq:p18-I}\tag{I}
+\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLand
+\neg\frml{d}=0\text{,}\;\;\;\;\;\;\;
+\exists\frml{d}\left(\frml{d}'+\frml{a}=\frml{b}\right)\OLand
+\neg\frml{d}=0\text{.}
+\end{equation}
+\end{SCEnvWLabel}
+
+Согласно этому определению, если $\infr{t}$~свободен для~$\infr{x}$
+в~${\infr{A}(\infr{x})}$~---~и только в этом случае~---~при
+подстановке~$\infr{t}$ вместо~$\infr{x}$ в~${\infr{A}(\infr{x})}$
+терм~$\infr{t}$ не возникнет в~${\infr{A}(\infr{x})}$ ни на каком месте, где
+какая\nobreakdash-нибудь (свободная) переменная~$\infr{y}$ из~$\infr{t}$ вошла
+бы в качестве связанной переменной в результат~$\infr{A}(\infr{t})$.
+
+\begin{SCEnvWLabel}{Пример\kern1ex8\kern1ex\textup{(окончание)}.}%
+{exmpl:p18-8-end}{exmpl:p18-8-end}
+Подстановка~${\frml{d}+0'}$ вместо~$\frml{a}$ в~\eqref{eq:p18-I} даёт
+\begin{equation}\label{eq:p18-II}\tag{II}
+\exists\frml{c}\left(\frml{c}'+\left(\frml{d}+0'\right)=\frml{b}\right)\OLand
+\neg\frml{d}=0\text{,}\;\;\;\;\;\;\;
+\exists\frml{d}\left(\frml{d}'+\left(\frml{d}+0'\right)=\frml{b}\right)\OLand
+\neg\frml{d}=0
+\end{equation}
+
+\noindent%
+соответственно. В первом случае введённое подстановкой вхождение~$\frml{d}$
+из~${\frml{d}+0'}$ остаётся свободным во всей формуле, а во втором случае это не
+имеет места.
+\end{SCEnvWLabel}
+
+Мы будем говорить, что подстановка~$\infr{t}$ вместо~$\infr{x}$
+в~${\infr{A}(\infr{x})}$ \emph{свободна}, если $\infr{t}$~свободно
+для~$\infr{x}$ в~${\infr{A}(\infr{x})}$. Уже при поверхностном взгляде на
+указанную выше интерпретацию видно, что подстановка не годится, если она не
+свободна.
+
+%% ======================= Страница 76 =======================
 
+Обе формулы в~\eqref{eq:p18-I} означают одно и то же, но в~\eqref{eq:p18-II} это
+не так.
 
+В качестве содержательного примера рассмотрим второе выражение
+из~\eqref{eq:p18-A} или~\eqref{eq:p18-C}. Оно означает некоторую функцию от~$y$,
+назовём её
+\begin{equation}\label{eq:p18-G}\tag{G}
+f(y)=\lim_{x\to 0} f(x,y)=\lim_{z\to 0} f(z,y)\text{.}
+\end{equation}
+
+Значение~${f(y)}$ для~${y=z}$ правильно записывается в виде
+\begin{equation}\label{eq:p18-H}\tag{H}
+f(z)=\lim_{x\to 0} f(x,z)\text{,}
+\end{equation}
+
+\noindent%
+но не в виде~${f(z)=\displaystyle{\lim_{z\to 0} f(z,z)}}$.
+
+\begin{SCEnvWLabel}{Пример\kern1ex9.}{exmpl:p18-9}{exmpl:p18-9}
+Для иллюстрации обращения с терминологией и обозначениями, введёнными в этом
+параграфе, предположим, что $\infr{x}$~---~переменная (т.~е.
+<<$\infr{x}$>>~обозначает переменную), ${\infr{A}(\infr{x})}$~---~формула (т.~е.
+<<${\infr{A}(\infr{x})}$>> обозначает формулу), а $\infr{b}$~есть (т.~е.
+<<$\infr{b}$>>~обозначает \ldots) такая переменная, что
+(i)\itemlabel{listItem:p18-list1-i}{(i)}~$\infr{b}$~свободна для~$\infr{x}$
+в~${\infr{A}(\infr{x})}$ и
+(ii)\itemlabel{listItem:p18-list1-ii}{(ii)}~$\infr{b}$~не входит свободно
+в~${\infr{A}(\infr{x})}$ (или $\infr{b}$~есть~$\infr{x}$). Согласно нашим
+обозначениям для подстановки, поскольку обозначение~${\infr{A}(\infr{x})}$ было
+введено для~<<$\infr{x}$>>~и~<<${\infr{A}(\infr{x})}$>>,
+(iii)\itemlabel{listItem:p18-list1-iii}{(iii)}~${\infr{A}(\infr{b})}$~есть (по
+определению) результат подстановки~$\infr{b}$ вместо (свободных
+вхождений)~$\infr{x}$ в~${\infr{A}(\infr{x})}$. В
+силу~\ref{listItem:p18-list1-i}, вхождения~$\infr{b}$ в~${\infr{A}(\infr{b})}$,
+введённые этой подстановкой, являются свободными. В
+силу~\ref{listItem:p18-list1-ii}, других свободных вхождений~$\infr{b}$
+в~${\infr{A}(\infr{b})}$~нет. Итак, свободные вхождения~$\infr{b}$
+в~${\infr{A}(\infr{b})}$~---~это в точности вхождения, введённые этой
+подстановкой. Поэтому (обратно
+к~\ref{listItem:p18-list1-i}--\ref{listItem:p18-list1-iii})
+(iv)\itemlabel{listItem:p18-list1-iv}{(iv)}~$\infr{x}$~свободно для~$\infr{b}$
+в~${\infr{A}(\infr{b})}$,
+(v)\itemlabel{listItem:p18-list1-v}{(v)}~$\infr{x}$~не входит свободно
+в~${\infr{A}(\infr{b})}$ (или $\infr{x}$~есть~$\infr{b}$), и, кроме того,
+(vi)\itemlabel{listItem:p18-list1-vi}{(vi)}~${\infr{A}(\infr{x})}$~является
+результатом подстановки~$\infr{x}$ вместо (свободных вхождений)~$\infr{b}$
+в~${\infr{A}(\infr{b})}$. Например,
+\begin{equation*}
+\infr{x},\;\;\;\;\;\infr{A}(\infr{x}),\;\;\;\;\;
+\infr{b},\;\;\;\;\;\infr{A}(\infr{b})
+\end{equation*}
+
+\noindent%
+могут быть соответственно
+\begin{equation*}
+\frml{c},\;\;\;\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl
+\neg\frml{a}=\frml{b}+\frml{c},\;\;\;
+\frml{d},\;\;\;\exists\frml{c}\left(\frml{c}'+\frml{a}=\frml{b}\right)\OLimpl
+\neg\frml{a}=\frml{b}+\frml{d}
+\end{equation*}
+\end{SCEnvWLabel}
+
+\section{Правила преобразования}
+\label{sec:19-transformation_rules}
+
+В этом параграфе мы введём дальнейшие метаматематические определения (называемые
+\emph{дедуктивными правилами}, или \emph{правилами преобразования}), которые
+превращают формальную систему в дедуктивную теорию. Чтобы подчеркнуть аналогию с
+содержательной теорией, мы начнём с перечня <<постулатов>>; однако для
+метаматематики они являются не постулатами в смысле допущений, каковыми они
+действительно не могут быть, поскольку официально они не имеют смысла, а только
+формулами и формами (или схемами), к которым мы будем прибегать, давая
+определения.
+
+Прежде чем приводить этот перечень постулатов, мы рассмотрим типы постулатов,
+которые в нём встречаются. Простейший тип есть ,,аксиома``~---~примером этого
+типа служит <<${\neg\frml{a}'=0}$>>. Это~---~формула нашей формальной системы.
+Затем имеется ,,форма аксиом`` или ,,схема аксиом``, примером которой
+служит~<<${\infr{B}\OLimpl\infr{A}\vee\infr{B}}$>>. Это~---~метаматематическое
+выражение, которое даёт конкретную аксиому каждый раз, когда выбраны формулы,
+представляемые метаматематическими буквами~<<$\infr{A}$>>~и~<<$\infr{B}$>>.
+Например, если $\infr{A}$~есть~${\frml{a}'=0}$‚ а
+$\infr{B}$~есть~${\neg\frml{a}'=0}$‚ получаем
+аксиому~${\neg\frml{a}'=0\OLimpl\frml{a}'=0\vee\neg\frml{a}'=0}$. Таким образом,
+эта схема аксиом является метаматематическим методом для описания бесконечного
+класса аксиом, имеющих общую форму.
+
+Нам нужны также постулаты другого рода, формализующие операции вывода дальнейших
+теорем из аксиом. Это~---~,,правила вывода``, например:
+\begin{equation*}
+\frac{\infr{A},\infr{A}\OLimpl\infr{B}}{\infr{B}}\text{.}
+\end{equation*}
+
+stub
 
 \chapter{Формальный вывод}
 \label{chap:v-formal_deduction}
@@ -672,6 +1016,16 @@ stub
 
 stub
 
+\begin{SCEnvWLabel}{Исчисление предикатов с постулированным правилом %
+подстановки.}{spar:p37-predicate_calculus_with_a_postulated_substitution_rule}%
+{spar:p37-predicate_calculus_with_a_postulated_substitution_rule}
+Также, как исчисление
+высказываний~(\textsection~\ref{sec:30-decision_procedure_interpretation}),
+исчисление предикатов обычно \ldots
+\end{SCEnvWLabel}
+
+stub
+
 \chapter{Формальная арифметика}
 \label{chap:viii-formal_number_theory}