Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 16
Текст из файла (страница 16)
Если мы теперь зададимся вопросом о том, может ли система (Е') служить объектом применения нашей нп-теоремы, то обнаружим, что из-за наличия в (Х') схемы индукции применение этой теоремы (во всяком случае, прямое) оказывается невозможным. (Аксиома индукции, естественно, приводит к тем же самым трудностям, так как она не является собственной аксиомой.) Если же схему индукции опусгить, то, как легко убедиться, нп-теорема становится применимой.
Действительно, постоянные элементарные формулы системы (Е') представляют собой равенства между постоянными термами. Но эти термы либо сами являются цифрами, либо строятся из цифр с помощью знаков сложения и умножения. Как известно, для таких термов имеется процедура рекурсивного вычисления их значений (она основывается на использовании рекурсивных равенств для сложения и умножения в качестве фннитно понимаемых инструкций для выполнения соответствующих действий) и эта процедура всегда дает в качестве значения такого терма некоторую цифру.
Таким образом, любое равенство между постоянными термами после вычисления значений этих термов переходит в некоторое равенство между цифрами и такое равенство 6=1 мы объявляем, как это делалось и раньше, истинным или ложным в зависимости от того, совпадает или не совпадаег цифра в с цифрой ц При таком распределении истинностиых значений постоянных элементарных формул все аксиомы системы (Е'), как легко убедиться '), оказываются верифицируемыми формулами. Поэтому для системы (2') при условии исключения из нее схемы индукции будут справедливы все утверждения нашей ип-теоремы и, в частности, утверждение о том, что всякая выводимая формула, ие содержащая ни связанных индивидных, ни формульных переменных, является верифицируемой. Все эти утверждения остаются в силе и в том случае, если к аксиомам системы (Х') добавить в качестве исходных формул какие-либо новые верифицируемые формулы этой формальной системы, т.
е. такие формулы этого формализма, не содержащие никаких других переменных, кроме свободных нндивидных, которые при только что рассмотренном определении 1) В связи с рекурсивными равенствами см, рассуждение в гл. ЧН т. 1, с. 359. Е 77 Ф и ПРИМЕ именение нп-теоРемы к АРиеметик нностных значений постоянных элементарных формул при любой заме е вободн х пер м ине фо м лы. Действительно, при д авлении павия применимости нп-теоремы продал.
в к качестве исходных условия п жают ост аваться выполненными. яет включить в наш результат схему Это обстоятельство позволяет в условии, айней ме е частично,а именно при "- мулам без св б дет применяться лишь к р е чтобы бедиться в этом, нам ных переменных.
В самом деле, что ы у ж ение, проведенное в гл. . Чи7.1 дос остаточно повторить рассужд, р п отиво ечивости рекурсивно ари любого и ове)юг«гю«тз Из э р этого ассуждения получается, что у лю ог (Е') тельства такого, что схема индукц к ии средствами системы (Е ) доказател а(о) а(Е а~ ) а~4 применяетс я в нем только к формулам 7((с) без связанных я фо м ла всякого вхождения схемы Сл льно при я ве ифицируемой '). едовате индукции оказывается р р к ии во всяком таком доказа ательстве равменение схемы индукц (Г) некоторого числа обавлению к аксиомам системы насильно д м л.
Отсюда, согласно сделанному выше атриаасмый фо мализм включить аксиому ыду~~~щ формализму будут выполнены фо мализму ся и в том случае, если мы добавим к з, рм выполняться и в том й урсии. В самом деле, любой ей вид примитивной рекурсии схем примитивной рекурсии. паре рекур сивных равенств, имеюще вид тельно-финитного истолковани я ек сии ') — некоторая вычислительная процедур, тв ет — в смысле содержатель а дставляющему собой посредством которои каждому терму функциональный знак с аргуме ментами в виде ци р, соп его значения вполне определенная цифра, л в качестве его з результате введения какихстоянных термов, получающ л чающихся в оп е еленное расых нкциональных знаков, это дает опреде з ' ° ° - ф ° пределение значений этих термов.
и ым асп еделением, упомянуты данным р р ные равенства оказываются вер ц, „ е ифицируемыми орму что при лю о б й замене свободных переменных цифрами с з) См. т. 1, с 364 — 366. ° ) См. т. 1, с. 364. «) См. т. 1, с. 61 — 63 78 исследование Авифметикн НРИ помощи -символа 1гл и дующим вычислением значений термов равенгтва эти переходят в равенства вида д = б. То же самое справедливо и а отношении схемы перекрестной рекурсии. И, вообще, не нарушая условий применимости нашей нп-теоремы, мы можем допустить введение (при помощи соответствующих систем равенств) любого числа новых функциональных -знаков или — еще более общо — введение новых аксиом, если при этом: 1) рассматриваемые аксиомы являются собственными аксиомами без связанных переменных и 2) указывается какой-либо способ, который каждому из добавляемых постоянных термов сопоставляет в качестве его значения вполне определенную цифру и на основе которого эти новые аксиомы оказываются верифицируемыми формулами ').
При таком введении функциональных знаков в соответствии с упомянутыми условиями всегда можно брать в качестве аксиом связанные с этими знаками (или соответственно с их аргументами) формулы равенства ') а = Ь - ( (а) 1(Ь), Действительно, в силу указанного распределения значений постоянных термов любая такая формула является верифнцируемой, потому что если вместо входящих в эту формулу переменных подставить какие-либо цифры, а затем заменить получившиеся постоянные термы их значениями, то в том случае, когда переменные а и Ь заменяются равными цифрами, у иас получится формула вида 8=8 '8-8, где й-цифра, являющаяся значением терма ((х); а в том случае, когда а и Ь будут заменены отличными друг от друга цифрами х г) Одии обшдй способ введеиив новых фуиациовальиых аваков при помощи аксиом был использован Эрбрацом в его работе; Н е ~ Ь г а и б Л.
Ецг 1а попсоц1гавдсноп бе ГАг))ьщ4119ца.— Л. ге)па аокачч. Мащ., 1981, '166 (абгооре Св), Этот способ является иесколько более частным, чам способ. црвмевеииый здесь, поскольку Эрбраи трабувг, чтобы процедура вахождеикя авачеивй, вак и в схемах ревурсивиых оораделеиий. получалась фивитным истолкованием аксиом.— Относительно понятия общарецурсиввой функции в том виде как его, следув Эрбраву, излагают Гедель и Клива, а также огиоситальво других примывающвх и нему понятий см.
гл. Ч, с. 421 и Приложение П, с. 477 и 489. а) Заццсь такой формулы, иаи ато ужа делалось вами в гл. ЧП т. ! (см. с. 458), всегда понимается таким образом, что у рассматриваемого функциоиальиого знака 1, кроме указанных аргумеичов, допускается иаличиа каких-нибудь других, которые в атом случае в обеих частях рававства иа одииаховых местах должны быть соотвагствеиио одинаковыми, отличиымя от и, от Ь и друг Рт друга гвободиымц иидивидвыми церемеииыми, пРименение нп-теоРеЫы к АРиометике и,),уна нас получится формула вида г=й- 8=1. лы истинны: первая потому, что истинно ее Ио обе эти фора'Улы и о ложна ее посылка а=)). и б=б, а втоРаЯ потомУ, чт заключение = * ЧП 1 обобц(смпл схемы индукции, РассмотРенные в гл. т ограничения, наложенные дак1шие Частичиу ю компенсацию за ог на эту схему, .
тоже согласуютсл с наш ей нп-теоремой, потому '), одятся при помощи прими- что онн, а у , к к мы же установили, св е индукции нашей рекурсивной тинных рекурсий к обычной схеме инду е ем итог п оведенным нами рассмотрениям. Вонепосредственно римечаю ем ся в результате объединения (2') (б исчисления предик икатов с аксиомами системы ему формализму, не индукции)., а ии . Далее, мы выяснили, что к эт емы можно добавить: Ц схему о м л без связанных переменных, 2) схемы п именимости нп-теоремы, м 3) аксиомы равенства для имой ф нкции. Тем самым в рассмотрение те лишь о ии е включается вся рекурсивная арифметика — с м нием, что вмес сто общей аксиомы равенства а = Ь -э (А (а) -ь А (Ь)) б т фигурировать некоторые ее частные случаи. у нас удут жиг зультата подсказывается самой форе кото ая недвусмысленным образом дообоб ение этого результата мулир акой ж-~нор~~, которая ие в ассмат„иваемы рмал м пускает включение в р лы.
Как мы уже знаем, при введении в- о в-формулы ь-правило в.формулы. Ек м ) становится производным. Поэтому (т. е. пр авило с «е» вместо щл ста может быть включено в наш получает ся что ыправило тоже мо и на теорему об устранимости ь-пра- результат, причем без ссылки на теор вила из гл. . АЛ11 т. 1. б„азом приходим, содержит Формализм, к которому мы таким о следующие компоненты: 1. Формализм исчисления предикатов. 2. Формализм з-символа и в-формулы.
катный символ =, индивидны символ 3. Предикат символ (функциональны знак й ак) вместе с относящимися к ним аксиомами а а, а=Ь-+ (а=с-~Ье с), Ф Ф а=Ь-+и = ° 0'~0. а) См. т. 1, о.419 — 497. 81 80 исса ЯДОВАНИЕ АРнфмвтИКИ ПРИ ПОМОЩИ и-СИМВОЛА 1гл. и пРименения нп-ТЕОРямы к АРНФмятикя 4 11 4. Схему индукции рекурсивной арифметики (при этом применять ее допускается лишь к формулам без связанных переменных). 5. Схемы для введения функциональных знаков при помощи таких рекурсивных равенств (или соответственно таких собственных аксиом без связанных переменных), которые при финитном распределении значений добавляющихся при этом постоянных термов оказываются верифицируемыми формулами. 6.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
