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


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

320 МЕТОД АРИФМЕТИЗАЦИИ МЕТАМАТЕМАТИКИ [ГЛ. IV
Полученному результату можно также придать и другую формулировку, приняв во внимание связь, имеющую место между формулами логики предикатов и системами аксиом. Непротиворечивость какой-либо системы аксиом, представленной с помощью конечного числа формул без функциональных знаков, равносильна неопровержимости формулы g логики предикатов, которая получается из этой системы, если входящие в ее состав формализо-' ванные аксиомы связать знаком конъюнкции, а затем заменить все входящие в них символы основных предикатов формульными переменными с соответствующим числом мест для аргументов, а все индивидные символы — индивидными переменными, связываемыми проставленными в начале формул кванторами существования. Переход от формулы % с помощью соответствующих арифметических подстановок к формуле g* по смыслу представляет собой построение арифметической модели рассматриваемой системы аксиом, так как формулы, изображающие эти аксиомы, при замене символов для основных предикатов арифметическими выражениями, подставляемыми вместо соответствующих формульных переменных, переходят в доказуемые арифметические формулы (доказуемые, конечно, только при добавлении некоторой верифицируемой исходной формулы q(&) = 0, которая выражает непротиворечивость этой системы аксиом в математической формализации и которая сама по себе не обязана быть выводимой в формализме арифметики).
Таким образом, существование арифметической модели для непротиворечивой системы аксиом рассматриваемого нами типа имеет место в некотором дедуктивном смысле.
Разумеется, доказанная теорема имеет смысл теоремы о полноте, т. е. выражает некоторую дедуктивную завершенность исчисления предикатов, только в предположении непротиворечивости этого арифметического формализма, ибо если этот формализм противоречив, то никакого арифметически непротиворечивого формализма не будет вообще.
Это соображение указывает нам на то, что задача установления непротиворечивости всего арифметического формализма в целом в наших исследованиях пока что остается нерешенной проблемой. На самом деле, все рассмотренные нами до сих пор методы установления непротиворечивости оказываются неприменимыми для решения этой задачи. Это обстоятельство, которое может нас озадачить, находит принципиальное объяснение в одной теореме Гёделя о дедуктивных формализмах, первым объектом применения которой является формализм арифметики. Выводы, которые влечет за собой эта теорема, вынуждают нас расширить область допустимых неформальных рассуждений, употребляемых в теории доказательств, по сравнению с тем, что до сих пор допускалось при фактической реализации нашей финитной точки зрения.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200 210 220 230 240 250 260 270 280 290 300 310 320 321 322 323 324 325 326 327 328 329 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика