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


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

540 ПОНЯТИЕ «ТОТ, КОТОРЫЙ» И ЕГО УСТРАНИМОСТЬ 1ГЛ. VIII
Теперь устранение i-терма 1ХФ (а, Ь, х) оказывается равносильным устранению ф (а, Ь). Если мы произведем устранение терма 1д.Ф (а, Ь, х), то вместо любой построенной по правилам формализма @ формулы, содержащей функциональный символ Ф (•,•)> мы получим «представляющую» ее формулу формализма (?*, получающегося из© опусканием функционального символа Ф (•,•) и аксиомы й(а, Ь, с, ф (а, Ь), ф (а, с)) и добавлением предикатного символа Ф, а также трех сформулированных для него аксиом. Если формула, построенная по правилам @, выводима средствами этой системы, то представляющая ее формула будет выводима средствами ©*, и наоборот. Действительно, одна выводимость следует из другой с учетом i-правила; но так как результирующая формула i-символов не содержит, то применение i-правила может быть устранено.
Тем же самым способом мы можем убедиться в том, что в формализме, получающемся из @ путем присоединения явного определения
Ф (а, Ь, с) ~ ф (а, 6) = с,
формула, не содержащая функционального знака ф (-,•), выводима тогда и только тогда, когда она выводима в @>*.
Таким образом, формализмы @ и (&* оказываются равносильными в этом смысле слова.
Этот результат может быть немедленно распространен на случай произвольного числа функциональных знаков (с произвольным количеством аргументов) и произвольного числа аксиом для этих функций. Под этот случай подпадают и индивидные символы, так как их можно рассматривать как функциональные знаки без аргументов.
Итак, мы убеждаемся, что если за основу рассмотрения взять исчисление предикатов и аксиомы равенства, то всякая система аксиом, содержащая только собственные аксиомы и, быть может, аксиому индукции, будет равносильна такой системе аксиом, в которой функциональные и индивидные символы отсутствуют.
Замена системы аксиом рассмотренного типа, формализованной с применением функциональных знаков, равносильной системой аксиом без функциональных знаков дает, в частности, возможность (в том случае, если аксиома индукции среди аксиом не встречается) свести проблемы выводимости в этой системе и ее непротиворечивости к некоторым частным проблемам разрешимости в исчислении предикатов *).
Исключение индивидных символов не дает в этом смысле никаких преимуществ. Вообще, замена индивидного символа представляющим его предикатным символом по большей части
См. гл. IV с. 199—200.

 

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 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 541 542 543 544 545 546 547 548 549 550


Математика