|
|
@@ -244,7 +244,6 @@ ${\exists\mathit{c}%
|
|
|
\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}
|
|
|
@@ -268,18 +267,300 @@ ${\exists\mathit{c}%
|
|
|
|
|
|
%% ======================= Страница 70 =======================
|
|
|
|
|
|
+Из индуктивных определений терма и формулы следует, что каждый терм и каждая
|
|
|
+формула могут быть построены из $0$~и переменных посредством ряда шагов, каждый
|
|
|
+из которых соответствует некоторому прямому пункту одного из этих
|
|
|
+определений~(\textsection~\ref{sec:6-the_natural_numbers}) и может быть назван
|
|
|
+\emph{применением} этого пункта.
|
|
|
+
|
|
|
+Каждый шаг, за исключением применений
|
|
|
+пунктов~\ref{listItem:p17-list1-1}~или~\ref{listItem:p17-list1-2} из определения
|
|
|
+терма, производится следующим образом: вначале нам дано одно или два ранее
|
|
|
+полученных выражения. Заключаем данное выражение или каждое из данных выражений
|
|
|
+в скобки и вводим выражение одного из следующих десяти видов:
|
|
|
+\begin{equation}\label{eq:p17-B}\tag{B}
|
|
|
+\OLimpl,\;\;\;\OLand,\;\;\;\vee,\;\;\;\neg,\;\;\;\forall\mathrm{x},\;\;\;%
|
|
|
+\exists\mathrm{x},\;\;\;=,\;\;\;+,\;\;\;\OLmult,\;\;\;'\text{,}
|
|
|
+\end{equation}
|
|
|
+
|
|
|
+\noindent%
|
|
|
+где $\mathrm{x}$~---~переменная. Выражение каждого из этих десяти видов мы будем
|
|
|
+называть \emph{оператором}. В частности,
|
|
|
+$\OLimpl$,~$\OLand$,~$\vee$,~$\neg$~являются \emph{пропозициональными связками},
|
|
|
+а операторы вида ${\forall\mathrm{x}}$~или~${\exists\mathrm{x}}$~суть
|
|
|
+\emph{кванторы}, причём ${\forall\mathrm{x}}$~---~\emph{квантор общности}, а
|
|
|
+${\exists\mathrm{x}}$~---~\emph{квантор существования}; операторы этих шести
|
|
|
+видов называются \emph{логическими операторами}.
|
|
|
+
|
|
|
+Данное выражение или пара выражений называются \emph{областью действия}
|
|
|
+оператора в получающемся выражении. Прослеживая всё построение терма или
|
|
|
+формулы, устанавливая очевидным образом соответствие между частями данного
|
|
|
+выражения или пары выражений и частями выражения получающегося на каждом шаге
|
|
|
+построения, мы приходим к определению \emph{области действия} не только для
|
|
|
+оператора, введённого последним в законченный терм или формулу, но и для всякого
|
|
|
+оператора в этом терме или формуле.
|
|
|
\end{SCEnvWLabel}
|
|
|
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p17-3}{exmpl:p17-3}
|
|
|
+В формуле~(\ref{eq:p17-A}) область действия первого вхождения оператора~$=$
|
|
|
+состоит из
|
|
|
+части~${\left(\left(\mathit{c}\right)'\right)+\left(\mathit{a}\right)}$ и
|
|
|
+первого вхождения $\mathit{b}$, а область действия ${\exists\mathit{c}}$~есть
|
|
|
+часть~${%
|
|
|
+\left(
|
|
|
+ \left(
|
|
|
+ \left(\mathit{c}\right)'
|
|
|
+ \right)+
|
|
|
+ \left(\mathit{a}\right)
|
|
|
+\right)=
|
|
|
+\left(\mathit{b}\right)}$.
|
|
|
+\end{SCEnvWLabel}
|
|
|
|
|
|
+Отметим теперь следующий факт, к строгому доказательству которого мы сейчас
|
|
|
+перейдём. В данном терме или данной формуле области действия операторов можно
|
|
|
+установить однозначно, исходя из расположения скобок. Другими словами, скобки
|
|
|
+дают возможность, коль скоро дан терм или формула как конечная
|
|
|
+последовательность формальных символов, восстановить все существенные детали его
|
|
|
+(её) построения согласно индуктивным определениям терма и формулы.
|
|
|
+
|
|
|
+Строгое доказательство этого факта даётся
|
|
|
+леммой~\ref{lemma:p7-2}~(\textsection~\ref{sec:7-mathematical_induction},
|
|
|
+пример~\ref{exmpl:p7-2}) вместе со следующей леммой, которую можно доказать по
|
|
|
+индукции, исходя из индуктивных определений терма и формулы.
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Лемма\kern1ex4.}{lemma:p17-4}{4}
|
|
|
+\emph{В каждом данном терме или формуле существует собственное спаривание
|
|
|
+скобок} (\emph{число всех скобок равно}~${2n}$, \emph{из них} $n$~\emph{левых
|
|
|
+скобок и} $n$~\emph{правых}), \emph{такое}, \emph{что область действия всякого
|
|
|
+оператора входит следующим образом}:
|
|
|
+
|
|
|
+(a)\kern1ex\emph{Для операторов}, \emph{область действия которых состоит только
|
|
|
+из одного выражения}, \emph{эта область действия непосредственно заключается в
|
|
|
+парные скобки и оператор ставится вне этой пары скобок вплотную к ней},
|
|
|
+\emph{т}.~\emph{е}. \emph{непосредственно слева от левой скобки} (\emph{в
|
|
|
+случае}~$\neg$,~${\forall\mathrm{x}}$,~${\exists\mathrm{x}}$) \emph{или
|
|
|
+непосредственно справа от правой скобки} (\emph{в случае}~$'$).
|
|
|
+
|
|
|
+(b)\kern1ex\emph{Для операторов}, \emph{область действия которых состоит из двух
|
|
|
+выражений} (\emph{именно}~$\OLimpl$,~$\OLand$,~$\vee$,~$=$,~$+$,~$\OLmult$)‚
|
|
|
+\emph{каждое из этих двух выражений непосредственно заключается в парные
|
|
|
+скобки}, \emph{а оператор ставится непосредственно между правой скобкой пары},
|
|
|
+\emph{в которую заключено левое выражение}, \emph{и левой скобкой пары}, \emph{в
|
|
|
+которую заключено правое выражение}.
|
|
|
+\end{SCEnvWLabel}
|
|
|
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex3~\textup{(окончание)}.}%
|
|
|
+{exmpl:p17-3-end}{exmpl:p17-3-end}
|
|
|
+Рассмотренный пример формулы~(\ref{eq:p17-A}) содержит 22 скобки. По
|
|
|
+лемме~\ref{lemma:p17-4}, эти 22 скобки допускают собственное спаривание,
|
|
|
+%% ======================= Страница 71 =======================
|
|
|
+которое находится из процесса построения формулы согласно определениям терма и
|
|
|
+формулы и которое указывает области действия операторов. Так как существует
|
|
|
+собственное спаривание, то, по лемме~\ref{lemma:p7-2}, это спаривание однозначно
|
|
|
+и поэтому может быть найдено посредством алгоритма
|
|
|
+из~\textsection~\ref{sec:7-mathematical_induction}, без предварительного знания
|
|
|
+построения формулы согласно определениям терма и формулы. Мы фактически уже
|
|
|
+проделали это в конце~\textsection~\ref{sec:7-mathematical_induction}, где те же
|
|
|
+самые 22 скобки рассматривались независимо от стоящих между ними символов.
|
|
|
+Пользуясь полученным разбиением на пары для этих 22 скобок, входящих в полную
|
|
|
+формулу~(\ref{eq:p17-A}), можно заметить, что область действия первого
|
|
|
+вхождения~$=$ состоит из выражения, заключённого между
|
|
|
+скобками~${\big(\vphantom{a}^{3}_{4}\;\:\big)\vphantom{a}^{10}_{4}}$, и
|
|
|
+выражения, заключённого между
|
|
|
+скобками~${\big(\vphantom{a}^{11}_{5}\;\:\big)\vphantom{a}^{12}_{5}}$. Это
|
|
|
+согласуется с нашим прежним определением этой области действия. Аналогично,
|
|
|
+область действия~${\exists\mathit{c}}$ заключена между
|
|
|
+скобками~${\big(\vphantom{a}^{2}_{6}\;\:\big)\vphantom{a}^{13}_{6}}$.
|
|
|
+\end{SCEnvWLabel}
|
|
|
|
|
|
+Лемма~\ref{lemma:p7-3} из~\textsection~\ref{sec:7-mathematical_induction}, хотя
|
|
|
+она и не требуется для доказательства того, что области действия могут быть
|
|
|
+найдены по распределению скобок, полезна при рассуждениях об областях действий в
|
|
|
+частях и во всем выражении (терме или формуле). Например, если
|
|
|
+$\mathrm{М}$,~$\mathrm{N}$~и~$\mathrm{A}$~---~формулы и $\mathrm{A}$~входит
|
|
|
+в~${\left(\mathrm{M}\right)\OLimpl\left(\mathrm{N}\right)}$ как (связная) часть,
|
|
|
+отличная от всей формулы, то можно заключить, что эта часть (или каждая такая
|
|
|
+часть) является частью~$\mathrm{М}$ или частью~$\mathrm{N}$.
|
|
|
+
|
|
|
+При выборе наших определений терма и формулы мы, конечно, вводили скобки ради
|
|
|
+вышеизложенной цели, однозначного определения областей действия. Ясно, однако,
|
|
|
+что обычно в определениях вводят больше скобок, чем строго необходимо для этой
|
|
|
+цели. Ничего не меняя в определениях, мы можем согласиться опускать лишние
|
|
|
+скобки для сокращения записи термов и формул или представляющих их
|
|
|
+метаматематических выражений.
|
|
|
+
|
|
|
+Возможности в этом направлении расширяются употреблением соглашений, аналогичных
|
|
|
+тем, которые приняты в алгебре, где <<${a\OLmult b+c}$>> понимается в
|
|
|
+смысле~${\left(a\OLmult b\right)+c}$. Мы будем говорить в этом случае, что
|
|
|
+$+$~имеет \emph{ранг}, более высокий, чем~$\OLmult$‚ и припишем нашим операторам
|
|
|
+ранги, понижающиеся в том порядке, в котором мы их перечислили выше
|
|
|
+в~(\ref{eq:p17-B}). Чтобы восстановить любые скобки, опущенные при сокращении
|
|
|
+терма или формулы, можно, выбирая последовательно каждый раз из всех
|
|
|
+присутствующих операторов тот, который раньше других встречается в
|
|
|
+списке~(\ref{eq:p17-B}), т.~е. оператор наивысшего ранга, придавать ему
|
|
|
+наибольшую область действия, совместимую с требованием, чтобы всё выражение было
|
|
|
+термом или формулой.
|
|
|
+%%
|
|
|
+%% исправлен шрифт в алгебраических формулах
|
|
|
+%% надо отметить, что в оригинале присутсвует тот же недочёт, что и в переводе -
|
|
|
+%% используется не подходящий по смыслу шрифт
|
|
|
+%%
|
|
|
|
|
|
+Мы не всегда будем опускать максимальное число скобок, допускаемое нашим
|
|
|
+соглашением, стремясь обеспечить максимальное удобство для чтения. (С этой целью
|
|
|
+мы будем также иногда заменять круглые скобки на квадратные или фигурные.)
|
|
|
|
|
|
-stub
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex4.}{exmpl:p17-4}{exmpl:p17-4}
|
|
|
+Восстановление скобок
|
|
|
+в~<<${\mathrm{A}\OLimpl\mathrm{B}\vee\mathrm{C}\OLand\mathrm{D}}$>> даёт
|
|
|
+последовательно~%
|
|
|
+<<${\mathrm{A}\OLimpl
|
|
|
+\left(
|
|
|
+ \mathrm{B}\vee\mathrm{C}\OLand\mathrm{D}
|
|
|
+\right)}$>>,
|
|
|
+<<${\mathrm{A}\OLimpl
|
|
|
+\left(
|
|
|
+ \left(
|
|
|
+ \mathrm{B}\vee\mathrm{C}
|
|
|
+ \right)
|
|
|
+ \OLand\mathrm{D}
|
|
|
+\right)}$>>,
|
|
|
+<<${\left(\mathrm{A}\right)\OLimpl
|
|
|
+\left(
|
|
|
+ \left(
|
|
|
+ \left(\mathrm{B}\right)\vee\left(\mathrm{C}\right)
|
|
|
+ \right)
|
|
|
+ \OLand\left(\mathrm{D}\right)
|
|
|
+\right)}$>>. Рассмотренный пример формулы~(\ref{eq:p17-A}) сокращённо
|
|
|
+записывается в виде
|
|
|
+\begin{equation}\label{eq:p17-A-stroke}\tag{A$'$}
|
|
|
+\exists\mathit{c}
|
|
|
+\left(\mathit{c}'+\mathit{a}=\mathit{b}\right)
|
|
|
+\OLimpl\neg\mathit{a}=\mathit{b}\text{.}
|
|
|
+\end{equation}
|
|
|
+
|
|
|
+Другого рода сокращения даёт нам введение нового символа вместе с методом
|
|
|
+обратного перевода любого выражения, содержащего новый символ, в выражение, не
|
|
|
+содержащее последнего. Например,
|
|
|
+термы~${
|
|
|
+\left(0\right)',
|
|
|
+\left(\left(0\right)'\right)',
|
|
|
+\left(\left(\left(0\right)'\right)'\right)'\ldots}$ мы сокращаем
|
|
|
+соответственно в~<<$1$>>,~<<$2$>>,~<<$3$>>,~$\ldots\:$;
|
|
|
+формулу~${\neg\mathit{a}=\mathit{b}}$ сокращаем
|
|
|
+в~<<${\mathit{a}\neq\mathit{b}}$>>, а
|
|
|
+формулу~${\exists\mathit{c}\left(\mathit{c}'+\mathit{a}=\mathit{b}\right)}$
|
|
|
+сокращаем в <<${\mathit{a}<\mathit{b}}$>>. Рассмотренная
|
|
|
+формула~(\ref{eq:p17-A}) может быть при этом записана так:
|
|
|
+\begin{equation}\label{eq:p17-A-stroke-stroke}\tag{A$''$}
|
|
|
+\mathit{a}<\mathit{b}\OLimpl\mathit{a}\neq\mathit{b}\text{.}
|
|
|
+\end{equation}
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+%% ======================= Страница 72 =======================
|
|
|
+
|
|
|
+Общее правило для сокращения <<$\neq$>> позволяет нам
|
|
|
+писать~<<${\mathrm{s}\neq\mathrm{t}}$>> как сокращение
|
|
|
+для~${\neg\mathrm{s}=\mathrm{t}}$‚ где $\mathrm{s}$~и~$\mathrm{t}$~---~термы.
|
|
|
+Общее правило для сокращения~<<$<$>> позволяет нам
|
|
|
+писать~<<${\mathrm{s}<\mathrm{t}}$>> как сокращение
|
|
|
+для~${\exists\mathrm{x}\left(\mathrm{x}'+\mathrm{s}=\mathrm{t}\right)}$‚
|
|
|
+где $\mathrm{x}$~---~переменная, а $\mathrm{s}$~и~$\mathrm{t}$~---~термы, не
|
|
|
+содержащие~$\mathrm{x}$. При восстановлении сокращения, если оно было связано с
|
|
|
+опусканием переменной, как в случае~<<$<$>>, имеется произвол в отношении выбора
|
|
|
+подлежащей восстановлению переменной. Так, при
|
|
|
+восстановлении~<<${\mathrm{s}<\mathrm{t}}$>> мы можем выбрать в
|
|
|
+качестве~$\mathrm{x}$ любую переменную, не содержащуюся
|
|
|
+в~$\mathrm{s}$~и~$\mathrm{t}$. Этот произвол является мало существенным,
|
|
|
+поскольку утверждения, которые мы собираемся делать о сокращённой формуле, имеют
|
|
|
+место независимо от выбора допустимой переменной.
|
|
|
+
|
|
|
+Мы будем считать, что все эти сокращения относятся только к изложению
|
|
|
+метаматематики. Это соответствует нашим целям, и таким путём мы сохраняем
|
|
|
+теоретически более простые основные определения, посредством которых
|
|
|
+устанавливается формальная система. Метаматематические утверждения о термах и
|
|
|
+формулах системы должны поэтому рассматриваться как относящиеся к несокращённым
|
|
|
+выражениям в буквальном смысле определений, какого бы рода стенографией мы ни
|
|
|
+пользовались при записи этих утверждении.
|
|
|
|
|
|
\section{Свободные и связанные переменные}
|
|
|
\label{sec:18-free_and_bound_variables}
|
|
|
|
|
|
+Вхождение переменной~$\mathrm{x}$ в формулу~$\mathrm{A}$ называется
|
|
|
+\emph{связанным} (или вхождением в качестве \emph{связанной переменной}), если
|
|
|
+оно является вхождением в квантор~${\forall\mathrm{x}}$
|
|
|
+или~${\exists\mathrm{x}}$ или в область действия квантора~${\forall\mathrm{x}}$
|
|
|
+или~${\exists\mathrm{x}}$ (с тем же самым~$\mathrm{x}$); в противном случае
|
|
|
+вхождение называется \emph{свободным} (или вхождением в качестве
|
|
|
+\emph{свободной переменной}).
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex1.}{exmpl:p18-1}{exmpl:p18-1}
|
|
|
+В~${
|
|
|
+\exists\mathit{c}
|
|
|
+\left(\mathit{c}'+\mathit{a}=\mathit{b}\right)
|
|
|
+\OLimpl\neg\mathit{a}=\mathit{b}}$‚ оба вхождения~$\mathit{a}$ и оба
|
|
|
+вхождения~$\mathit{b}$~---~свободные‚ а оба
|
|
|
+вхождения~$\mathit{c}$~---~связанные. В~${
|
|
|
+\exists\mathit{c}
|
|
|
+\left(\mathit{c}'+\mathit{a}=\mathit{b}\right)
|
|
|
+\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}}$ первые два
|
|
|
+вхождения~$\mathit{c}$~---~связанные, а третье~---~свободное.
|
|
|
+В~${
|
|
|
+\exists\mathit{c}\left(
|
|
|
+ \exists\mathit{c}\left(
|
|
|
+ \mathit{c}'+\mathit{a}=\mathit{b}
|
|
|
+ \right)\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}
|
|
|
+\right)}$ все вхождения~$\mathit{c}$~---~связанные.
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+Мы будем говорить также, что любое вхождение переменной~$\mathrm{x}$ в
|
|
|
+терм~$\mathrm{t}$ является \emph{свободным}, как это будет следовать из
|
|
|
+приведённого определения, если заменить в нем слова <<формула~$\mathrm{A}$>>
|
|
|
+на <<терм~$\mathrm{t}$>>. Различие между свободным и связанным вхождением
|
|
|
+переменной всегда связано с термом или формулой, для которых (в каждом случае)
|
|
|
+рассматривается это вхождение.
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex2.}{exmpl:p18-2}{exmpl:p18-2}
|
|
|
+Третье вхождение~$\mathit{c}$ в~${
|
|
|
+\exists\mathit{c}\left(
|
|
|
+ \exists\mathit{c}\left(
|
|
|
+ \mathit{c}'+\mathit{a}=\mathit{b}
|
|
|
+ \right)\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}
|
|
|
+\right)}$ является свободным, если его рассматривать как вхождение в саму эту
|
|
|
+часть~$\mathit{c}$, или в часть~${\mathit{c}'}$, или в
|
|
|
+часть~${\mathit{c}'+\mathit{a}}$‚ или в
|
|
|
+часть~${\mathit{c}'+\mathit{a}=\mathit{b}}$, и связанным, если его рассматривать
|
|
|
+как вхождение в часть~${
|
|
|
+\exists\mathit{c}\left(
|
|
|
+ \mathit{c}'+\mathit{a}=\mathit{b}
|
|
|
+\right)}$‚ или в часть~${
|
|
|
+\exists\mathit{c}\left(
|
|
|
+ \mathit{c}'+\mathit{a}=\mathit{b}
|
|
|
+\right)\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}}$, или во всю формулу.
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+Если переменная~$\mathrm{x}$ входит в качестве свободной переменной (коротко:
|
|
|
+входит свободно) в~$\mathrm{A}$, то говорят, что $\mathrm{x}$~является
|
|
|
+\emph{свободной переменной} выражения~$\mathrm{A}$, или что
|
|
|
+$\mathrm{A}$~\emph{содержит}~$\mathrm{x}$ \emph{в качестве свободной
|
|
|
+переменной} (коротко: $\mathrm{A}$~\emph{содержит свободно}~$\mathrm{x}$);
|
|
|
+аналогично для связанных переменных.
|
|
|
+
|
|
|
+\begin{SCEnvWLabel}{Пример\kern1ex3.}{exmpl:p18-3}{exmpl:p18-3}
|
|
|
+Свободные переменные в~${
|
|
|
+\exists\mathit{c}\left(
|
|
|
+ \mathit{c}'+\mathit{a}=\mathit{b}
|
|
|
+\right)\OLimpl\neg\mathit{a}=\mathit{b}+\mathit{c}
|
|
|
+}$ суть~$\mathit{a}$,~$\mathit{b}$~и~$\mathit{c}$, а единственная связанная
|
|
|
+переменная есть~$\mathit{c}$.
|
|
|
+\end{SCEnvWLabel}
|
|
|
+
|
|
|
+Связанное вхождение переменной~$\mathrm{x}$ в формулу~$\mathrm{A}$ связано
|
|
|
+\emph{тем} вхождением квантора~${\forall\mathrm{x}}$ или~~${\exists\mathrm{x}}$
|
|
|
+(с тем же самым~$\mathrm{x}$), в области действия которого
|
|
|
+%% ======================= Страница 73 =======================
|
|
|
+
|
|
|
+
|
|
|
stub
|
|
|
|
|
|
\section{Правила преобразования}
|
