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