Избранное
ЭБ Нефть
и Газ
Главная
Оглавление
Поиск +
Еще книги ...
Энциклопедия
Помощь
Для просмотра
необходимо:


Книга: Главная » Гильберт Д.N. Математическая логика и основания математики
 
djvu / html
 

200 ИСЧИСЛЕНИЕ ПРЕДИКАТОВ [ГЛ. IV
окажется, что формула
может быть соответствующими подстановками получена из некоторой выводимой формулы исчисления предикатов. Но указанная формула средствами исчисления высказываний может быть преобразована в отрицание формулы
Hi& ... &Щ.
Таким образом, если аксиомы §Ii, . . ., Щ приводят к противоречию, то каждая формула, которая получается из формулы $i & . . . & Щ в результате замены предикатных символов формульными переменными с тем же самым числом аргументов, а индивидных символов — свободными индивидными переменными, должна бьгть опровержимой в исчислении предикатов. Отсюда и вытекает справедливость той теоремы, которую мы приводили при разъяснении взаимосвязи между непротиворечивостью систем аксиом и неопровержимостью логических формул 1).
Вернемся теперь к нашей дедукционной теореме и извлечем из нее еще одно следствие. Пусть снова формула 533 выводима из некоторой формулы §1- Однако относительно этого вывода мы сейчас не будем предполагать, что все свободные переменные формулы 21 остаются незатронутыми. Будем лишь предполагать, что в 51 остаются незатронутыми формульные переменные. Тогда можно будет утверждать, что если формула 2Г получается из формулы ЭД в результате связывания свободных индивидных переменных в ЭД кванторами всеобщности, написанными в начале этой формулы, то формула ЭД' — >• 58 будет выводимой (без использования формулы ЭД).
Действительно, согласно правилу (е') 2), формула ЭД выводима из И' и в этом выводе формульные переменные, входящие в ЭД', остаются незатронутыми. Но, по предположению, формула 58 выводима из ЭД при незатронутых формульных переменных. Тем самым мы получаем некоторый вывод 93 из формулы ЭД', при котором формульные переменные в ЭД' остаются незатронутыми. §1' не содержит никаких свободных переменных, кроме формульных. Следовательно, дедукционная теорема применима, и отсюда получается, что формула
является выводимой.
В частности, этот результат мы можем применять для того, чтобы избавляться от необходимости выводить те или иные форму-
J) См. с. 170. ») См. с. 175.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200 201 202 203 204 205 206 207 208 209 210 220 230 240 250 260 270 280 290 300 310 320 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550


Математика