Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 109
Текст из файла (страница 109)
35 ° ДОБЛВЛКИИЕ 548 3. Формулы вида а = Ь вЂ” ». (1(а) = 1(Ь)), а =6 -+ (З (с, а) — »- З (с, Ь)) к формуле а = Ь -ь (Я (а) -»- Я (Ь)) а =- 6 -+ (Я (а) «- Я (Ь)) а = Ь -+. 1„З (х, а) = «„й (х, Ь). а =- Ь -+. «„й (х, а) = 1«й (х, Ь), а = Ь -ь (»э (а) -»- б (6)), 11 См. с.
485. а = Ь вЂ” ~1 З (х, а) =1„З (х, 6) ПОНЯТИЕ «ТОТ, КОТОРЫЙ» И ЕГО УСТРЛИИМОСТЬ 1ГЛ. УП1 где З(а) и ~ (а) обозначают предикатный символ и функциональный знак с аргументом а и, быть может, какими-нибудь другими аргументами. Это рассуждение теперь нуждается в дополнении с учетом гюявления 1-символов. Прежде всего следует обратить внимание на осложнения, вызванные условиями, ограничивающими 1-правило (мы берем его здесь в первоначальном виде).
Для какой-либо формулы З(а, с) и терма 1 может оказаться, что выражение 1„З(х, 1) является термам, в то время как «„й(х„с) термам не является. В этом можно убедиться на простых примерах. Поэтому выражение Я (1) иногда может быть формулой без того, чтобы формулой было Я (с). С учетом этого обстоятельства мы докажем наше утверждение в несколько уточненной формулировке: Если а и 6 — термы, а Я (а) и Я (Ь) — формулы, то формула может быть выведена из аксиом (1) при помои~и средств исчисления предикотов и «-правила.
Это утверждение может быть доказано следующим образом. Прослеживая построение формул, — аналогично тому, как это делалось в уже упоминавшемся рассуждении иа гл. 1Г11,— мы сначала убеждаемся в том, что формула может быть выведена средствами исчисления предикатов из фор- мул (1) и формул вида где 1„З (х, а) и 1«й (х, Ь) суть термы, которые входят в Я (а) или соответственно в Я (Ь) в качестве внеп1яих 1-термов (в отличие от вложенных в другие 1-термы).
Наше предположение о том, что Я (а) и Я (Ь) являются формулами„включает в себя допущение, что входящие в Я (а) и в Я (Ь) 1-термы (в частности, стало быть, и термы 1, З (х, а), 1 й (х, 6)1 вводятся по 1-правилу при помощи соответствующих формул единственности. Разумеется, здесь вместо х ыожет фигурировать и какая-нибудь другая свизанная переменная. Теперь каждую из формул можно будет вывести без использования аксиом равенства из некоторой формулы вида а = Ь-ь (б (а)-+ Ж (Ь)), в которой Ж (а) и 14 (6) содержат меныпе 1-символов, чем Я (а) и Я (6). Действительно, если мы возьмем какую-нибудь не входящую ни в З (х, а ), ни в З (х, 6) свободную индивидную переменную (например, с), то формула будет иметь укааанный вид; при этом й (с, а) будет содержать меньше 1-символов, чем Я (а), а Я (с, 6) — меньше, чем Я (Ь), потому что 1„З(х, а) является составной частью Я (а), а1 З(х, 6)— составной частью Я (Ь).
Далее, при помощи средств исчисления предикатов мы можем перейти от формулы а = Ь -».(й (с, а) -«. З (с, 6)) а = Ь -+ 'ух (й (х, а) »- З (х, Ь)). С другой стороны, применив формулы З(1,З(х, а), а) и й (1„З(х, Ь), Ь) и вторую связанную с »„й (х, 6) формулу единственности, мы, как было показано ранее '), получим средствами исчисления предикатов формулу 'ох (З (х, а) -ь З (х, 6) ) -»-1,З (х, а) = 1,З (х, Ь), а эта последняя, вместе с предыдущей формулой, по правилу сил- логизма даст нам формулу Таким образом, в итоге получается, что при помощи средств исчисления предикатов, 1-правила и формул (1) формула а=-Ь-~(Я (а) — ~- Я (Ь)) может быть выведена из формул вида у которых число входящих в них 1-символов меньше, чем у формулы а = Ь -«-(Я (а) -»- Я (6)).
550 ПОНЯТИЕ «ТОТ, КОТОРЫЙ» И ЕГО УСТРАНИМОСТЬ !ГЛ. У1П АЛФАВИТНЫЙ УКАЗАТЕЛЬ Гейтинг (Неу11п8 А.) 102 Гельмгольц (Не!тйо!Сх Н.) 56 Генетический способ построения теории 24 Генцен (Бепххеп 6.) 14 Гедель (Боойе! К.) 14, 19 — 20, 168, 187 †1, 203, 502, 510 Гильберт (Н1)Ьегс Б.) 11, 13 — 16, 19 — 20, 23 — 24, 28 — 29, 39, 96 Гипотетическое истолкование всеобщности 59 Беман (Ве)ппапп Н.) 189, 250 Бернайс (Вегпауе Р.) 11, !5 — !6, 19, 187 Брауэр (Вгопвег !., Е. !.) 12 — 13, 24, 61, 71 Буль (Воо)е Б.) 11 Двоичная дробь 66 Двойственность 83.
151, 168 Дедекинд (Бе8е)с!пй В.) 11, 265, 500, 502 Вайсберг ()Уа)зйеги 5!.) 101. 160. 163 Веблеи («'еЫеп О.) 26, 36 Повторное применение этой процедуры в конце концов сводит вывод формулы а* Ь-ь(Я (а)-+. л(Ь)) к выводам таких формул а Ь -«. (Й (а) -ь з! (Ь)), которые вообще не содержат ни одного 1-символа. А эти формулы, как мы внаем, могут быть получены иэ формул (!) При помощи средств исчисления предикатов. Тем самым для вывода формулы а=Ь-ь(Й (а)-+ Я (Ь)) окаэывается достаточно средств исчисления преднкатов, х-пра- вила и формул (!), что и требовалось доказать.
Аккерман (Ас)гегщапп Ж.) 19, 20, 187 — 188, 406 — 408, 509 Аксиома индукции 325, 5Ы вЂ” о параллельных 29 Аксиоматнка Евклида 45 Аксиоиатпческая теория 122 Аксиоматический способ построення теории 24 Аксиомы как формулы 125 — Пеано 272, 351 — — (Рх) и (Ре) 273 — порядка 28 — равенства (Х,) и (!з) 210 — собственные 511 — соединения 28 Алгебра логики 83 —, содержательный подход к ней 56 †, формальная точка зрения в ней 56 Анализ, аксиоматический 43 —, выход за рамии фнпптной установки з нем 62 Аргумент формулы 138 Арифмегпзацпн понятая величины 70 Арифметика 45, 351 —, открытые проблемы 63 †, рекурсивная 376 —, формализация ее в (7) 486 Вейерштрасс ()те!егз1газе К.) 11 Вейль (Гтеу! Н.) 67 Верифицируемая формула 294, 301, 305, 307, 336, 339, 343, 360, 363, 441, 449 Верхняя грань 67 Весла («ее!еу В.) 15 Взаимно простые числа 491 Вложение 1-термов 472 Воавратный перенос подстаиовок 278 — — — при включении схемы индукции 328 — — — — наличии связанных переменных 286 Вывод средствами исчисления предикатов 141 — формальный 94 Выделенная переменная рекурсии 353 Выполнимость 31, 164, 167, 171 — в конечном 233 Выражение 77, 123 АЛФАВПТНЫЙ УНАЭАТИЛЬ АЛФАВПТНЫЙ УКАЗАТНЛЬ 553 Евклид 23, 45, 51 Дедекиндово определение бесконечности 265 — сечение 64 Дедуктивное равенство 192 Дедуицвониая теорема 194 Деление в рекурсивной арифметике 391 — цифр 51 Диагональная процедура 405 Диаъюнкция 27, 75 †, нульчлеиная 144 †, распространенная на всю анди- видную область 34 — и-члсияая 34 Диофантово уравнение 455 Доказательство как вывод 274 — невозможности 54 — независимости 37, 103 Дополнение мноисества 166 Закон исключаниого третьего 62, 71 — тождества 212 Законы ассоциативности, коммутативности и дистрибутнвности в исчислении высказываний 79 Замена свободных переменных связанными 250 Заменимость дизъюнкции пьшликацией 81 — связок исчисления высказываний 79 — 82 Зенон 40 Зифкес (8!е!)сез Р.) 18 Знак отрицания 27, 75 Знаки для сообщения 46 Идентификация переменных 209 Изображение рациональных чисел целыми 64 «Или» разделительное 82 Именная переменная 522 — форма 123 Иьшликативиая формула 99 .— —, регулярная 99 Импликация 27, 76 Индивпдная область 24, 32 — —, бесконечная 38, 42 — —, пустая 32, 43 Индивидные переменные 31„ 12! — †, свободные и связанные 130 Индивндный символ 123 Индукция 49, 371 —, полная 49, 325 Иатеисиональная логика 83 Интерпретация 103 Интуициониэм 71 — как расширение фшштной установки 7! Исключение свободных переменных 279 — формульных переменных 251— 255 — функциональных знаков 56 — экаистенцпальных высказываний 270 Истинностное значение 75 — †, выделенное 106 Истиниостные функции 74 — —, зыразимость пх через Л, тсси )77 — —, зависимость между ними 77 Исходная формула 94, 142 Исчисление бесконечно малых 64 — второй ступени 501 — высказываний 83, 96, !!5 — предикатов 141, 144 †1 — †, одноместное !62, 188 — —, —, расширенное 226 — —, расширенное 276, 5!1 Кальмар (Ка)тпаг ! .) !87 — 188 Кантор (Сап!от 6.) 11, 39 Кариап (Сагпар К.) 511 Кваитор всеобщности 26, 135 — существования 26, 135 Класс с разрешимоп проблемои выводимасти 186 — — — — выполнимости !86 Клаузиус (С!аизгиз К .) 23 Клейн (К)е!и Р.) !3 Клинп (К!еепе 8.
С.) 15, 532 Количественные формулы 225 Количество суждения 135 Коллизия между связанныьти переиенными 133, 470 Компоненты формулы 161 Конструктивный способ построения теории 24 Континуум 41 Контрапозицпя 117 Конъюнкции 27, 75 —, нульчленная 144 —, распрсютранеипая на всю индквидиую область 135 — и-члеииаа 34 Крайзел (Кге1зе! О.) 18, 375 Кронекер (Кгоиесйег ! .) 7! Куайн (Ои!ие %. У.) 143, 515 Лейбниц (Ье!)тшсх О.
Ъу.) 11 Лесьневсктш (Ьези!еиэйй 8.) 96 Левенгейм (1,6меийе!ш 1,.) 168, 250 Лобачевский Н. И. 13 Логика предпкатов 121 — †, теоретико-множественная 165 — †, чистая 31 Логическая сумма 83 2!огические знаки 26 Логическое произведение 83 Лукасевич (!.и)саэ!есттсг 7.) 46, 10!в 103 Льтоис (! етЛэ С. !.) 99 Максимум двух и трех чисел 387— 388 — конечной последовательности чисел 499 Матиясевич Ю.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
