yandex rtb 1
ГоловнаЗворотній зв'язок
yande share

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

6.2 Формальная теория S

Теория первого порядка S имеет единственную предикатную букву А12 единственную предметную константу а, и три функциональные буквы f11(t), f22(t.s), f22(t,s) Чтобы не порывать с привычными нам по неформальной арифметике обозначениями, в дальнейшем будем обычно писать t=s вместо A12 (t,s), 0 вместо a1 и t', t+s, t-s соответственно вместо f11(t), f22(t.s), f22(t,s), где t и s - термы. Собственные аксиомы теории S есть:

(S1) x1=x2(x1=x3x2=x3);

(S2) x1=x2x1=x2;

(S3) 01)';

(S4) x1=x2x1=x2;

(S5) x1+0=x1;

(S6) x1+x2'=(x1+x2)';

(S7) x1. 0=0;

(S8) (x1.x2)(x1.x2)+x1;

(S9) A(0) (x(A(x) A(x'))  (x')), где А(х) - произвольная формула теории S.

Аксиомы (SI) - (S8) являются конкретными формулами, в то время как [S9), представляет собой схему аксиом, порождающую бесконечное множество аксиом. При этом схема аксиом (S9), которая называется принципом математической индукции, не соответствует полностью аксиоме (Т5) системы аксиом Пеано, поскольку в этой последней интуитивно чред полагаются континуум свойств натуральных чисел, а схема аксиом (S9) может иметь дело лишь со счетным множеством свойств, определяемых формулами теории S.                    

С   помощью   МР   из   схемы   аксиом   (S9)   можно   получить   следующее правило индукции: из A(0) и х(А(x) А(х')) выводится xA(х).

 Отметим, что интерпретация теории S, в которой

a) множество всех неотрицательных целых чисел служит областью,

b) целое число 0 интерпретирует символ 0,

c)       операция       взятия       последующего       (прибавление       единицы)

интерпретирует функцию ' (т.е. функциональную букву f11(t)),

d) обычные сложение и умножение интерпретируют + и •,

e) предикатная буква = интерпретируется отношением тождества, называется" стандартной моделью теории S.

 

38