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


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

МО ПРИЛОЖЕНИЕ [IV
можно ввести символ f для функционала. Но из этого равенства с помощью формулы (4) в результате применения подстановки функции -вместо переменной и выводится формула
НО- в (О-
В качестве еще одной выводимой схемы для определения функционалов упомянем схему
f-8, ;
где f — вновь вводимый символ для функционала, а д— функ- : ционал. В самом деле, всякая формула этого вида, если свободная индивидная переменная с в нее не входит, дедуктивно равна формуле
НО = 8(0-
В дальнейшем, вводя явные определения для тех или иных интересующих нас функционалов, мы будем пользоваться обеими этими выводимыми схемами определений.
После этого замечания мы перейдем к фундаментальной теореме, утверждающей существование точной верхней границы у любого непустого ограниченного сверху (т. е. имеющего какую-либо верхнюю границу) множества положительных действительных чисел.
С учетом выбранного определения теорема эта в нашем формализме может быть изображена следующей формулой:
(5) Vx (А (х) -У в ( *)) & Зх А (х) & 3yVx (А (х) -> * (0)< у) -> 3z {в (z) & Vx (A (x)-»x^z)& Vy (Vx (А(х)-+х^у)-+г^ у)}.
Эта формула может быть выведена с использованием функционала v-xA (х), вводимого следующим определяющим равенством:
(V- А (х)) (п) = ^Vx (А (х) ->*(/!)==? г).
В самом деле, из этого определения применением формул (^ и мы получим формулу
(5а)
Vx (А (х)-+ х (п) ^ (V- А (г)) (п)) &
(Vx (А (х) -+х(п)^:а)-+ ^ А (г)) (п) ^ а),
откуда далее с помощью выводимой формулы
в (d) & и (0)< Ь -+ Vx (и (х)<Ь- 2х)

 

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 550 560 561 562 563 564 565 566 567 568 569 570 580 590 600 610 620 630 640 650


Математика