«Principia Mathematica, том 2»

PRINCIPIA MATHEMATICA

ИЗДАТЕЛЬСТВО КЕМБРИДЖСКОГО УНИВЕРСИТЕТА Лондон : FETTER LANE, E.C. К. Ф. КЛЕЙ, УПРАВЛЯЮЩИЙ

Эдинбург : 100, PRINCES STREET Берлин : A. ASHER AND CO. Лейпциг : F. A. BROCKHAUS Нью-Йорк : G. P. PUTNAM'S SONS Бомбей и Калькутта : MACMILLAN AND CO., LTD.

Все права защищены

PRINCIPIA MATHEMATICA

АВТОРЫ:

АЛЬФРЕД НОРТ УАЙТХЕД, доктор естественных наук, член Королевского общества

Член и бывший лектор Тринити-колледжа, Кембридж

И

БЕРТРАН РАССЕЛ, магистр искусств, член Королевского общества

Лектор и бывший член Тринити-колледжа, Кембридж

ТОМ II

Кембридж в Издательстве университета 1912

Кембридж : ОТПЕЧАТАНО ДЖОНОМ КЛЕЕМ, магистром искусств В ИЗДАТЕЛЬСТВЕ УНИВЕРСИТЕТА

СОДЕРЖАНИЕ ТОМА II

PAGE

PREFATORY STATEMENT OF SYMBOLIC CONVENTIONS ix

PART III. CARDINAL ARITHMETIC.

Summary of Part III 3

SECTION A. DEFINITION AND LOGICAL PROPERTIES OF CARDINAL NUMBERS 4

*100. Definition and elementary properties of cardinal numbers 13

*101. On 0 and 1 and 2 19

*102. On cardinal numbers of assigned types 24

*103. Homogeneous cardinals 36

*104. Ascending cardinals 42

*105. Descending cardinals 52

*106. Cardinals of relational types 60

SECTION B. ADDITION, MULTIPLICATION AND EXPONENTIATION 66

*110. The arithmetical sum of two classes and of two cardinals 75

*111. Double similarity 88

*112. The arithmetical sum of a class of classes 97

*113. On the arithmetical product of two classes or of two cardinals 105

*114. The arithmetical product of a class of classes 124

*115. Multiplicative classes and arithmetical classes 135

*116. Exponentiation 143

*117. Greater and less 171

General note on cardinal correlators 185

SECTION C. FINITE AND INFINITE 187

*118. Arithmetical substitution and uniform formal numbers 193

*119. Subtraction 201

*120. Inductive cardinals 207

*121. Intervals 233

*122. Progressions 253

*123. 268

*124. Reflexive classes and cardinals 278

*125. The axiom of infinity 289

*126. On typically indefinite inductive cardinals 293

PART IV. RELATION-ARITHMETIC.

Summary of Part IV 301

SECTION A. ORDINAL SIMILARITY AND RELATION-NUMBERS 303

*150. Internal transformation of a relation 306

*151. Ordinal similarity 319

*152. Definition and elementary properties of relation-numbers 330

*153. The relation-numbers , and 334

*154. Relation-numbers of assigned types 339

*155. Homogeneous relation-numbers 344

SECTION B. ADDITION OF RELATIONS, AND THE PRODUCT OF TWO RELATIONS 347

*160. The sum of two relations 351

*161. Addition of a term to a relation 357

*162. The sum of the relations of a field 362

*163. Relations of mutually exclusive relations 369

*164. Double likeness 376

*165. Relations of relations of couples 386

*166. The product of two relations 396

SECTION C. THE PRINCIPLE OF FIRST DIFFERENCES, AND THE MULTIPLICATION AND EXPONENTIATION OF RELATIONS 403

*170. On the relation of first differences among the sub-classes of a given class 411

*171. The principle of first differences (continued) 423

*172. The product of the relations of a field 428

*173. The product of the relations of a field (continued) 443

*174. The associative law of relational multiplication 447

*176. Exponentiation 458

*177. Propositions connecting with products and powers 471

SECTION D. ARITHMETIC OF RELATION-NUMBERS 473

*180. The sum of two relation-numbers 477

*181. On the addition of unity to a relation-number 482

*182. On separated relations 487

*183. The sum of the relation-numbers of a field 496

*184. The product of two relation-numbers 501

*185. The product of the relation-numbers of a field 505

*186. Powers of relation-numbers 507

PART V. SERIES.

Summary of Part V. 513

SECTION A. GENERAL THEORY OF SERIES 516

*200. Relations contained in diversity 518

*201. Transitive relations 525

*202. Connected relations 533

*204. Elementary properties of series 547

*205. Maximum and minimum points 559

*206. Sequent points 577

*207. Limits 594

*208. The correlation of series 605

SECTION B. ON SECTIONS, SEGMENTS, STRETCHES, AND DERIVATIVES 612

*210. On series of classes generated by the relation of inclusion 615

*211. On sections and segments 624

*212. The series of segments 651

*213. Sectional relations 668

*214. Dedekindian relations 684

*215. Stretches 691

*216. Derivatives 700

*217. On segments of sums and converses 710

SECTION C. ON CONVERGENCE, AND THE LIMITS OF FUNCTIONS 715

*230. On convergents 720

*231. Limiting sections and ultimate oscillation of a function 727

*232. On the oscillation of a function as the argument approaches a given limit 737

*233. On the limits of functions 745

*234. Continuity of functions 753

ДОПОЛНИТЕЛЬНЫЕ ОПЕЧАТКИ К ТОМУ I.

стр. 5, строка 20, удалить "." стр. 34, строка 20, вместо " " читать "." стр. 36, строка 7 и строка 10, вместо " " читать "." стр. 44, строка 17, вместо " " читать "." стр. 112, в *2·52, вместо " " читать "." стр. 129, в *5·11, вместо ссылки на " " читать ссылку на "." стр. 129, в *5·12, вместо ссылки на " " читать ссылку на "*2·51." стр. 144, *10·23 должно быть "." стр. 157, строка 11, вместо "*10" читать "*9." стр. 184, последняя строка доказательства *14·111, вместо второго " " читать "." стр. 228, в *23·81, вместо " " читать "." стр. 242, в *25·37, вместо " " читать "." стр. 242, в *25·412, вместо " " читать "." стр. 253, 2-я и 4-я строки доказательства *31·16, вместо "*21·35" читать "*23·35." стр. 259, в примечании к *32·35, вместо "*32·2" читать "*32·3." стр. 263, в *33·16, 4-я строка доказательства, вместо "*20·34" читать "*22·34." стр. 265, в *33·26, 2-я строка доказательства, вместо "*21·34" читать "*23·34." стр. 275, в *34·6, 4-я строка доказательства, вместо первого " " читать "." стр. 289, 1-я строка, вместо " " читать "." стр. 322, в *40·18, формулировка, вместо " " читать "." стр. 329, в *40·69, доказательство, вместо " " читать " " (3 раза). стр. 387, в *55·224, 1-я строка доказательства, вместо " " читать " " (дважды). стр. 388, в *55·281, вместо третьего " " читать "." стр. 410, в *60·53, последняя строка доказательства, вместо " " читать "." стр. 453, в *71·25, доказательство, 1-я строка, вместо " " читать "." 2-я строка, вместо " " читать "." 3-я строка, вместо " " читать "." 6-я строка, вместо " " читать " " и вместо " " читать "." 7-я строка, вместо " " читать "." стр. 465, в *72·16, доказательство, 1-я строка, вместо последнего " " читать "." стр. 483, в *73·44, доказательство, 1-я строка, вместо второго " " читать "." стр. 485, в *73·511, вместо " " читать "." стр. 522, в *81·23, формулировка и 2-я строка доказательства, вместо " " читать "." стр. 592, в *91·33, доказательство, 1-я строка, вместо " " читать "." стр. 614, в *93·36, доказательство, вместо " " читать " " повсеместно. стр. 628, в *95·21, доказательство, строка 6, вместо " " читать "."

ОПЕЧАТКИ К ТОМУ II

стр. 82, предпоследняя строка, вместо " " и " " читать " " и "." стр. 101, *112·23, формулировка, во втором случае, где встречаются две точки, читать одну точку. стр. 573, *205·7, формулировка, вместо " " читать "."

ПРЕДИСЛОВИЕ К СИМВОЛИЧЕСКИМ УСЛОВНЫМ ОБОЗНАЧЕНИЯМ

ЦЕЛЬ следующих замечаний состоит в том, чтобы собрать воедино в рамках одного обсуждения различные пояснения, необходимые при применении теории типов к кардинальной арифметике. Удобно собрать эти замечания, поскольку в противном случае их разбросанность по различным номерам Части III затрудняет понимание их совокупного эффекта. Но хотя мы поместили эти замечания в начале, их следует читать одновременно с текстом Части III, по крайней мере с той частью текста, которая состоит из пояснений к определениям. Ранняя часть того, что следует ниже, является лишь резюме предыдущих пояснений; только в более поздних частях осуществляется применение к кардинальной арифметике.

I. Общие замечания о типах.

В наших предложениях задействованы три различных вида типической двусмысленности, касающиеся:

(1) функциональной иерархии,

(2) пропозициональной иерархии,

(3) экстенсиональной иерархии.

Значимость этих аспектов должна рассматриваться отдельно.

Мы часто говорим так, как будто тип, представленный малыми латинскими буквами, не состоит из функций. Однако это совместимо со всем, что мы должны сказать, что он может состоять из функций. Далее следует отметить, что при заданном числе индивидов в наших аксиомах нет ничего, что показывало бы, сколько существует предикативных функций индивидов, т.е. их число не является функцией от числа индивидов: мы знаем только, что их число , где " " обозначает класс индивидов.

На практике мы движемся вдоль экстенсиональной иерархии после начальных номеров книги. Если мы начали с индивидов, то результатом этого является полное исключение функций из нашей иерархии; если мы начали с функций заданного типа, то все функции других типов исключаются. Таким образом, новая экстенсиональная иерархия, полностью исключающая любую другую, начинается с каждого типа функций. Когда мы говорим просто об "экстенсиональной иерархии", мы имеем в виду ту, которая начинается с индивидов.

Следует отметить, что когда мы имеем утверждение пропозициональной функции, скажем " ", то должно быть некоторого определенного типа, т.е. мы утверждаем лишь то, что истинно, что бы ни было в рамках одного типа. Таким образом, например, " " не утверждает большего, чем то, что это утверждение справедливо для любого из заданного типа. Верно, что символически то же самое утверждение справедливо и в других типах, но другие типы не могут быть включены под один знак утверждения, поскольку ни одна переменная не может выйти за пределы своего типа.

Процесс придания типам переменных двусмысленности начинается в *9, где мы делаем первый шаг в отношении пропозициональной иерархии. До *9 нашими переменными являются элементарные предложения. Они таковы, что не содержат кажущихся переменных. Следовательно, единственные функции, которые встречаются, — это матрицы, и они встречаются только через свои значения. Предположение, задействованное при переходе от Раздела A к Разделу B (Часть I), заключается в том, что, имея " ", где есть элементарное предложение, мы можем подставить вместо " ", где есть любая матрица. Таким образом, вместо " ", которое содержало одну переменную заданного типа, мы имеем " ", которое содержит несколько переменных нескольких типов (возможно любое конечное число переменных и типов). Это предположение включает в себя некоторые довольно сложные моменты. Следует помнить, что никакое значение не содержит в качестве составляющей, и поэтому не является составляющей даже если является значением . Таким образом, мы переходим выше от утверждения, не содержащего функцию в качестве составляющей, к утверждению, содержащему одну или несколько функций в качестве составляющих. Утверждение " " касается любого элементарного предложения, тогда как " " касается любого из определенного набора элементарных предложений, а именно любого из тех, которые являются значениями . Различные типы функций дают различные способы выделения элементарных предложений.

Приняв или доказав " ", где элементарно и, следовательно, не предполагает никакой двусмысленности типа, мы таким образом утверждаем , где типы аргументов и их количество совершенно произвольны, за исключением того, что они должны принадлежать к функциональной иерархии, включающей индивидов. (Предположение о том, что предложения являются неполными символами, исключает возможность того, что аргументами для являются предложения.) Примечательным моментом является то, что мы таким образом получаем утверждение, в котором может быть любое конечное число переменных и переменные имеют неограниченную типическую двусмысленность, исходя из утверждения, содержащего одну переменную совершенно определенного типа. Все это предполагается до того, как мы приступим к пропозициональной иерархии.

Следует отметить, что все элементарные предложения являются значениями предикативных функций одного индивида, т.е. , где есть индивид. Таким образом, нам не нужно предполагать, что элементарные предложения образуют тип; мы можем заменить на " " в " ". Таким образом, предложения как переменные полностью исчезают.

