Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 58
Текст из файла (страница 58)
с. 162. ') См. !1рнложенне 1, с. 468. а) Это было сделано в его новаторской работе: бобе) К ()1гег гоппа! ппеп1»сьегбьаге я!ае бег Рг)пс)рга Майегпа1)са ппб чегтчапщег яуа)егпе.— Мопа1»Л. Май. Р!гуа., !931, 38, 5. !73 — 198. Агиемптизация исчисления првдиклтов йп МЕТОЛ АРИФМРТИЗАЦСССС МГТАМАТГМАТИКН !ГЛ СЧ тельности ними'). Это утверждение справедливо даже независимо от того, что метаматематика по своему характеру является финитной. Но для фииитиой метаматематики ее арифметическую модель можно, кроме того, построить в виде финитно-арифметической модели.
Эги принципиальные соображения сами по себе, конечно, еще не дают никакого конкретного способа арнфметизации. Но главная трудность заключается в том, что вообще заранее нельзя предвидеть, удастся ли математические соотношения, имеющие место в данной арифметической модели метаматематики, проследить настолько эффективно, насколько это требуется для наших применений; к тому же с этой арифметизацией мы должны связать еще и формализацию метаматематнки. Гйдель показал, что средств рекурсивной арифметики вполне достаточно для математического построения такой модели и для ее формализации. Используемый им метод арифметизации состоит в арифметическом имитировании линейного расположения знаков в формулах формализованной математики.
Действительно, логическую и математическую символику мы всегда можем выбрать таким образом, чтобы расположение символов и переменных в формулах было строго линейным. Если теперь каждому символу, каждой переменной, а также скобкам и запятой сопоставить некоторые цифры (номера данных знаков), то всякой формуле будет взаимно однозначно сопоставлена некоторая цепочка цифра). Затем, пользуясь однозначностью разложения чисел иа простые множители, каждой (конечной) последовательности цифр можно, как было показано ранее'), взаимно однозначным образом поставить в соответствие некоторую цифру: а именно, последова- с) Такую модель можно расеыатраеать а как модель, выполняющую некоторую «я«тему аксиом, потому что ыетаыатематика любого дедуктаацого форыалнэыа асегдз может быть акевоыатязароааца На такую возможность впервые указал А, Тарский (А.
Та!ай!) е слоях работах: Е!и!йе Ве1гасщцссбеп йЬег сне Вейг!Не бег ы-%!бегзргцсьз!ге!Ье!1 ццб бег ю-Чо!!з(йцб!басе!1.— Мопа1зЬ. Марш РЬуз., 1933, 40, я Оег цгаьгье!1»ьейг!!! !и бец !огта1сыег(ец ЗргаеЬеп.— Тгач. Яос. Яе!. Чагэоч!е, 1933, немецкий перевод а Я(цб!з ры1оз., 1935, а которых оа, кроме того, дал ацсиоыатачесцое оцределецяе понятия вы р а же я и я длэ некоторых ледуктяаяых формализмов. Общий подход к ацсаоыатцзацяи метаыатемагэзя дедуктивных формализмов кратко обрисован Г, Гермесом з его докладе; Негшез Н. Есп Ах!ошецзуз1есп Гбг сце Зуп1ах без (Ыазз!зсьесс) 1.ой№1са11сц!з.
— Тгач. дц !Х еоойг. бе р!й1оз., Раг!з, 1937, № б. ') Идея такого азображеаяа форыульных аыражецяй последовательностями цифр ц, тем самым, переаодэ правил построения формальных еыраж»иай и призеденяа формальных доцаэательсга ц арифыетаческяы араэалам была высказана Гальбертоы уже а процессе его раэыышленай аад аантороэскай пРоблемой континуума.
Но а то время реализация этой идеи казалась слишком сложной. ») См. т. 1, с. 394 — 395. и„..., в, ставится в соответствие цифра )эз ° ° ° )э с — с г е,", )э, ..., )э с — первые г простых чисел. Таким образом . П нменив каждая формула изобразится присвоенным ей номером. Прн е аналогичный прием еше раз, можно с помощью номеров охарактеризовать и конечные списки формул. При этом списку, состоящему из формул с номерами и„..., п„будет сопоставлен номер )ээ . 1э' г-с Т б азом, мы будем иметь дело с тремя типами нумераций аким о р пей знаков об теории доказательств: во-первых, с нумерацией ъектов р являющихся составными частями формул', во-вторых, у р формул н, в-третьих, с нумерацией списков формул, в частности доказательств.
С помощью этих нумераций структурные свойства формул и списков формул, а также отношения между ними изобразятся некоторыми а и м ми арифметическими свойствами и отнопсениямн. Однако арифметизацию можно осуществить и несколько иным б: вместо того чтобы воспроизводить способ записи формул, ст кт . Отлимы можем проимилгировать их грамматическую структуру. чительной чертой этого способа будет то, что предикатам, символам и функцион нальным знакам, а также знакам логических о ые а и метические операций мы сопоставим не номера, а некоторые арифме функции.
Для начала мы изложим этот способ в применении к исчислению предикатов. бо ных и Фо мулы исчисления предикатов строятся из сво одных и связанных индивидных переменных, формуль орм льных пе сменных Р с а г ментами н без них'), а также нз символов исчисления с аргументами н высказываний и кванторов всеобщности и сущ с ествования. В качестве номеров для связанных переменных мы возьмем простые '), лич ые от чисел 2, 3 и 5, а в качестве номеров для свободйых индивидных переменных — числа вида р, р— простое число, ббльшее б. В качестве номеров для формульных жлеаае переменных любого т па, ) Здесь ыы цредполэгаеы, что поро е я ~" ыульцых перемеяаых с л ыы чцс о з тоы числе я ~"р у й последовательности, цодобвой нату- водится а виде векоторой цеограацченно и «) Таз как эта арафыетцэац аф ацаа производится э рамках содержашельлой арафыетакя, ыы говорим здесь о «часлах», а це о «цафрах».
метод дпиеметиздции мгтлмхтгмлтики переменных без аргументов мы возьмем числа вида 10 р, где р — простое число, ббльшее 5. Формульиые переменные с 1 аргументами мы будем изображать 1-местнымн функциями вида где оы ..., ог — простые числа, ббльшие 5 и такие, что и; -я. о . при 1~!<1. Это представление формульной переменной нужно понимать следующим образом: выражение, состоящее из формульной переменной с аргументами, номера которых (расположенные в порядке следования аргументов) суть пм ..., пп в качестве номера получает число Это сопоставление номеров и функций выбирается таким образом, чтобы соответствие между всеми простыми числами, ббльшими 5, и всеми связанными переменными, между всеми числами этого рода, умноженными на 2, и всеми свободными индивидными переменными, между всеми числами этого рода, умноженными на 10, и всеми формульными переменными без аргументов, а также (при любом 1) между упорядоченными по возрастанию всеми 1-членными наборами простых чисел, ббльших 5, и всеми формульными переменными с ! аргументами было взаимно однозначным ').
Для логических операций мы возьмем следующие нх изображения: для отрицания †умножен иа 3, для конъюнкции †функц 20 7" 11", для дизъюнкции †функц 40 7" 1 Р, для импликации †функц 80 7".!1', для эквивалентности †функц !60 7".11». Квннтор всеобщности мы изобразим функцией 50 яа, а квантор СущЕСтВОВаНИя — фуНКцИЕЙ 100 яа, ГдЕ В ОбОИХ СЛуЧаяХ П ПрЕдставляет собой номер связанной переменной, стоящей за квантором, а вместо а подставляется номер выражения, представляющего собой область действия этого квантора.
Для арифметизации рассмотрений, связанных с проблемой разрешимости, нам еще потребуется какое-либо изображение цифр и функциональных знаков'). В качестве номера для цифры и з) Сопостввление Ьместных бюрмульных переменных упорядоченным пп впзрвствнию Ьчленным наборам, состояньям нз простых чисел, больших б, может быть получено нв основе перечислимосги згих наборов из какого-либо перечисления Ьместных формульных переменных. *) Мы считаем, что для любого О может быть произведено неограниченное порождение Г-местных функпнопвльных знаков. эя днпеметиздция исчисления пгеднкхтои мы возьмем число а вс 2.
3о який 1-местный функциональный знак мы изобразим какой-либо функцией а аг 5 и',г ...-и где о„..., по — упоряд оченные по возрастанию простые числа, б . ерация не зависит от тех или е 5. Выб анная таким о разом нум ", касаю ихся конкретного способа записи фор- иных соглашений, касающ штрих-символа ущесгвенным слн п оизвести нумерацию каких-либо конкретно нап захотим прои б ополнительно условиться ных форму, л, то нам н жно удет д етных б кв, изображающих те или относительно нумерации конкретных укв, с нашими и нме в полном соответствии с иа иные переменные. Например, ями можно условиться, что номерами п определениями 7, 11 и 13, номерами переменных и г будут считаться числа , и енных — а 14, 22 и 26, номерами формульных переменны А, В и С без аргументов-числа 70, 11О и и , В С переменные А, и с одни м аргументом будут изображаться соответственно функциями 1О 7, '1О !1' и 10 13', а формульная переменная А с двумя аргументами — функцией 10.
7а. 1 !о 11ри этом формула А бо В - В бг А получит в качестве номера число 8о 7 7(оо.т|о т,ц1о и) 11(оо.гм и 1 ~о г\ точнее говоря, число, являющ ляющееся результатом вычисления зна(чения этого арифметического выражения), формула зйхА (х)-ь А (с) получит номер 80 7<з'т по'г ' 1!< ю'™> а формула )ЛхУуА (х, у) )/ УхЛуА (у, х) получит номер 40 7гзоо г (зол~по т'цгч]) 1 1(оо. гбоол' ), Основное требование, которому должна удовлетворять эта нуме- 271 МЕТОД АРИФМЕТИЗАЦИИ МЕТАМАТЕМАТИКИ 1гл щ 4 П Рация, заключается в том, что различные выражения должны иметь различные номера.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
