Математическая логика и теория алгоритмов

51 JC| = J:2=>((JCI = JC3); 52; xi= JC2=?> xi'= X2'; S3: 0 5^Х|'; 54.- Xi'=X2'=>JC|= X2-, 55; л:1+0= S6: xi+X2'=(j^i+X2)'; S I : xi-0=0; SS: ХГx2'=xrX2+xi; S9: A{Q):^(VxiiA{x,)^A{xi • ) ) ^ \ / х4{хд), где A {Xi) - произвольная формула теории S. Напомним, что правилами вывода любой теории первого поряд­ ка являются правила MP и Gen. Рассмотрим собственные аксиомы теории S и сравним их с ак­ сиомами Пеано. Заметим, что аксиомы 51 - 58 являются конкретными формула­ ми, в то время как 59 представляет собой схему аксиом, порождаю­ щую бесконечное множество аксиом. Аксиомы 51 и 52 обеспечивают некоторые необходимые свой­ ства равенства, которые Дедекиндом и Пеано предполагались как ин­ туитивно очевидные. Аксиомы 53 и 54 соответствуют аксиомам РЗ и Р4 системы аксиом Пеано. Аксиомы Р1 и Р2 пеановской системы обеспечивают существование О (нуля) и операции "непосредственно следующий", которым в теории 5 соответствуют предметная константа й] и функ­ циональная буква / I . Аксиомы 55- 5 8 служат для определения операций сложения и умножения. В аксиоматике Пеано нет аксиом, соответствующих 55 - 58, потому что Дедекинд и Пеано допускали использование интуи­ тивной теории множеств, в рамках которой существование операций + и • (сложения и умножения), удовлетворяющих аксиомам 55 - S8, выводимо. 172