При расширении утверждений, касающихся элементарных предложений, чтобы формально применить их к предложениям первого порядка, мы должны заново принять примитивное предложение *1·11 (*1·1 никогда не используется), т.е. имея " " и " ", мы имеем " ", что практически является *9·12. Это было утверждено в *1·11 для любого случая, в котором и являются элементарными предложениями. Здесь уже существовала двусмысленность типа, обусловленная тем фактом, что x не обязательно должен быть индивидом, а может быть функцией любого порядка. Например, мы могли бы использовать *1·11 для перехода от , где заменяет из *1·11, а , заменяют и . Таким образом, *1·11, даже до своего расширения в *9, уже формулирует новое примитивное предложение для каждого нового рассматриваемого типа функций. Новизна в *9 заключается в том, что мы позволяем и содержать одну кажущуюся переменную. Она может быть любого функционального типа (включая Indiv); таким образом, мы получаем еще один набор символически идентичных примитивных предложений. Переходя, как указано в конце *9, к более чем одной кажущейся переменной, мы вводим новую порцию примитивных предложений с каждой дополнительной кажущейся переменной.

Аналогичные замечания применимы и к другим примитивным предложениям *9.

То, что делает вышеуказанный процесс законным, заключается в том, что ничто в трактовке функций порядка не предполагает функций более высокого порядка. Мы можем иметь дело с каждым новым типом функций по мере его возникновения, не принимая во внимание тот факт, что существуют более поздние типы. Из символической аналогии мы "видим", что процесс может повторяться бесконечно. Эта возможность основывается на двух вещах:

(1) Новая интерпретация наших констант— , , !, ( )., ( ).—на каждом новом этапе;

(2) Новое предположение, символически неизменное, примитивных предложений, которые мы сочли достаточными на более раннем этапе — возможность избежать символического изменения обусловлена новой интерпретацией наших констант.

Вышеуказанные замечания применимы как к аксиоме сводимости, так и к другим нашим примитивным предложениям. Если на каком-либо этапе мы хотим иметь дело с классом, определенным функцией 30 000-го типа, нам придется повторять наши аргументы и предположения 30 000 раз. Но все еще нет необходимости говорить об иерархии в целом или предполагать, что утверждения могут быть сделаны обо "всех типах".

Теперь мы переходим к экстенсиональной иерархии. Она начинается с какой-то одной точки в функциональной иерархии. Мы обычно предполагаем, что она начинается с индивидов, но любая другая отправная точка столь же законна. С какого бы типа функций (включая ) мы ни начали, все более высокие типы функций исключаются из экстенсиональной иерархии, а также все более низкие типы (если таковые имеются). Здесь возникают некоторые сложности. Предположим, мы начинаем с . Тогда, если есть любая предикативная функция индивидов, . Но тождество между функцией и классом не обладает обычными свойствами тождества; на самом деле, хотя каждая функция тождественна некоторому классу, и наоборот, число функций, вероятно, больше, чем число классов. Это связано с тем фактом, что мы можем иметь , не имея .

В экстенсиональной иерархии мы доказываем расширение от классов к классам классов и так далее, без новых примитивных предложений (*20, *21). Задействованные примитивные предложения — это те, которые касаются функциональной иерархии.

Из всех этих различных способов расширения мы "видим", что все, что может быть доказано для более низких типов, будь то функциональных или экстенсиональных, может быть также доказано для более высоких типов [1]. Следовательно, мы предполагаем, что нет необходимости знать типы наших переменных, хотя они всегда должны быть ограничены каким-то одним определенным типом.

Теперь, хотя все, что может быть доказано для более низких типов, может быть доказано для более высоких типов, обратное неверно. В Том I встречаются только два предложения, которые могут быть доказаны для более высоких, но не для более низких типов. Это и . Они могут быть доказаны для любого типа, кроме типа индивидов. Следует отметить, что мы не утверждаем, что все, что истинно для более низких типов, истинно для более высоких типов, а только то, что все, что может быть доказано для более низких типов, может быть доказано для более высоких типов. Если, например, , то это предложение ложно для любого более высокого типа; но это предложение, , является тем, которое не может быть доказано логически; на самом деле, оно устанавливается только переписью, а не логикой. Таким образом, среди предложений, которые могут быть доказаны логикой, есть некоторые, которые могут быть доказаны только для более высоких типов, но нет таких, которые могут быть доказаны только для более низких типов.

Предложения, которые могут быть доказаны в одних типах, но не в других, все являются или зависят от теорем существования для кардинальных чисел. Мы можем доказать . Совершенно аналогичные замечания применимы и к функциональной иерархии. В обоих случаях возможность доказательства этих предложений зависит от аксиомы сводимости и определения тождества. Предположим, существует только один индивид, . Тогда , — это две разные функции, которые, согласно аксиоме сводимости, эквивалентны двум разным предикативным функциям. Следовательно, существуют по крайней мере две предикативные функции от , и по крайней мере два класса , . Этот аргумент не работает ни для классов, ни для функций, если мы либо отрицаем аксиому сводимости, либо предполагаем, что могут существовать два разных индивида, которые согласуются во всех своих предикатах, т.е. что определение тождества вводит в заблуждение.

Утверждение, что то, что может быть доказано для более низких типов, может быть доказано для более высоких типов, требует определенных ограничений, или, скорее, более точной формулировки. Принимая в качестве примитивной идеи, положим . Затем рассмотрим предложение . Мы можем доказать . Таким образом, может быть доказано в самом низком типе, в котором оно значимо, и опровергнуто в любом другом. Сложность, однако, устраняется, если Indiv заменить на переменную , а на . Тогда мы имеем , и это справедливо независимо от того, каким может быть тип . Таким образом, чтобы наш принцип о более низких и более высоких типах был верным, необходимо, чтобы любое отношение, которое может существовать между двумя типами, встречающимися в предложении, сохранялось; другими словами, когда один постоянный тип определяется через другой (как и ), определение должно быть восстановлено до того, как тип будет изменен, так что когда один тип изменяется, изменяется и другой. С этой оговоркой наш принцип о более высоких и более низких типах остается в силе.

С вышеуказанной оговоркой истинность нашего утверждения очевидна. Ибо мы показали, что те же самые примитивные предложения, символически, которые справедливы для самого низкого типа, задействованного в наших рассуждениях, справедливы также и для последующих типов; и поэтому все наши доказательства могут быть повторены символически без изменений.

Важность этого заключается в том факте, что, доказав предложение для самого низкого значимого типа, мы "видим", что оно справедливо в любом другом назначенном значимом типе. Следовательно, каждое предложение, которое доказано без упоминания какого-либо типа, должно рассматриваться как доказанное для самого низкого значимого типа и расширенное по аналогии на любой другой значимый тип.

Совершенно аналогичными соображениями мы "видим", что предложение, которое может быть доказано для некоторого типа, отличного от самого низкого значимого типа, должно быть справедливо для любого типа в прямом происхождении от него. Например, предположим, что мы можем доказать предложение (такое как ) для типа (где ); тогда, просто написав вместо , мы имеем предложение, которое доказано относительно , а именно , и здесь, согласно тому, что было сказано ранее, может быть заменено любым более высоким типом.

Таким образом, имея типически двусмысленное отношение , такое что, если есть тип, есть тип ( или есть такое отношение), мы "видим", что если мы можем доказать , мы можем также доказать , где есть любой тип, и состоит из типически двусмысленных символов. Аналогично, если мы можем доказать , мы можем доказать , где есть любой тип. Но мы не можем в общем случае доказать или , и они могут быть на самом деле неверными. Например, мы имеем .

Таким образом, более общо, когда предложение, содержащее несколько двусмысленностей, может быть доказано для типов , , ..., но не для более низких типов, оно должно рассматриваться как функция от , и тогда оно становится истинным для любого типа; то есть, имея , мы также будем иметь , где есть любой тип. Таким образом, все доказуемые предложения в первую очередь касаются , и при таком выражении остаются истинными, если любой другой тип подставлен вместо .

Когда предложение, содержащее типически двусмысленные символы, может быть доказано как истинное в самом низком значимом типе, и мы можем "видеть", что символически то же самое доказательство справедливо в любом другом назначенном типе, мы говорим, что предложение обладает "постоянной истинностью". (Мы можем также сказать, нестрого, что оно "истинно во всех типах".) Когда предложение, содержащее типически двусмысленные символы, может быть доказано как ложное в самом низком значимом типе, и мы можем "видеть", что оно ложно в любом другом назначенном типе, мы говорим, что оно обладает "постоянной ложностью". Любое другое предложение, содержащее типически двусмысленные символы, называется "флуктуирующим" или обладающим "флуктуирующим истинностным значением", в противоположность "постоянному истинностному значению", которое принадлежит предложениям, обладающим либо постоянной истинностью, либо постоянной ложностью.

В дальнейшем двусмысленности, касающиеся пропозициональной иерархии, будут игнорироваться, поскольку они никогда не приводят к флуктуирующим предложениям. Таким образом, дизъюнкция, отрицание и их производные не получат явного типического определения, а только такое типическое определение, которое вытекает из назначения типов других задействованных типически двусмысленных символов.

Удобно называть символическую форму пропозициональной функции просто "символической формой". Таким образом, если символическая форма содержит символы двусмысленного типа, она представляет различные пропозициональные функции в зависимости от того, как настроены типы ее двусмысленных символов. Настройка, конечно, всегда ограничена необходимостью сохранения смысла. Очевидно, что идеи "постоянного истинностного значения" и "флуктуирующего истинностного значения" в действительности применимы к символическим формам, а не к предложениям или пропозициональным функциям. Двусмысленность типа может существовать только в процессе определения смысла. Когда смысл был присвоен символической форме и тем самым получена пропозициональная функция, всякая двусмысленность типа исчезает.

Утверждать "символическую форму" — значит утверждать каждую из пропозициональных функций, возникающих для набора возможных типических определений, которые где-то перечисляются. Мы, по сути, перечислили очень ограниченное число типов, начиная с типа индивидов, и мы "видим", что этот процесс может быть бесконечно продолжен по аналогии. Форма всегда утверждается постольку, поскольку перечисление достигло цели; и этого достаточно для всех целей, поскольку по существу невозможно использовать тип, который не был достигнут путем последовательного перечисления от более низких типов.

Единственные трудности, которые возникают в кардинальной арифметике в связи с двусмысленностями типа символов, — это те, которые входят через использование символа , или символа , который есть . Ибо может случиться так, что класс в одном типе не имеет подобного ему класса в каком-то более низком типе (ср. *102·72 ·73). Все ошибочные рассуждения в кардинальной или ординальной арифметике в связи с типами, помимо тех, что обусловлены простым отсутствием смысла в символах, обусловлены этим фактом — другими словами, тем фактом, что в одних типах истинно, а в других типах может быть не истинно. Ошибка состоит в пренебрежении этой последней возможностью невыполнения для ограниченного числа типов, то есть в принятии "флуктуирующей" формы так, как если бы она обладала "постоянным" истинностным значением.

Флуктуирующая форма, однако, часто обладает тем, что здесь называется "стабильным" истинностным значением, которое столь же важно, как и постоянное истинностное значение других форм. Например, предвосхищая наши определения элементарной арифметики, рассмотрим . Не существует абстрактного логического доказательства того, что существуют два индивида; поэтому предположим, что 2 и 3 относятся к классам индивидов, но 5 относится к классам достаточно высокого типа, тогда с этими определениями нельзя доказать. Но обладает стабильным истинностным значением, поскольку его всегда можно доказать, когда все типы достаточно высоки. В этом случае тот факт, что наша эмпирическая перепись индивидов (по крайней мере, "относительных" индивидов обычной жизни) опередила возможности логического доказательства, делает флуктуацию истинностного значения формы совершенно неважной.

Чтобы сделать эту идею точной, необходимо иметь конвенцию относительно порядка, в котором назначаются типы символов в символической форме. Правило, которое мы принимаем, состоит в том, что типы реальных переменных должны быть назначены первыми, а затем типы константных символов. Типы кажущихся переменных, если таковые имеются, будут тогда полностью определены.

Символическая форма обладает стабильным истинностным значением, если после любого назначения типов реальным переменным могут быть назначены типы константным символам так, чтобы истинностное значение полученного таким образом предложения было таким же, как истинностное значение любого предложения, полученного путем его модификации назначением более высоких типов некоторым или всем константным символам. Это истинностное значение является стабильным истинностным значением.

II. Формальные числа.

Конвенции, которые мы приведем ниже относительно назначения типов, практически ограничивают нашу интерпретацию флуктуирующих символических форм типами, в которых формы обладают своим стабильным истинностным значением. Предположение о том, что эти истинностные значения стабильны, никогда не входит в рассуждение. Но мы судим об истинностном значении как о стабильном, когда любой метод повышения типов константных символов на один шаг оставляет его неизменным.

На практике флуктуация истинностных значений входит в наше рассмотрение только через ограниченное число символов, называемых "формальными числами".

Формальные числа могут быть "константными" или "функциональными".

