Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 120
Текст из файла (страница 120)
С учетом выбранного определения теорема эта в нашем формализме может быть изображена следующей формулой: (5) Ух (А (х) -+ О (х)) й ЛхА (х) й Буях (А (х) -~- х (0) (у) -~- 'Вг(В (г) йУх(А (х)-~-х~г) йУу(чх(А(х) — ~х.~у)-~-г ' у)). Эта формула может быть выведена с использованием функционала Т„А (х), вводимого следующим определяющим равенством: (Р„А (х)) (и) = р, Чх (А (х) -~ х (и) «г). В самом деле, из этого определения применением формул (р,) и (1сс) мы полУчим фоРмУлУ (ба) УиЗуех(А(х)-~х(и) =у)-~ Чй(А(х) — ~х(и) ((т;А (г))(а))й (тсх(А(х)-~х(и) ~а)-Р(т;А(г))(а) =а) откуда далее с помощью выводимой формулы В (й) й д (0) < Ь -~- Ух (й (х) ~ Ь 2") и с использованием определения символа О получим формулу (5Ь) Чх(А (х)-~-В(х)) йЗхА (х) й Буях(А (х)-~.х(0) (у)-» 8(ч;А (г))й Чх(А (х) -~-х -т;А (г))й (Чх (А (х) -~- х ( с) -1- т; А (г) ( с) из которой средствами исчисления предикатов немедленно получается требующаяся нам формула (5).
Основная идея этого вывода заключается в том, что точная верхняя граница любого непустого ограниченного сверху множества положительных действительных чисел строится как числовая последовательность а„а„..., где а„(при Л=О, 1, 2, ...) представляет собой наибольшее из чисел, являющихся а-ми членами числовых последовательностей, принадлежаицнх рассматриваемому множеству. К нашему определению функционала т;А(х) можно еще сделать следующее замечание. Если положить 0 — -)сх(0 х), то с помощью формулы (5а) можно будет вывести формулу Чх 1 А (х) -~- т;А (х) — О. Эта формула в сочетании с формулой (5Ь) и без труда выводимой формулой О ~й даст нам формулу (5с) Ух (А (2) -+ В (х)) й Буях (А (х) -1- х (0) ~ у) -~ (0(т;А (г)) 1/ т;А (г) — 0)й чсх(А(х)-+х~т;А(г))й Чу(7х(А (х)-+ х ~у-Рт;А(г) ~у).
Замечание. Хотя введенный функционал 0 и не изображает никакого числа интересующего нас типа (на самом деле легко может быть выведена формула )6(0)), тем не менее введение этого функционала для нашей формализации теории положительных действительных чисел оказывается полезным.
Теперь, чтобы ввести сложение и умножение рассматриваемых нами чисел, мы сначала определим функцию п(а, Ь), положив п(а, Ь) =р„Чу(а=Ь х+уйу(Ь) Нз этого равенства может быть выведена формула Ь Ф 0 — Ь п (а, Ь) -=. а й а ( Ь и (а„Ь) + Ь. С помощью функции и (а, Ь) можно следующим образом определить сумму и произведение двух чисел рассматриваемого % З! теория положительных депствительных чисел 563 еЕ2 пч ПРИЛОЖЕНИЕ нами типа: (Ь (г Ь) (и) = р,!е'г (и (й (п+ г) + Ь (и+ г), 2') «х), (й ='С Ь) (и) = р,!ег (я (й (и+ г) Ь (и+ г), 2" +'*) «х). Из этих равенств сначала может быть выведена формула 6 (й) й 6 (Ь) е-Э (й фь Ь) й 6 (й Ь).
Затем могут быть получены (в виде выводимых формул) обыч- ные законы для арифметических действий, например такие, как йчРЬ вЂ” Ьфгй, Е (й) а Е (Ь) а Е (с) -а й >«(Б Ф с) — (й:ъС Ь) )Ь (й с). Мы получим также формулу 6 (й) й 6 (Ь) — (й «.Ь вЂ” Зх (й )ф й — Ь).
Кроме того, если при помощи равенства (Ьой) (и) =р,!!уг(п(Ь й(и+г), 2') «х) определить умножение положительных действительных чисел на натуральные, то можно будет получить формулы 6 (й) й Ь чь Ое-е(йой), Оой-О, и'ой-(пой) 4)й, е(й)ае(ь)- эх(Ь~хой).
Последняя из этих формул представляет собой формальное выра-'' жение того факта, что для рассматриваемых нами положительных действительных чисел выполняется аксиома Архимеда. Вычитание и деление рассматриваемых чисел можно форма- лизовать с помощью следующих определений *): й — ' ь — ' у„(е (х) а х Ф ь «й), —.— т„(6(х) ах >с Ь«й), из которых можно будет вывести формулы й«Ье-й — Ь='О, 6(й)йе(Ь)-е-(йфЬ) — Ь й, 6(й)ае(Ь)аь~й- 6(й — Ь)а(й--Ь) 1фЬ- й, 6(й)ае(ь)- 6( — '.)а-'.-::ьм й. ') Функционал а — ' Ь следует отлнчать от введенной в т. 1 (е.
370) функ.. цнн а — 'Ь.— Прим, нерее. Если теперь положить |й — ь! - (й — Ь) й) (Ь вЂ” й), то можно будет получить формулы |й — 'й| — 'О, 6(й)-~.|й — '0| — 'й, 6(й)йе(Ь)ййФЬ-е.е(|й — Ь/), |й — Ь/=|Ь вЂ” й|, 6(й)йе(Ь)аь~й ,'|й — ь'|-й — Ь, из которых становится ясно, что функционал |й — Ь| дает фор- мализацию понятия расстояния между двумя числами интересую- щего нас типа, т.
е., выражаясь в обычных математических тер- минах, понятия абсолютной величины их разности. Таким образом, мы определили все алгебраические операции для положительных действительных чисел. Для анализа положительных величин требуется еще одно фундаментальное понятие в понятие последовательности положи- тельных действительных чисел. Нужны также и различные свя- занные с такими последовательностями понятия: в частности, понятие сходимости данной последовательности к пределу. Подобно тому как понятие положительного действительного числа формализуется с помощью предикатного символа 6 (й), понятие последовательности таких чисел может быть формализо- вано с помощью символа 6,(й), который вводится следующим определением: 6! (й) !!ухе (Л,й (т (х, г))). Замечание.
Возможность представлять последовательности чисел интересующего нас типа с помощью функционалов основывается на возможности взаимно однозначного отображения последовательностей арифметических функций на сами функции. Эта возможность в свою очередь основывается на взаимно однозначной отобразимости числовых пар на числа. Мы пользуемся здесь тем отображением числовых пар на числа, которое дается нам функцией т(а, Ь). С учетом изображения с помощью функционала а последовательности арифметических функций в виде Л,а(т(п, г)), понятия элемента данной последовательности и ее подпоследовател ьности могут быть формализованы при помощи определений Е!(й, Ь) (х (й — Л,Ь (т (х, г))) и й С Ь !е'хауз!г(й(т(х, г)) = Ь(т(у, г))). Нз этих определений могут быть выведены формулы й С Ь Ю (Е1(х, й) -~- Е1 (х, Ь)) ПРИЛОЖЕНИЕ [!У с з[ ТЕОРИЯ ПОЛОЖИТЕЛЬНЫХ ДЕИСТВИТЕЛЬИЫХ ЧИСЕЛ 565 И д С Ьйб,(Ь) О,(д).
Понятие сходимоети последовательности чисел интересующего нас типа к пределу формализуется следующим определением: Су(д, Ь) 6,(а)й(6(Ь) Ч Ь ='-0)й Ухну)7г(у ~г — ~-[)с,д(т(г, и)) — Ь [(х) =О) '). Пусть 1п1;А (х) — символ, вводимый определением 1п1„А(х) Ух)йуЭг[А(г)й [си(и~у — ~гФ)),х(т(и, о)))1.
Тогда понятие бесконечного множества положительных действительных чисел может быть формализовано определением Г;А (х) Ух (А (х) -~. 6 (х)) й 1п1;А (х). Теорема о том, что всякое ограниченное сверху бесконечное множество положительных действительных чисел имеет пределеную точку, с использованием определений Г„*А (д) Г;А (х) й =[у)[[х (А (х) — ~- х (О) (у) Стп; (А (х, Ь)) [т и=[х (А (х) й х чь Ь й / х — Ь ! (и) = О) изображается формулой (6) Г'„'А(х)-эЗу((6(у) [/ у — 'О) йСш;(А(х), у)). Вывод этой формулы может быть построен с использованием.
формулы (5с) формализацией понятия верхнего предела (т. е. по-' нятия наибольшей предельной точки). Зту формализацию нам! дает определение У„А (х) — У; ~6 (х) й Уу (О (у) й у ( х -~-1п1; (А (г) й у г)Ц. На основании этого определения из формулы (5с) получается формула ГТА (х) -э- (6 (у„А (х)) Ч у„А (х) = О) й Туу(6(у)йу(У„А (х)-а-1п1 (А(г) йу(г))й [[[у(6(у) йУ„А (х) ~у-а.
11п1; (А (г) йу( г)),;", а из нее требующаяся нам формула (6) получается с использо.' ванием определения для 1п1„А(х), а также выводимых форму' Умах (6 (х) й Уг (6 (г) й г ~ х-а. г (и) = О)) т) Вместо 0 а — Э ~)(с) мы дли краткости пишем [а — З [(с). и 6(д) )уиЗхЛу(6(х)й6(у)йх(дйд(уй 'и г (6 (г) й х ~ г й г ~ у -~ ' г — д ~ (и) = О)). Заслуживает упоминания еще один, имеющий принципиальное значение вопрос теории положительных действительных чисел.
Мы имеем в виду некоторый применяемый в этой теории частный случай принципа вь)бора. В рассматриваемом случае этот принцип утверждает, что если для любого натурального числа и существует положительное действительное число с, находящееся с и в отношении 6 (и, с), то существует последовательность е„ с„ ... чисел рассматриваемого типа, обладающая тем свойством, что для любого п выполняется отношение 6(п, с„)'). Перевод этого высказывания в рассматриваемый формализм приводит нас к формуле (7) [[[хну(6(у)йА(х, у)) — )-=[у[6т(у)йтхА(х, ~„у(т(х, г)))Д.
Правда, вывести эту формулу в формализме Н мы не можем, потому что здесь в нашем распоряжении нет формулы д ='- Ь-~(А(д)-~ А(Ь)). Но эта трудность происходит только от того, что при изображении данного частного случая принципа выбора формулой (7) формализация понятия произвольного отношения между натуральным числом и и положительным действительным числом с, произведенная нами при помощи формульной переменной А(п, д), приводит к тому, что становятся возможными излишне общие подстановки. На самом деле для любой формулы е[(с) такой, что она формализует какое-либо математическое высказывание о числах интеРесующего нас типа, формула д ' Ь вЂ )-(Е[(д) -м )г[(Ь)) выводима в нашем формализме Н.
Зто обстоятельство делает возможным применение следующего приема: с помощью эквивалентности Ех[;А(х) ЧХЧу(х-)-у-м(А(х)-~А(у))) мы определяем символ Ех1 А (х) и добавляем в посылку формулы (7) в качестве конъюнктивного члена формулу )[[хЕх[„А(х, у). )В ! 69 )О, ПРИЛОЖЕНИЕ Возникающая таким образом формула (7а) 1Ух Ех1„А (х, у) й ЧхЛу (6 (у) й А (х, у)) -~. Лу[6,(у)йУЛЛ(х, Л,у(т(х, г)))] достаточным образом формализует рассматриваемый частный случай принципа выбора. С другой стороны, эта формула выводима в нашем формализме. Действительно, сначала можно получить формулу (7Ь) Ух Ех1„.
А (х, у) й Ух1уА (х, у) -+. Бу ТСЛА (х, Лу (т (х, г))). Это делается следующим образом. Если посредством с обозначить функционал Л„[[е А(т,(у), г[(т,(у))[ то с помощью формулы (Л„й(х)) (с) = й(с) можно будет вывести формулы (е;А (а, г))(Ь)=(Л,с(т(а, г))) (Ь), а тем самым и формулу е;А(а, г) -Л,с(с(а, г)). Из этой формулы может быть получена импликация Ех1„А(а, у)-~(А(а, е;А(а, г))-+ А(а, Л,с(т(а, г)))). С другой стороны, с по~1ощью трегьей е-формулы может быть получена формула ЛуА (а, у) -~ А (а, е; А (а, г)). Эти две формулы, взятые совместно, дают формулу Ех(„А (а, у) й 1уА (а, у)-~ А (а, Л,с (т(а, г))), а также формулу 7х Е х1„А (х, у) й УЛЗу А (х, у) — ~ УЕА (х, Л,с (т (х, г))), а из этой формулы, применяя формулу А (с) -~- (у А (у), мы получаем требующуюся нам формулу (7Ь).
Но подставив в (7Ь) вместо именной формы А (а, с) формулу 6(с)й А(а, с) и воспользовавшись выводимостью формул Ех1„.Л(а, у)-+ Ех1„(6(у)йЛ(а, у)) и 'чх6(Л,Ь(т(х, г)))-~-6,(Ь), мы получим формулу (7а). фи ТЕОРИЯ ПОЛОЖИТГЛЬИЫХ ДЕЙСТЕИТРЛЬИЫХ ЧИСЕЛ %7 С помощью формулы (7а) можно, в частности, вывести формулу (8) Ю (А (х) — ~ 6 (х)) й Ех1„А (х) й Сш„(А (х), Ь) -е=)Х[6т(х) й 1си(А (Л,х(т(и, г))) й Л,х(т(и, г))~Ьй[Л,х(т(и, г)) — Ь[(и)=0)], представляющую собой формализацию теоремы о том, что нз любого множества чисел интересующего нас типа, которое имеет предельную точку, можно выбрать последовательность, сходящуюся к этой точке. Формула (8), взятая вместе с формулой (8), дает формулу (9) Г„'А (х) й Ех(; А (Х) -~.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
