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


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

'80 е-символ и ЛОГИЧЕСКИЙ ФОРМАЛИЗМ [гл HI
жащпя вхождений к-символа, будет выводима в F и без использо~ вания е-символа.
Следовательно, если какая-либо формула, построенная из символов и переменных исчисления предикатов и знака равенства, может быть выведена с использованием, кроме правил исчисления предикатов и аксиом равенства (Jx) и (J2), еще и символьных решений некоторых экзистенциальных формул, то эти символьные решения из данного вывода могут быть устранены.
Более того, из доказанного следует, что если какая-либо формула (? выведена с помощью исчисления предикатов, аксиом равенства и каких-либо собственных аксиом, а также с привлечением операции символьного решения экзистенциальных формул и если ни один из введенных при этом символов в формуле & не встречается, то эти символьные решения из вывода (? могут быть устранены.
Вместе с тем метод, с помощью которого нашу вторую е-тео-рему мы распространили на аксиому (J2), позволяет также доказать следующее утверждение:
Если формула (?, построенная из символов и переменных исчисления предикатов и каких-либо индивидных, функциональных и предикатных символов, но не содержащая знака равенства, выводима с помощью средств исчисления предикатов, г-формулы и аксиом равенства, то она выводима и средствами одного только исчисления предикатов.
Из этого утверждения, в частности, следует, что из вывода любой формулы (?, обладающей указанными свойствами, производимого с помощью средств исчисления предикатов и аксиом равенства (Ji), (J2), применение аксиом равенства может быть устранено.
Эту теорему мы в свое время доказали для случая, когда формула (? представляет собой формулу исчисления предикатов1). Приведенное там доказательство немедленно распространяется на случай формулы 6г, содержащей индивидные или предикатные символы, но оно не может быть распространено на случай, когда в (? встречаются функциональные символы.
Доказательство мы снова начнем с замечания о том, что без ограничения общности можно считать, что формула (? имеет вид сколемовской нормальной формы. Далее, в точности так же, как раньше, получается, что, используя вывод формулы Ф, можно найти некоторую формулу
©?&...&©?->?*, обладающую следующими свойствами:
.1) См. т.,1, с. 462—466.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 181 182 183 184 185 186 187 188 189 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 550 560 570 580 590 600 610 620 630 640 650


Математика