Константное формальное число — это любой константный символ, для которого существует константа такая, что, в каком бы типе ни был определен константный символ, он в этом типе тождественен . Другими словами, если есть константный символ, то есть формальное число при условии, что "истина" является постоянным истинностным значением для некоторой константы .

Функциональные формальные числа определяются перечислением; они суть , где в каждом формальном числе символы , , , встречающиеся в нем, называются аргументами функциональной формы, даже когда они являются сложными символами. Аргументом является , а аргументами являются и , а аргументами являются 1 и 2.

Таким образом, среди константных формальных чисел находятся . Ссылки, подтверждающие это утверждение, суть *101·11 ·21 ·32. *123·36. *110·42. *113·23. *116·23.

Среди функциональных формальных чисел находятся . Будет замечено, что, например, является как константным, так и функциональным формальным числом, так что эти два класса не являются взаимоисключающими. На самом деле они обладают неопределенным числом общих членов.

Все формальные числа, за исключением и , являются членами без какой-либо гипотезы [ср. *100·41 ·01. *110·42. *112·101. *113·23. *114·1. *116·23, примечание к *119·12, и *120·411].

Функциональное формальное число состоит из двух частей, а именно: его аргумента или аргументов и константной "формы". Аргумент функционального формального числа может быть сложным символом и может быть константным или переменным. Таким образом, есть аргумент , и ( , и ( ; также есть аргумент ( . Константная форма образована другими символами, которые являются константами. Два вхождения функциональных формальных чисел являются вхождениями одного и того же формального числа только в том случае, если аргументы, а также константные формы идентичны в символике. Таким образом, два вхождения являются вхождениями одного и того же формального числа, даже если они определены как находящиеся в разных типах; но и являются разными формальными числами. Также и являются разными формальными числами, потому что их "формы" различны, хотя аргументы и 1 одинаковы и (в одном и том же типе) обозначаемая сущность одна и та же. Таким образом, различие между формальными числами зависит от символики, а не от обозначаемой сущности, и при их рассмотрении следует принимать во внимание символическую аналогию, а не денотацию. Например, два разных вхождения одного и того же формального числа не будут обозначать одну и ту же сущность, если в двух вхождениях двусмысленность типа определена по-разному.

Функциональные формальные числа делятся на три набора: (i) первичный набор, состоящий из форм , , , (ii) аргументальный набор, состоящий только из , (iii) арифметический набор, состоящий из , , , и .

Функциональное формальное число имеет не более двух аргументов. Но аргумент функционального формального числа может сам быть функциональным формальным числом и, соответственно, будет обладать одним или двумя аргументами, которые, в свою очередь, могут быть функциональными формальными числами, и так далее. Весь набор аргументов и аргументов аргументов, полученный таким образом, называется набором компонентов исходного формального числа. Таким образом, , , , и являются компонентами ( ; а , и являются компонентами ; а , и являются компонентами . Два аргумента ( суть и , а аргументы суть и , а аргументы суть и .

Сложение, умножение, возведение в степень и вычитание будут называться арифметическими операциями; и в , , , , и каждый будет, как говорят, подвергнут этим соответствующим операциям. Арифметические компоненты арифметического формального числа (т.е. принадлежащего к арифметическому набору) состоят из тех его компонентов, которые не выступают в качестве компонентов компонента, не принадлежащего к арифметическому набору. Таким образом, , , , являются арифметическими компонентами ; а и являются арифметическими компонентами , но не является таковым; а и являются арифметическими компонентами , но не является таковым; а и являются арифметическими компонентами , но и и являются компонентами и поэтому не являются арифметическими компонентами . Только арифметические формальные числа обладают арифметическими компонентами.

Формальное число арифметического набора, не имеющее компонентов, которые являются формальными числами аргументального набора, называется чистым арифметическим формальным числом. Например, и являются чистыми, но и не являются чистыми.

При рассмотрении формального числа задействовано много типов. Например, в есть тип и ; в есть тип , тип и тип ; и так далее для более сложных формальных чисел. Тип формального числа в целом в любом вхождении называется его актуальным типом. Это тип сущности, которую оно тогда представляет.

Другие типы, задействованные в формальном числе в любом вхождении, называются его подчиненными типами.

Актуальные типы не указаны в символике для различных формальных чисел, как указано выше. Они могут быть указаны относительно типа переменной путем написания , , ( , ( , ( , с помощью нотации *65. Даже когда актуальный тип сложного формального числа, такого как , установлен — так, например, что мы имеем — смысл символа не полностью определен, ибо тип остается двусмысленным. Однако из

*100·511. *110·23. *113·26. ·62, следует, что подчиненные типы не имеют значения для величины формального числа, пока компоненты не являются нулевыми.

Поэтому мы можем сделать формальное число определенным, как только его актуальный тип станет определенным, обеспечив, чтобы его компоненты не были нулевыми. Это делается с помощью конвенции II T (ниже) в сочетании с определениями *110·03 ·04. *113·04 ·05. *116·03 ·04. Когда подчиненные типы настроены в соответствии с этими определениями и конвенциями, они будут называться нормально настроенными.

Но чтобы сформулировать эту конвенцию, нам требуется определение того, что здесь называется адекватностью актуального типа формального числа. Общая идея адекватности достаточно проста, а именно: при заданных подчиненных типах , актуальный тип должен быть достаточно высоким, чтобы позволить нам логически доказать , когда такое доказательство возможно для типов, которые не слишком низки. Например, все типы, кроме самого низкого, для которого оно имеет смысл, являются адекватными для константного формального числа 2. Однако довольно трудно точно сформулировать значение адекватности способом, приспособленным ко всем формальным числам. К счастью, определение самого низкого типа, который соответствует этой общей идее адекватности, не важно для наших целей. Будет достаточно определить как адекватные некоторые типы, которые, безусловно, обладают рассматриваемым свойством.

Метод определения, который мы принимаем, состоит в замене формального числа на другое , так связанное с , что при одном и том же актуальном типе для обоих мы можем доказать , всякий раз, когда не равно в всех типах. Если функционально, нам нужно рассмотреть только его аргумент или его два аргумента, и мы можем отбросить из рассмотрения другие компоненты; затем мы заменяем эти аргументы другими так, чтобы имел требуемое свойство. Таким образом:

(i) Актуальные типы , , , и адекватны, когда мы можем логически доказать

(ii) Актуальные типы , , , и адекватны, когда мы можем логически доказать

Будет замечено, что , , и являются наибольшими классами того же типа, что и , , и соответственно, и что и являются наибольшими кардинальными числами того же типа, что и и соответственно. Эти определения справедливы, даже когда любой из , , , является сложным символом.

Оставшиеся формальные числа, которые не являются функциональными, должны, безусловно, быть константными. Трудность, которая здесь возникает, заключается в том, что если есть такое формальное число и встречается в его символике, у нас нет логического метода решения вопроса об истинности или ложности в любом типе. Но мы заменяем на , которое является наибольшим существующим кардиналом того же типа, что и в этом вхождении. Таким образом:

(iii) Если есть формальное число, которое не является функциональным, адекватный актуальный тип для есть тот, для которого мы можем логически доказать , где производно от путем замены любого вхождения в на . Соответственно, если не встречается в , адекватный тип — это любой актуальный тип, для которого мы можем логически доказать .

В случае членов первичной и аргументальной групп мы подставили соответствующего типа вместо каждой переменной. Когда актуальный тип адекватен, мы имеем

В случае членов арифметической группы (за исключением случая , мы подставили вместо каждого аргумента наибольшее кардинальное число, которое может быть получено в типе этого аргумента, а именно для соответствующего типа. Соответственно, мы уверены (за исключением случая , что для всех других значений аргументов, которые являются существующими кардинальными числами, формальное число не является нулевым.

Будет замечено, что нормальная настройка касается только подчиненных типов. Например, *110·03 обеспечивает, что в актуальный тип является адекватным, и *110·23 показывает, что любой адекватный актуальный тип подойдет. Но ничего не говорится об актуальном типе . Мы делаем следующее определение: Когда подчиненные типы формального числа нормально настроены, а актуальный тип адекватен, типы формального числа называются арифметически настроенными.

Мы замечаем, что для первичного набора арифметическая настройка типов означает то же самое, что и адекватная настройка актуального типа. Также, если аргументы формального числа арифметического набора являются простыми символами, обе идеи сводятся к одному и тому же.

В случае переменных формальных чисел первичного набора из *117·22 ·32 следует, что когда их типы арифметически настроены, они не равны для любых значений их переменных.

Также в случае тех переменных формальных чисел, которые относятся к чистому арифметическому набору (исключая ), из *100·4 ·52 ·42. *113·23. *116·23 следует, что, работая от конечных компонентов, достигнутых последовательным анализом вверх, для всех значений таких конечных компонентов, которые являются членами , они могут быть сведены к случаю формальных чисел первичной группы; и что, следовательно, они не равны , когда их типы арифметически настроены. Например, в , , , , являются этими конечными компонентами; пусть они будут существующими кардинальными числами. Следовательно, когда типы арифметически настроены, актуальный тип является адекватным и есть существующий кардинал; мы можем поэтому подставить вместо него. По тому же рассуждению мы можем подставить вместо , и снова вместо .

Определенная стандартная арифметическая настройка типов для любого формального числа всегда может быть найдена путем приведения каждого использования , будь то явного или скрытого в или в каком-то другом символе, к гомогенности. Доказательства, которые применимы к любой арифметической настройке типов, начинаются с рассмотрения этого стандартного типа, а затем с использованием *104·21. *106·21 ·211 ·212 ·213 расширение делается до соседних более высоких классических и реляционных типов. Мы затем "видим", что по аналогии символики это расширение всегда может быть формально доказано на каждом этапе, так что мы имеем дело со стабильным истинностным значением. Для некоторых константных формальных чисел может быть найден более низкий экзистенциальный тип, чем тот, который указан этим методом.

III. Классификация вхождений формальных чисел.

Символическая форма любого из видов [ср. *117·01 ·04 ·05 ·06] называется арифметическим неравенством.

Эти формы возникают только тогда, когда мы сравниваем кардинальные числа в отношении отношения "больше, чем" или "меньше, чем". Может показаться естественным включить уравнения в эти арифметические неравенства. Их использование, однако, даже между кардинальными числами, не является столь исключительно арифметическим, и удобно рассматривать их отдельно под другим заголовком во время наших предварительных исследований.

В арифметических неравенствах, как написано выше, и , или любые символы, заменяющие и , называются противоположными сторонами неравенства, и любая из или называется стороной неравенства.

Символические формы видов и , где либо или есть формальное число, будут называться уравнениями и неравенствами соответственно; и и называются противоположными сторонами уравнения или неравенства, и любая из них просто называется стороной уравнения или неравенства.

Когда мы достигаем исключительно арифметической точки зрения, будет удобно объединить уравнения, неравенства и арифметические неравенства в один вид символической формы. Их разделение здесь сделано ради исследований исключений, обусловленных невыполнением теорем существования в низких типах. Нет необходимости рассматривать арифметические неравенства в этой связи.

Способы, которыми символ может встретиться в символической форме, называются следующим образом:

Вхождение в называется аргументальным вхождением,

Вхождение в качестве аргумента арифметического формального числа (которое может быть компонентом другого формального числа) или в качестве одной стороны арифметического неравенства называется арифметическим вхождением,

Вхождение в качестве одной стороны уравнения называется уравнительным вхождением,

Вхождение в " " называется атрибутивным вхождением,

Любое другое вхождение называется логическим вхождением, так же как и .

Очевидно, что пара противоположных сторон уравнения или неравенства должна быть одного типа. Более того, если есть формальное число, и *20·18 применяется так, чтобы дать , уравнительное вхождение должно быть того же типа, что и его вхождение в ), иначе вывод ошибочен. Соответственно, подстановка в арифметические формулы может быть предпринята только тогда, когда конвенции относительно отношений двусмысленных типов обеспечивают это тождество. Этот вопрос рассматривается позже в этом предисловии, и результат появляется в тексте как *118·01.

В этом месте будут полезны некоторые примеры; на них также будут ссылаться впоследствии в связи с конвенциями, ограничивающими двусмысленности типа.

*100·35.

Здесь формальными числами являются и , каждое из которых имеет три вхождения. Первое вхождение является логическим, второе — уравнительным, а третье — атрибутивным.

*100·42 (в доказательстве).

Здесь и являются единственными формальными числами, и все их вхождения являются уравнительными.

*100·44 (в доказательстве).

Здесь и являются единственными формальными числами; первое вхождение является логическим, второе — уравнительным; оба вхождения являются уравнительными.

*100·511.

Здесь формальными числами являются и . Первое вхождение является логическим, второе — аргументальным, третье — уравнительным; единственное вхождение является уравнительным.

*100·521.

Здесь и являются единственными формальными числами; имеет два вхождения, первое — логическое, второе — аргументальное; имеет одно вхождение, которое является уравнительным.

*101·28 (в доказательстве).

Здесь формальными числами являются 1 и . Первое вхождение 1 является аргументальным, второе — атрибутивным; вхождение является атрибутивным.

*101·38.

Здесь формальными числами являются 0, 1 и 2, и все их вхождения являются логическими.

*110·54.

Здесь формальными числами являются . Вхождение ) и вхождение ( оба являются уравнительными, и они должны быть одного типа, поскольку они являются противоположными сторонами одного и того же уравнения. Вхождения других формальных чисел являются арифметическими компонентами более сложного арифметического формального числа и поэтому являются арифметическими.

*116·63.

Формальными числами являются , , , и ( . Каждое формальное число встречается только один раз. Вхождения и являются арифметическими, а вхождения двух других являются уравнительными.

*117·108.

Формальными числами являются и , каждое с тремя вхождениями. Первые два вхождения каждого формального числа являются арифметическими, последнее вхождение каждого является уравнительным.

*120·53 (в доказательстве).

Здесь формальными числами являются , , , , . Каждое формальное число имеет одно вхождение. Вхождения , и являются уравнительными, а вхождения и являются арифметическими.

*120·53 (в доказательстве).

Здесь формальными числами являются , , , , . Первое вхождение является уравнительным, второе вхождение — логическим; первые два вхождения являются уравнительными, третье вхождение является арифметическим; единственное вхождение является арифметическим; единственные вхождения и являются уравнительными.

IV. Конвенции и .

Два вхождения формального числа с одним и тем же актуальным типом называются связанными друг с другом.

Выбор типов для формальных чисел, когда они не сделаны определенными через переменные с помощью нотации *65, ограничен следующими конвенциями, которые позволяют нам в значительной степени обойтись без сложности, создаваемой определением типов.

. Все логические вхождения одного и того же формального числа находятся в одном и том же типе; аргументальные вхождения связаны с логическими и атрибутивными вхождениями; и, если нет аргументальных вхождений, уравнительные вхождения связаны с логическими вхождениями.

Это правило применяется только, насколько позволяет смысл, к тем типам, которые остаются двусмысленными после назначения типов реальным переменным.

Будет замечено, что если нет аргументальных или логических вхождений формального числа, то никак не применяется к назначению типов вхождениям в форме этого формального числа.

Идентификация типов в аргументальных и атрибутивных вхождениях с помощью необходима для обеспечения использования эквивалентности , где есть формальное число. Без этой конвенции это применение *37·1 было бы ошибочным. Единственный из наших примеров, к которому применяется эта часть конвенции, — это *101·28 (доказательство), где она обеспечивает, что два вхождения 1 находятся в одном и том же типе. Однако это актуально для символики в доказательстве *100·521.

На практике обнаружится, что данная конвенция соотносит типы вхождений таким же образом, как это естественным образом сделал бы любой, кто вовсе не задумывался бы о конвенции. Чтобы увидеть, как работает эта конвенция, мы разберем примеры, которые уже были приведены выше.

В *100·35 *100·35 указывает, что логические и эквациональные вхождения *100·35 должны быть одного типа, и аналогично для *100·35. Кроме того, «смысл» обеспечивает, чтобы эквациональные типы *100·35 и *100·35 были одинаковыми. Таким образом, эти четыре вхождения находятся в одном типе, который не имеет необходимой связи с типами атрибутивных вхождений *100·35 и *100·35. Следовательно, используя обозначение из *65·04 для обеспечения типической определенности, *100·35 должно означать

Типы этих атрибутивных вхождений определяются необходимостью «смысла».

В *100·42 (доказательство), поскольку все вхождения формальных чисел являются эквациональными, *100·42 не создает ограничения типов.

В *100·44 (доказательство) *100·44 обеспечивает, чтобы два вхождения *100·44 были одного типа. Мы также замечаем, что первое вхождение *100·44 на самом деле является (ср. *65·04) *100·44, поскольку встречается «*100·44», и, таким образом, «смысл» требует этого отношения типов, а второе вхождение *100·44 находится в типе вхождений *100·44.

В *100·511 *100·511 указывает, что логические и аргументальные вхождения должны иметь один и тот же тип. В *100·521 *100·521 указывает, что два вхождения *100·521 должны иметь один и тот же тип. В *101·28 оба вхождения 1 должны быть одного типа. В *101·38 *101·38 указывает, что все вхождения 2 должны иметь один и тот же тип.

Данная конвенция никоим образом не ограничивает типы в *110·54, ни в *116·63, ни в *117·108.

В первом примере из *120·53 (в доказательстве) конвенция *120·53 не имеет применения.

Во втором примере из *120·53 (в доказательстве) конвенция *120·53 указывает, что два вхождения *120·53 должны быть одного типа; а необходимость «смысла» обеспечивает, чтобы первое вхождение *120·53 также находилось в этом типе. Та же необходимость обеспечивает, чтобы *120·53 находилось в том же типе, что и *120·53; она также обеспечивает, чтобы в «*120·53» первое вхождение *120·53 и вхождение *120·53 имели общий тип, который в остальном ничем не ограничен; кроме того, ничего не было решено относительно типов *120·53 и *120·53 в *120·53.

Теперь мы переходим к конвенциям, воплощающим результат арифметических идей. Термин «арифметический» здесь используется для обозначения исследований, в которых интерес заключается в сравнении формальных чисел в отношении равенства или неравенства, исключая исключительные случаи — когда бы эти случаи ни были исключительными, — обусловленные отсутствием существования в низких типах. Последовательная арифметическая точка зрения, которую мы принимаем позже в исследовании отношений и количеств, а также в этом томе в *117 и *126 и некоторых более ранних предложениях, отбросила бы как неинтересное любое исследование точных способов, которыми отсутствие теорем существования относится к истинности предложений, тем самым концентрируя внимание исключительно на устойчивых истинностных значениях. Однако логическое исследование имеет свой собственный внутренний интерес среди принципов предмета. Очевидно, однако, что оно должно быть ограничено рассмотрением теорем, представляющих чисто логический интерес. На практике это исключение неинтересных случаев отсутствия арифметических теорем, даже среди логических исследований первой части этого тома, достигается путем обеспечения того, чтобы все арифметические вхождения формальных чисел имели свои актуальные типы адекватными.

Что касается формальных чисел первичной группы, т.е. *158, *158, *158, арифметическая корректировка типов формально обеспечивается в символике определениями *110·03·04 для сложения, *113·04·05 для умножения, *116·03·04 для возведения в степень, *117·02·03 для арифметических неравенств и *119·02·03 для вычитания.

Мы избавляемся от символической разработки, которая возникла бы из расширения аналогичных определений на другие формальные числа, с помощью следующей конвенции:

*160. Всякий раз, когда встречается формальное число *160, так что если бы оно было заменено на *160, актуальный тип *160 по определению должен был бы быть адекватным, тогда актуальный тип *160 также должен быть адекватным.

Например, в *161, если *161 заменить на *161, то согласно *110·04 актуальный тип *161 является адекватным. Следовательно, согласно *161, актуальный тип *161 должен быть адекватным: соответственно, пока *161 и *161 являются простыми переменными и членами *161, мы всегда можем предположить *161 для типа вхождения *161.

Важно заметить, что пока аргумент аргументального формального числа или аргументы арифметического формального числа скорректированы арифметически, точные выбранные типы не имеют значения. Это следует для аргументальных формальных чисел из *102·862·87·88, для сложения из *110·25, для умножения из *113·26, для возведения в степень из *116·26, для вычитания из *119·61·62. Таким образом (помня также о *100·511), в любом определенном типе формальное число имеет одно определенное значение при условии, что любое подчиненное формальное число, которое встречается в его символике, определено экзистенциально. Конвенция *162 предписывает нам всегда брать это определенное значение для любого чисто арифметического формального числа.

Конвенция *163 не определяет полностью значение арифметического формального числа, которое не является чистым. Например, *163 является чисто арифметическим формальным числом, когда *163, *163, *163 определены по типу; и конвенция *163 предписывает, чтобы тип *163 был адекватным. Но *163 является арифметическим формальным числом, которое не является чистым, и конвенция *163 предписывает, чтобы тип области *163 был адекватным, но не влияет на тип *163. Таким образом, легко видеть, что *163 обеспечивает адекватность актуальных типов всех арифметических компонентов любых арифметических формальных чисел, которые встречаются, но не влияет на актуальный тип формального числа, которое встречается как аргумент аргументального формального числа. Но в этом случае конвенция *163 свяжет актуальный тип этого вхождения аргумента с любым логическим или атрибутивным вхождением того же формального числа. Например, если *163 и *163 встречаются в одной и той же форме, то эти два вхождения *163 должны иметь один и тот же актуальный тип. На практике аргументальные формальные числа полезны как компоненты арифметических формальных чисел именно для того, чтобы избежать автоматической корректировки типов, предписываемой *163.

Значение *164 лучше всего объясняется на примерах. Среди наших предыдущих примеров нам нужно рассмотреть только те, в которых встречаются арифметические формальные числа.

В *110·54 конвенция или определения предписывают нам определять типы *165 и *165 адекватно при формировании *165, а также определять *165 и *165 адекватно при формировании *165. Конвенция не применяется к типам *165 и *165. Эти типы должны быть идентичными, чтобы обеспечить смысл.

В *116·63 конвенция предписывает нам адекватно скорректировать типы *166 и *166; она не влияет на типы *166 и *166, которые должны быть идентичными для обеспечения смысла. Если мы заменим *166, *166, *166 на формальные числа, например, на 2, *166 и 1, мы получим «*166». Конвенция теперь предписывает, что 1 должно быть определено адекватно. Так случается, что любой тип является для него адекватным, поскольку *166 может быть доказано в любом типе. Тогда адекватными типами для *166 и *166 являются типы, для которых мы можем доказать *166 и *166. Таким образом, если *166 — это тип *166 в обоих случаях, адекватный тип для *166 — это *166, а для *166 — это *166.

В *117·108 мы находим арифметические вхождения в арифметических неравенствах. Таким образом, *167 предписывает нам брать первые два вхождения *167 и первые два вхождения *167 с адекватными актуальными типами. Тип *167 и *167 в *167 не затрагивается этим. Очевидно, что конвенции *167, *167 недостаточно для обеспечения истинности этого предложения в такой символической записи. Существенно, чтобы в уравнении тип был адекватно скорректирован для обоих формальных чисел. Фактически здесь используется общая арифметическая конвенция, согласно которой типы как эквациональных, так и арифметических вхождений корректируются арифметически.

V. Некоторые важные принципы.

Принцип арифметической подстановки. В *120·53 применение *169 требует рассмотрения всего вопроса об арифметической подстановке. Рассмотрим первый из двух примеров. Мы имеем

Очевидно, что если мы не можем перейти с практической непосредственностью от «*170» к «*170» согласно *20·18, то арифметика становится практически невозможной из-за теории типов. Но трудность возникает из применения *170. Предположим, мы сначала назначаем типы наших реальных переменных. Тогда типы *170, *170, *170, *170 могут быть назначены произвольно, и между ними нет необходимой связи, возникающей из сохранения смысла. Таким образом, *170 может находиться в типе, который не является адекватным типом для *170. Предположим, что это так. Но эквациональное использование *170 находится в том же типе, что и *170, а согласно арифметическому использованию *170 в *170 находится в адекватном типе. Таким образом, на первый взгляд, рассуждение, апеллирующее к *20·18, с помощью которого была оправдана подстановка, является ошибочным; ибо два вхождения *170 на самом деле означают разные вещи.

Чтобы обобщить наше решение этой трудности, удобно определить термин «арифметическое уравнение». Арифметическое уравнение — это уравнение между чисто арифметическими формальными числами, чьи актуальные типы определены адекватно. Тогда очевидно, что из «*171», где *171 и *171 являются формальными числами, а *171 встречается арифметически в *171, мы не можем вывести *171, если только уравнение *171 не является арифметическим. Ибо в противном случае *171 в уравнении не может быть отождествлено с *171 в *171.

Когда мы имеем «*172», где *172 — формальное число, а *172 — число в определенном типе, и хотим перейти к «*172» или «*172» и хотим перейти к «*172», причем вхождение *172 в *172 является арифметическим, тип *172 может не быть адекватным типом для *172. Соответственно, *172 в «*172» не может быть отождествлено с *172 в *172. Тип *172 в уравнении должен быть освобожден от зависимости от типа *172. Соответственно, переход является законным только тогда, когда мы можем написать вместо этого, где в обоих случаях уравнение является арифметическим. Ибо теперь все символы подчиняются одним и тем же правилам.

Если эта модификация может быть сделана без изменения истинностного значения утверждаемых предложений, подстановка является законной, в противном случае — нет.

Очевидно, что в вышеприведенном наш непосредственный переход осуществляется к или от *174. Но легко видеть, что, поскольку вхождение *174 является арифметическим, мы всегда имеем *174. Чтобы доказать это, нам нужно лишь доказать