аксиомы Пеано натурального ряда и арифметики

определения

0 -- [натуральное] число
число x' [прямой] потомок числа x
число x [прямой] предок числа x'

аксиомы:

¬(x'=0) -- 0 не имеет предков и не является потомком;
¬((∃y)(y=x') → x=0 -- если число не имеет предков, то это число 0;
x=y → x'=y' -- у одного предка  один [прямой] потомок,
   иначе: x=z'∧y=z' → x=y;
x'=y' → x=y -- у одного потомка один [прямой] предок,
   иначе: z=x'∧z=y' → x=y;

(F(0)∧(∀x)(F(x)→F(x'))) → (∀x)(F(x)) -- аксиома индукции;

x=y → y=x -- симметричность равенства; 
x=y → (x=z → y=z) -- транзитивность равенства; 

арифметика

x+0 = x, x+y' = (x+y)' -- аксиомы суммы; 
x∙0 = 0, x∙y' = (x∙y)+x -- аксиомы умножения;