Исчисление с равенством

В данном исчислении вводится предикат =, а к аксиомам ИП добавляются аксиомы равенства.

E1.

E2.

Здесь Е1 является аксиомой, а Е2 – схемой аксиомы, где – произвольная формула, а – формула, полученная из заменой некоторых вхождений x на y.

Теорема 6.1. В любой теории с равенством:

1) |- для любого терма t;

2) |-;

3) |-.

Доказательство. 1) Данное утверждение непосредственно следует из аксиом 11’ и Е1, где .

Для свойств 2), 3) построим формальные выводы формул.

Нам понадобятся старые правила вывода (напоминаем)

3. Правило удаления посылки.

Если T,|- и T |-, то T |-.

4. Правило силлогизма.

Если T |-,..., T |-и |-, то T |-.

5. Правило введения импликации.

Если T,|-, то T |-.

6. Правило удаления импликации.

Если T |-, то T,|-.

Вывод формулы 2)

1. |-	Е2
2. |-	6 (1)
3. |-	Е1
4. |-	3 (2, 3) Т: x = y, U: x = x, V: y = x
5. |-	5 (4)

3)

1. |-	Е2
2. |-	1, где ,
3. |-	6 (2)
4. |-	Теорема 6.1
5. |-	4 (4, 3)
6. |-	5 (5)

Дата добавления: 2014-01-11