Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 101
Текст из файла (страница 101)
Возможно, что в целях предотвращения коллизий между связанными переменными при этом придется произвести некоторые переименования переменных. От явных определений следует отличать рекурсивные определения, которые фигурируют в арифметических фарясаяизмах. Арифметические формализмы характеризуются тем, что в иих содержится та или иная формализация натурального ряда. В качестве индивидного символа для исходного элемента натурального ряда мы берем знак О, а в качестве функционального знака, формализующего переход от данного числа к следующему за ним числу, мы берем штрих-символ. Построенные из символа 0 и штрих-символа термы такие, как О, 0', 0" и т. д., мы называем цифрами.
Введение же привычных числовых символов может быть произведено с помощью явных определений таких, например, как 1=0', 2=0", 3=0 и т. д. Структура натурального ряда позволяет использовать особого рода определения для функций, у которых значениями аргументов и значениями самих этих функций являются числа натурального ряда, который мы считаем начинающимся с нуля. Такие функции мы называем арифметическими. Именно, определение арифметических функций иногда может быть произведено таким образом, что нахождение значения функции для заданного числового значения некоторого выделенного аргумента сводится к нахождению значений для меньших значений этого аргумента; при этом нужно еще дополнительно задать значение функции (или соответственно пробег ее значений) для равного 0 значения данного аргумента.
Определения такого рода называются р е к у р с н в н ы м и определениями. Простейшим и важнейшим видом рекурсивных определений') арифметических функций является определение с помощью примитивной рекурсии или, более общо, с помощью последовательности примитивных рекурсий, каждый член которой вводит новый функциональный знак с одним или несколькими аргументами. Всякая примитивная рекурсия состоит д) В свяэи с этим см. т.
д, с, 352 — 357 и 40!. из пары рекурсивных равенств вида ( (с„..., сс, 0) = а (с„..., с!), ((сд, ..., сс, и')=Ь(сд, ..., с! п ((сы "° р с! п))р где ((" ) — вводимый функциональный знак, с„..., с! — какие-либо свободные переменные') (параметры этой рекурсии), а а(с„..., с!) и Ь(с„..., сс, и, лд) — определенные термы, которые, кроме указанных свободных индивндных переменных (впрочем, эти переменные не обязаны присутствовать в полном составе), символа 0 и штрих-символа, могут содержать в качестве составных частей лишь функциональ- ные знаки, введенные предшествующими примитивными рекур- сиями.
В частности, такой вид имеют рекурсивные равенства для сложения и умножения: а+О=а, а 0=0, а+и'=(а+п)', а п'=а и+а. Первая пара этих равенств дает рекурсивное определение сама по себе, а вторая — в том случае, если оиа вводится после первой. Функцию, рекурсивное определение которое дается некоторой примитивной рекурсией нли последовательностью примитивных рекурсий, мы кратко называем рекурсивной функцией.
Рекурсивные определения содержательно могут интерпретироваться как некоторые вычислительные процедуры, и в сочетании с аксиомами равенства они дают определенный способ формализованного вычисления значений рекурсивных функций такой, что если ((а„..., л,) представляет собой рекурсивную функцию, то для каждого набора цифр и,, ..., и, данное рекурсивное определение в сочетании с аксиомами равенства позволяет вывести равенство ((и„..., пс)=п, где цифра и представляет собой значение этой функции для набора аргументов и„ ..., и„ причем для получения этого вывода нам требуются средства одного только элементарного исчисления со свободными переменными.
Общее правило, позволяющее допускать рекурсивные равенства любых примитивных рекурсий в качестве исходных формул выводов, называется схемой примитивной рекурсии. Способу рекурсивного определения противостоит в качестве ~'Ф р Ф Р р ~ ~ Р 'рпр„,",.„...,„... ~ „р„р и иложания мая полная индукция (заключение от и к и+1). Одна из формализаций этого способа умозаключений дается так называе- мой схемой индукции 6 (0) Я (а) -ь 6 (а') а( (а) в которой требуется, чтобы в формуле л(0) отсутствовала пе е. менная а. а пере- Добавив к элементарному исчислению со свободными пе ными схе еременса му примитивнои рекурсии и схему индукции вмес ксиомами равенства и аксиомой 0'чьО, мы получим формализм те рекурсивной арифметики. взято Если в основу рассмотрения положить исчисление пре р дикатов, ии е в его полном составе, то упоминавшаяся выше схема ц будет равносильна так называемой аксиоме индукции'): индук- А (0) и Чх (А (х) -«.
А (х')) -«А (а). Систему арифметических аксиом, состоящую из аксиомы авенства (Юз), аксиом равен- (Р,) (Рз) а чьО, а' Ь'-+а=Ь, «) См. т. 1, с 325. ') См, т. 1, с. 4ЕХ а также рекурсивных равенств для сложения и умножения и аксиомы индукции, мы называем системой (Х), а фо состоя ий щ из исчисления предикатов и символов и аксиом системы (Е), мы называем фо р мал измом системы (Е) или, для краткости, формализмом (Е). А ксиомами (Рз), (Р,) и аксиомой индукции формализуются— на основе введения символа 0 и штрих-символа — аксиомы арифметики в том виде, как их, следуя Дедекинду, сформулировал Пеано.
Мы кратко называем эти аксиомы аксиомами Пе Пи е кт р д ду ианом построении арифметики на базе формализма я ля (У) с добавленным к нему «-правилом очень существенным ш в ется введение так называемого (ь-символа с помощью следующего явного определения: 1з,А(х) ьл((Чх ~А(г)-+х 0)бз (ЗгА(г)-+ А (х) йз Чи(А(и)- х~и))), Л ля этого нужно сначала о помощью «-правила') ввести стоящи в правой части этого равенства ь-терм.
Необходимые в дан- нисгвенносги выводятся с нспользовани формулы 1(а) -ь ~х(А (х) й Чу(А (у) -ьх~ у)). лпиФмвтичаскип Формализмы 4Я посредством которой формализуется так называемый принцип наименьшего числа, т. е. принцип, утверждающий, что для каждого числового предиката, выполняющегося хотя бы для одного числа, имеется наименьшее число, для которого этот предикат выполняется. Упомянутая формула выводится на основе явного определения ') а е- Ь Бх(а+х Ь) ') В т.
1 вместо этого явно«о определения мы использовали определения л ~ Ь лл(л Од«о+л а(Ь а Ь«Ул<Ь (см с. 438 и 358). Эквивалентность, используемая здесь для определения символа =, выводится нз этих двух формул. с помощью аксиомы индукции и аксиом (Яз), а+ 0 = а, а+ и' (а+ и)' н а' Ь'-ч. а Ь. Из приведенного выше явного определения для символа Р„А (х) при помощи ь-правила получаются формулы (р) ЗхА (х) -«- А (р„А (х)), (р) А (а) -ь рлА (х) ~ а, (1«з) «Ух 1А(х)-ьрлА(х) О.
Содержательно 1з-символ истолковывается следующим образом: для любого числового предиката 81(а) в том случае, если этот предикат выполняется хотя бы для одного числа, терм 1«„л(х) изображает наименьшее среди таких чисел, а в противном случае он изображает число О. Как это уже было отмечено в гл. ЧП т. $, рекурсивные определения для сложения и умножения в формалиаме системы (У) не могут быть-в отличие от явных определений — устранены при помощи каких-либо замен. Но зато все остальные определения функций, сформулированные в виде примитивных рекурсий, при условии добавления к формализму (Е) ь-символа могут быть свеЛены к явным определениям', это означает, что для любого рекурсивно введенного функционального знака вместо рекурсивного его определения можно указать такое явное определение, при помощи которого рекурсивные равенства этого рекурсивного 470 ТЕОРЕМЫ ОБ ИСЧИСЛЕНИИ ПРЕДИКАТОВ 47! ПРИЛОЖЕНИЕ 4 з! определения могут быть выведены').
Фо определения и онзв ). ормулировка такого явного я производится с использованием )г-символа. з факта сводимости рекурсивных определений к явным и с учетом теоремы об устранимости 1-правила получается сле в формализме (У): Всякой рекурсивной функции ((и„..., и ) может быт ставлена такая построенная из символов формализма (У) и д и„..., и, и), где и„..., п„п— встречающиеся в ней свободные переменные что для б аб ля лю ого набора мула 0(1„..., 1, в формализме системы (Е) будет вывод ф ) или ее отрицание в зависимости от того, равно или не равно цифре 7 значение втой ф нк ие вто функции для набора алее, при помвщи эквивалентности ((и„..., пс) =и б(п„..., п„, и) и соответствующих эквивалентностей для всех нк ий, чающихся в рекурсивном апред ф „..., и, если елении функции 1(п„..., и,) (если зти эквивалентности добавить к нашем аксиом), могут быть вывед нашему формализму в качестве 1'(Пх ".
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
