Доказательство первого из этих предложений выглядит следующим образом:
В вышеприведенном доказательстве шаг к (3) является законным, поскольку согласно гипотезе *176 является определением *176 в адекватном типе.
Аналогичные доказательства справедливы для других предложений с использованием *113·204, *116·204, *117·12 и *103·13.
Мы должны также рассмотреть обстоятельства, при которых мы можем перейти от «*178» к «*178», где последнее уравнение является арифметическим. Другими словами, используя *65·01, нам требуется гипотеза, необходимая для
Мы имеем
Теперь в (4) вхождения *180 и *180, которые находятся в одном типе, могут быть выбраны так, чтобы находиться в любом типе, который нам нравится. Следовательно, мы выводим
Следовательно, *181 является необходимым условием. Теперь, поскольку *181 может находиться в любом типе, мы также можем выбрать его в любом экзистенциальном типе для *181. Таким образом, с *181, применяемым к арифметическому вхождению *181 в *181, мы имеем, где *181 — формальное число, а *181 — число в определенном типе,
В последнем предложении согласно *182 уравнение *182 является арифметическим. Эти уравнения суммируются в *118·01.
Эти три фундаментальные теоремы воплощают принцип арифметической подстановки. Гипотеза *183 на самом деле слабее, чем предполагается в обычной жизни, где обычное молчаливое допущение — это *183. Фактически, если *183, то *183 обязательно ложно.
Принцип отождествления типов. Предположим, мы доказали «*184» и «*184», где *184 — формальное число, чье вхождение в «*184» находится в совершенно двусмысленном типе, а *184 — то же самое формальное число, чей тип соотносится с типом *184 согласно *65·01. Тогда, поскольку тип *184 в «*184» является двусмысленным, мы можем написать «*184» и отсюда вывести «*184».
Принцип заключается в следующем: совершенно неопределенный тип в утверждаемой символической форме может быть отождествлен с любым типом, двусмысленным или иным, в любой другой утверждаемой символической форме или в той же самой символической форме.
Например, в *100·42 (доказательство), рассмотренном выше, поскольку встречается *186, первые вхождения *186 и *186 одного типа, так же как и их вторые вхождения в *186. Но два типа не определены нашими конвенциями как имеющие какую-либо необходимую связь. Фактически тип *186 в *186 совершенно произволен. Соответственно, он может быть отождествлен с другим типом, и таким образом вывод к следующей строке, а именно к «*186», является оправданным.
В случае арифметических уравнений важно заметить, что мы имеем *187. Следовательно, если *187 и *187 являются формальными числами, *187. Таким образом, если мы имеем «*187» и «*187», мы можем вывести из первого предложения «*187», и из этого и последнего предложения мы выводим «*187», так что общий принцип отождествления может быть использован, когда *187 в первом предложении является арифметическим уравнением.
Например, в примере, приведенном выше, *100·44 (доказательство), а именно уравнение *188 является арифметическим. Соответственно, мы оправданы в утверждении пропозициональной функции, где *188 в «*188» все время предполагалось необходимостью смысла. Таким образом, следует вывод,
Это доказательство теряет смысл, когда *189 рассматривается как переменная, обязательно имеющая один и тот же тип повсюду. Ибо тогда предложение сводится к
Но если *190 является формальным числом, обязательно являющимся членом *190, предложение на самом деле является
С этим предположением мы имели бы в первой строке доказательства *191, хотя с «*191» как единой переменной строка формально верна в том виде, в каком она стоит в тексте.
Распознавание частных случаев. Важно заметить условия, при которых *192 может быть распознано как частный случай *192, где *192 — реальная переменная, а *192 — формальное число. Во-первых, очевидно, мы должны подставить *192 вместо *192, где бы оно ни встречалось в *192, и таким образом получить *192. Затем мы можем обнаружить, что путем применения наших конвенций мы можем заменить это на *192. Например, мы имеем
*100·42.
Теперь подставим *194 вместо *194, мы получим
Теперь согласно *195, даже когда *195 является формальным числом, идентичность типов двух вхождений *195 одинаково обеспечена в
Таким образом, это частный случай *100·42. Такие выводы могут быть сделаны в общем виде без какого-либо явного формального утверждения.
Двусмысленность *197. Из типической двусмысленности *197 следует (ср. *100·02 и *103·02), что *197 также является типически двусмысленным. Следовательно, «*197» согласно нашим методам интерпретации не требует, чтобы *197 и *197 были одного типа. Мы всегда будем интерпретировать «*197» как означающее «*197» и, следовательно, как не обязательно отождествляющее типы *197 и *197. Аналогично для *197, *197 и *197. Например
*110·402.
Здесь *199 и *199 не обязательно должны быть одного типа. Опять же
*110·41.
Здесь отождествление типов *201 и *201 требует гипотезы «*201».
VI. Конвенции *202 и *202.
Общая арифметическая конвенция. Конвенции *203 и *203 применяются всегда, но следующая конвенция поначалу не используется. Эта конвенция ограничивает остаточную двусмысленность типа путем устранения исключительных случаев в низких типах, обусловленных отсутствием теорем существования. Конвенция будет цитироваться как *203.
*204. Все уравнения, включающие чисто арифметические формальные числа, должны быть арифметическими.
Мы видели, что из арифметического уравнения можно вывести аналогичное уравнение в любом другом типе. Таким образом, с *205 все уравнения между формальными числами определены по типу так, что их истинность в «любом типе» выводима. Таким образом, в немногих ранних предложениях, где вводится *205, этот факт отмечается утверждением, что уравнения верны «в любом типе». Эти предложения — *103·16, *110·71·72.
Эффект применения *206 к другим предложениям в *100 заключается в том, чтобы сделать некоторые из гипотез (обычно логические формы, утверждающие существование) ненужными, но также существенно ограничить область действия предложений. Возьмем, например,
*100·35.
Если мы применим *208 к этому, мы можем написать
Ибо эквациональные вхождения *209 и *209 должны согласно *209 и *209 иметь адекватные актуальные типы. Но если *209 — малый класс в высоком типе, адекватным актуальным типом для *209 будет высокий тип, тогда как *209 может быть верным в низком типе. Таким образом, с *209, ради простоты, мы отказываемся от формулировки минимума гипотез, необходимых для наших предложений. Формулировка ни одного другого предложения в *100 не затрагивается.
Формулировка ни одного предложения в *101 не затрагивается *210, хотя это чрезмерно ограничило бы область действия *101·34. В *110 *210 чрезмерно ограничило бы область действия таких предложений, как *110·22·23·24·25·251·252·3·31·32·331·34·35·351·44·51·54 и многих других, не изменяя их формулировок. В *110 нет предложения, формулировку которого это изменило бы. *212 уже применяется к *110·71·72; если *212 удалить из этих предложений, то *212 должно быть добавлено как гипотеза к обоим из них. Эффект *212 на *113 и *116 полностью аналогичен эффекту на *110; ни в одном из этих двух номеров нет предложения, к которому *212 применялось бы в тексте.
Что касается *117, *213 применяется повсюду, так что все предложения имеют форму, подходящую для последующих исследований, в которых интерес является чисто арифметическим. Однако важно проанализировать эффект AT на формулировки ради логических исследований, особенно в связи с *120. Во-первых, *213 может затрагивать только предложения, в которых встречаются уравнения или неравенства, и среди таких предложений оно не затрагивает формулировки тех, в которых обе стороны уравнений не являются формальными числами, так что уравнения не являются арифметическими после применения AT. Эти предложения — *117·104·14·24·241·243·31·551. Эти предложения, которые характеризуются наличием одной буквы на одной стороне любого вовлеченного уравнения, могут быть распознаны с первого взгляда. Предложения, включающие арифметические уравнения, чьи формулировки не изменяются удалением *213, — это *117·21·54·592. Предложения, включающие неравенства, чьи формулировки не изменяются удалением *213, — это *117·26·27. Наконец, единственные предложения *117, чьи формулировки изменяются удалением *213, — это *117·108·211·23·25.
В *118 и *119 *214 не используется.
В *120, который посвящен тем свойствам индуктивных кардинальных чисел, которые представляют логический интерес, *215 никогда не используется. Ни одно из предложений *117·108·211·23·25·3 не цитируется в нем, за исключением *117·25 в доказательстве *120·435 для использования, где *215 не является релевантным. Применение AT к *120 упростило бы гипотезы *120·31·41·451·53·55 и ограничило бы области действия предложений.
Требуется еще одна конвенция, которую мы назовем «*216», в определенных предложениях, где гипотеза подразумевает, что существуют типы, в которых существует каждое индуктивное кардинальное число, т.е. в которых *216 не является индуктивным классом. Среди таких гипотез — *216, *216, *216 (или типически определенные формы этих гипотез) или *216 или *216. Когда встречаются такие гипотезы, мы будем предполагать, что *216 индуктивно, всякий раз, когда значимость позволяет, должно быть определено в типе, в котором существует каждое индуктивное кардинальное число, т.е. в котором выполняется аксиома бесконечности (ср. *120·03·04). Формулировка этой конвенции выглядит следующим образом:
*217. Когда гипотеза предложения подразумевает, что существует тип, в котором существует каждое индуктивное кардинальное число, каждое вхождение «*217» в этом предложении должно быть взято (если условия значимости позволяют) в достаточно высоком типе, чтобы обеспечить существование каждого индуктивного кардинального числа.
Следует заметить, что эта конвенция была бы ненужной, если бы мы ограничились одной экстенсиональной иерархией, ибо в любой такой иерархии *218 все типы являются индуктивными или все являются неиндуктивными, так что если каждое индуктивное кардинальное число существует в одном типе в иерархии, то же самое верно для любого другого типа в иерархии. Но когда мы больше не ограничиваемся одной экстенсиональной иерархией, этот результат может не последовать. Например, может оказаться, что число индивидов индуктивно, но число предикативных функций индивидов не является индуктивным; во всяком случае, нельзя привести логической причины против этой возможности, которая может быть отвергнута только на эмпирических основаниях, если вообще может быть отвергнута.
То, как используется эта конвенция, может быть проиллюстрировано доказательством *122·33. Во второй строке этого доказательства мы показываем, что гипотеза подразумевает *219. Будет видно, что эти определения не достаточны для определения типа *219. Следовательно, в (1) *219 слева может не быть того же типа, что и *219 справа. Теперь использование *122·473, которое встречается в следующей строке доказательства *122·33, требует, чтобы *219 слева и *219 справа были одного типа. Это требует, чтобы *219 не было взято в типе, в котором мы имеем *219. Следовательно, чтобы применить *120·473, мы должны выбрать тип, в котором существуют все индуктивные кардинальные числа. Поскольку «*219» встречается в гипотезе, мы знаем, что все индуктивные кардинальные числа существуют в типе *219. Но нет необходимости ограничиваться типом *219, поскольку любой другой тип, в котором существуют все индуктивные кардинальные числа, одинаково обеспечит справедливость доказательства. Таким образом, конвенция *219 обеспечивает требуемое ограничение и не более того.
Конвенция *220 часто релевантна, когда «*220» без какого-либо типического определения встречается в гипотезе. Всякий раз, когда это так, если «*220» встречается в предложении таким образом, что его тип остается неопределенным, насколько это касается условий значимости, оно должно быть взято в типе, в котором существуют все его члены.
VII. Окончательное рабочее правило в арифметике.
Теперь (всякий раз, когда используется *222 вместе с *222, когда это необходимо) возможно окончательно отбросить всякое рассмотрение типов в связи с индуктивными числами. Ибо, объединяя *126·121, *126·122 и *120·4232·4622, мы видим, что всегда возможно взять тип достаточно высоким, чтобы никакое определенно установленное индуктивное число не было нулевым (*222), и чтобы все индуктивные рассуждения могли происходить внутри этого типа. Более того, мы уже видели, что арифметические операции не зависят от типов компонентов, пока они являются экзистенциальными. Таким образом, насколько это касается обычной арифметики конечных чисел, все конвенции (включая AT) и необходимость гипотез относительно существования индуктивных чисел окончательно заменяются следующим единственным правилом:
Правило неопределенных чисел. Тип, назначенный любому символу, который представляет индуктивное число, таков, что символ не равен *223.
Мы делаем определение
*126·01.
Везде, где используется этот символ «*226» для класса «неопределенных индуктивных кардинальных чисел», вышеуказанное правило соблюдается. Другими словами, «*226» всегда может быть заменено на «*226», где *226 является гомогенным или возрастающим кардинальным числом, а *226 является соответствующей константой или переменной, в зависимости от случая. В последнем случае символическая форма, такая как *226, может быть заменена на
Более того, согласно *120·4622 следует, что с этим правилом результат проведения индукции в одном типе, а затем преобразования в другой тип, такой же, как результат проведения индукции в последнем типе. Таким образом, например, нет никакого преимущества в различении *227 и *227; ибо *227, *227, *227, *227, *227, *227 и *227 и так далее.
Следовательно, всякое различение типов неопределенных индуктивных чисел может быть отброшено; и типы являются совершенно неопределенными и нерелевантными.
СНОСКИ:
[1] Но ср. следующую страницу для более точной формулировки этого принципа.
ЧАСТЬ III. КАРДИНАЛЬНАЯ АРИФМЕТИКА.
ОГЛАВЛЕНИЕ ЧАСТИ III.
В этой части мы будем заниматься, во-первых, определением и общими логическими свойствами кардинальных чисел (Раздел A); затем операциями сложения, умножения и возведения в степень, определения и формальные законы которых не требуют никакого ограничения конечными числами (Раздел B); затем теорией конечного и бесконечного, которая становится несколько сложной из-за того факта, что существуют два разных смысла «конечного», которые не могут (насколько известно) быть отождествлены без предположения мультипликативной аксиомы. Теория конечного и бесконечного будет возобновлена в связи с рядами в Части V, Раздел E.
Именно в этой части теория типов впервые становится практически релевантной. Обнаружится, что противоречия относительно максимального кардинального числа решаются этой теорией. Поэтому мы посвятили наш первый раздел в этой части (за исключением двух номеров, дающих самые элементарные свойства кардинальных чисел в общем, а также 0, 1 и 2 соответственно) применению типов к кардинальным числам. Каждое кардинальное число типически двусмысленно, и мы придаем типическую определенность с помощью обозначений *63, *64 и *65. Именно там, где речь идет о теоремах существования, теория типов является существенной. Главная важность предложений настоящей части заключается не только, как и во всей книге, в гипотезах, необходимых для обеспечения выводов, но также в типической двусмысленности, которая может быть допущена для символов в соответствии с истинностью предложений во всех случаях, тем самым включенных.
РАЗДЕЛ A. ОПРЕДЕЛЕНИЕ И ЛОГИЧЕСКИЕ СВОЙСТВА КАРДИНАЛЬНЫХ ЧИСЕЛ.
Оглавление Раздела A.
Кардинальное число класса *237, которое мы будем обозначать «*237», определяется как класс всех классов, подобных *237, т.е. как *237. Это определение принадлежит Фреге и было впервые опубликовано в его «Grundlagen der Arithmetik» [2]; его символическое выражение и использование можно найти в его «Grundgesetze der Arithmetik» [3]. Главные достоинства этого определения: (1) формальные свойства, которые мы ожидаем от кардинальных чисел, следуют из него; (2) если мы не примем это определение или какое-то более сложное и практически эквивалентное определение, необходимо рассматривать кардинальное число класса как неопределяемое. Следовательно, вышеуказанное определение позволяет избежать бесполезного неопределяемого понятия с сопутствующими ему примитивными предложениями.
Будет замечено, что если *238 — любой объект, 1 не является кардинальным числом *238, но является кардинальным числом *238. Это предотвращает путаницу, которая в противном случае может возникнуть при работе с классами. Предположим, у нас есть класс *238, состоящий из многих членов; мы говорим, тем не менее, что это один класс. Таким образом, кажется, что он одновременно один и многие. Но на самом деле именно *238 — это многие, а *238 — это один. Что касается нуля, аналогичный момент еще яснее. Предположим, мы говорим «нет королей Франции». Это эквивалентно «класс королей Франции не имеет членов» или, на нашем языке, «класс королей Франции является членом класса 0». Очевидно, что мы не можем сказать «король Франции является членом класса 0», потому что нет короля Франции. Таким образом, в случае 0 и 1, как более очевидно во всех других случаях, кардинальное число относится к классу, а не к членам класса.
Для целей формального определения мы подвергаем формулу *239 некоторому упрощению. Будет видно, что согласно этой формуле «*239» является отношением, а именно отношением кардинального числа к любому классу, числом которого оно является. Так, например, 1 имеет к *239 отношение *239; так же имеет 2 к *239, при условии *239. Отношение *239 — это, фактически, отношение *239; ибо *239. Следовательно, для формальных целей определения мы полагаем
Класс кардинальных чисел — это класс объектов, которые являются кардинальными числами чего-либо, т.е. объектов, которые для некоторого *240 равны *240. Мы называем класс кардинальных чисел *240; таким образом, мы имеем
Для целей формального определения мы заменяем это более простой формулой
В настоящем разделе мы будем заниматься тем, что можно назвать чисто логическими свойствами кардинальных чисел, а именно теми, которые не зависят от арифметических операций сложения, умножения и возведения в степень, а также от различения конечного и бесконечного [4]. Главный момент, с которым нужно иметь дело, как в отношении важности, так и трудности, — это отношение кардинального числа в одном типе к тому же или ассоциированному кардинальному числу в другом типе. Когда символ двусмысленен в отношении типа, мы будем называть его типически двусмысленным; когда, либо всегда, либо в данном контексте, он однозначен в отношении типа, мы будем называть его типически определенным. Теперь символ «*242» типически двусмыслен; единственное ограничение на его тип состоит в том, что его область и область значений должны состоять из классов. Когда мы имеем *242, *242 и *242 не обязательно должны быть одного типа, фактически, в любом типе классов существуют классы, подобные некоторым классам любого другого типа классов. Например, мы имеем *242, к каким бы типам *242 и *242 ни принадлежали. Эта двусмысленность «*242» проистекает из двусмысленности *242, которая, в свою очередь, проистекает из двусмысленности 1. Мы обозначаем (ср. *65·01) через «*242» все единичные классы, которые того же типа, что и *242. Тогда (согласно определению *70·01) *242 будет классом тех взаимно однозначных отношений, чья область того же типа, что и *242, а область значений того же типа, что и *242. Таким образом, «*242» типически определено, как только заданы *242 и *242. Предположим теперь, вместо того чтобы иметь просто *242, мы имеем *242; тогда мы знаем не только, что *242, но также что *242 принадлежит к тому же типу, что и *242, а *242 принадлежит к тому же типу, что и *242. Когда двусмысленный символ «*242» делается типически определенным путем определения его области как имеющей тот же тип, что и *242, и его области значений как имеющей тот же тип, что и *242, мы пишем его «*242», потому что обычно, в соответствии с *65·1, если *242 — типически двусмысленное отношение, мы пишем *242 для типически определенного отношения, которое получается, когда область *242 должна состоять из членов того же типа, что и *242, а область значений должна состоять из членов того же типа, что и *242. Таким образом, мы имеем *242. Здесь все типически определено, если заданы *242 и *242 (или их типы).