15.Формальная арифметика

Эгалитарные теории. Теория, содержащая исчисление предикатов, называется эгалитарной, если она имеет дополнительный двуместный предикат = (*,*), для которого выполняются две нелогические аксиомы:

1. для люб x(= (х,х));

2. = (х,у) => (А(...,х,...,у,...) =>А{...,у,...,у,...)).

Здесь А произвольная формула.

Вместо = (x, у) пишут х = у. Таким образом, эгалитарная теория - это просто теория с равенством.

2.4.2. Язык и правила вывода формальной арифметики

Формальная арифметика - это эгалитарное прикладное исчисление, в котором дополнительно имеются:

1. Предметная константа 0.

2. Двуместные операции + и * и одноместная операция `.

3. Знак равенства • = •.

4. Нелогические аксиомы равенства и некоторые нелогические аксиомы арифметики:

(t`1 = t`2) => (t1 = t2)

отриц. (t` = 0)

(t1 = t2) => ((t2 = t3) => (t1 = t3))

(t1 = t2) => (t`1 = t`2)

t +0 = t

(t1 + t`2) = (t1 + t2)`

t*0 = 0

где A - любая формула, а t,t1,t2 - любые термы.

Первая аксиома - это известный способ доказательства посредством математической индукции. Если вместо t` писать t + 1, то ясно, что t` - это следующее натуральное число, идущее за t. Другими словами, аксиомы арифметики определяют натуральные числа и правила оперирования с ними с помощью операций сложения и умножения.