Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

виде теории первого порядка, которая оказывается достаточной для вывода всех основных результатов элементарной арифметики. Формальной арифметикой (теорией S) называем теорию первого порядка, имеющую: единственную предикатную букву Aj ; единственную предметную постоянную aj; три функциональные буквы f i , fi , f2 \ кроме того, очевидно, ее символами являются —i, ), (, ' , xi, Х2,..., Vxi, Vx2,...,3xi,3Х2,... . Чтобы использовать привычные для нас записи, обозначим (t,s) через t=s, aj через О, f}(t) через Г, fi 4&pQ3t+s, •у /2 (t,s) через t »s { •- понимается как знак умножения). Как известно, аксиомы каждой теории первого порядка, следовательно, и формальной арифметики, делятся на две группы: логические аксиомы - аксиомы ^7-^5 и собственные аксиомы. Собственными аксиомами формальной арифметики являются следующие формулы: S1: Xi= Х2^((Xi= Хз)^(Х2= Хз)): S2: Xi= X2^Xi'= Х2': S3: О ^Xj': S4: Xi'=X2'^Xi= Х2: S5: Xi+0= Xj; S6: Xi+x2'=(xi+X2) S7: Xi »0=0: S8: Xi»X2'=Xi»X2+x f , S9: A(Q)^(Vx,(A(xi)^A(x,'))^VxA(xi)), где A{Xi) - произвольная формула теории S. Напомним, что правилами вывода любой теории первого порядка являются правилам/* и Gen. Рассмотрим собственные аксиомы теории S и сравним их с аксиомами Пеано. Заметим, что аксиомы S1 - S8 являются конкретными формулами, в то время как S9 представляет собой схему аксиом, порождающую бесконечное множество аксиом. Аксиомы S1 и S2 обеспечивают некоторые необходимые свойства равенства, которые Дедекиндом и Пеано предполагались как интуитивно очевидные. Аксиомы S3 и S4 соответствуют аксиомам РЗ и Р4 системы аксиом Пеано. Аксиомы Р1 и Р2 пеановской системы обеспечивают существование О (нуля) и операции "непосредственно следующий", которым в теории S соответствуют предметная константа aj и функциональная буква / / . 125