Теория 1-ого порядка с равенством

Эта теория, в предположении, что среди предикатных символов есть символ «=», характеризуется двумя схемами нелогических аксиом:

(НЛ1) (аксиома рефлексивности равенства);

(НЛ2) , где предполагается, что формула

A<x, y> получена из формулы A<x, x> заменой некоторых (всех, в частности) свободных вхождений переменной x переменной y при условии, что терм y свободен для всех заменяемых вхождений x в формуле A, т.е. ни одно из заменяемых вхождений x не попадает в область действия квантора по y [5]. Эта аксиома называется аксиомой подстановочности равенства.

Исходя из этих аксиом, можно доказать следующие свойства равенства (формально: бинарного отношения, обозначенного значком «=»).

Теорема 4. 1) Для любого терма t ├ (t = t).

2) ├ (x = y) ® (y = x);

3) ├ (x = y) ® ((y = z) ® (x = z))[6].

Доказательство. 1) Из аксиомы (НЛ1) по правилу индивидуализации получаем для любого терма t , так как исходная формула не содержит никаких связанных вхождений переменных, ├ (t = t).

2) Положим, что формула A<x, x> есть (x = x), а A<x, y> есть (y = x). Тогда, согласно (НЛ2) имеем:

(x = y) ® ((x = x) ® (y = x)).

Пусть формула (x = y) есть гипотеза. Тогда, применяя MP, получим

((x = x) ® (y = x)). По правилу индивидуализации из аксиомы (НЛ1) при

t = x получим формулу (x = x). Откуда, еще раз применяя MP, получим

(y = x). Так как в построенном выводе правило Gen нигде не использовалось, применив теорему дедукции, получим требуемую формулу[7].

3) Полагая, что A<y, y> есть (y = z), а A<y, x> есть (x = z), построим вывод:

1. (y=x) ® ((y=z) ® (x=z)) – аксиома (НЛ2);

2. (x=y) – гипотеза;

3. (x = y) ® (y = x) – п. (2) настоящей теоремы;

4. (y = x) – MP, шаги (2) и (3);

5. ((y=z) ® (x=z)) – MP, шаги (1) и (4).

Итак, мы доказали секвенцию (x=y) ├ ((y=z) ® (x=z)), откуда по теореме дедукции получим требуемое.

Теорема 5. при условии, что термы и свободны для переменной в формуле .

Доказательство.

1. - НЛ2;

2. - Gen, (1);

3, - Gen, (2);

4. - теорема;

5. - MP, (3) и (4);

6. - теорема;

7. - MP, (5) и (6).

Следствие. , где - терм, содержащий терм в качестве подтерма.

Доказательство.

1. - НЛ2; (множества переменных термов s и t не содержат x и y);

2. - дважды Gen;

3. - переход к частному случаю вместе с MP;

4. - равенство терма себе самому;

5. - секвенция (2) ИВ к шагам (3) и (4);

Но .

Приложение. Интерпретации и состояния.

При заданной интерпретации = состояние – это частичное отображение множества переменных в область интерпретации. Попросту, это присваивание значений некоторым переменным. Состояние может быть определено только, если задана интерпретация.

Значение терма в состоянии определяется следующим образом.

Если , то, то (значение переменной); если , то (значение константы); если для некоторого и некоторых термов , то .

Истинностное значение формулы в состоянии определяется аналогично понятию истинностного значения формулы в интерпретации на последовательности .

Удобно ввести такое отношение на множестве состояний: означает, что для каждой переменной выполняется , т.е. состояние отличается от состояния , может быть, только значением переменной . Если (переменная с номером ), то будем писать вместо .

В этих обозначениях тогда и только тогда, когда для каждого состояния имеет место .

Выполнимость формулы в интерпретации означает, что для некоторого состояния имеет место ; истинность формулы в интерпретации означает, что для каждого состояния имеет место .

[1] Вариант изложения нижеследующих понятий через определение состояния см. в Приложении.

[2] Аналогично, для нескольких переменных используем обозначение .

[3] В противном случае подстановка терма приведет к появлению связанных вхождений переменных, отличных от , и тогда для истинности новой формулы требуется, чтобы формула была истинна на некоторой последовательности, отличной от более, чем в одном -ом члене.

[4] Например, для области интерпретации, совпадающей с множеством целых чисел, и при сопоставлении предикатному символу предиката «быть четным».

[5] Если это справедливо для всех свободных вхождений x в A, то терм y будет свободен для переменной x в формуле A.

[6] Содержательно: первое свойство состоит в том, что всякий терм равен самому себе, а второе и третье свойства называются соответственно симметричностью и транзитивностью равенства.

[7] Подробная запись этого вывода:

1. (x=y) ® ((x=x) ® (y=x)) – НЛ2; 2. (x=y) – гипотеза; 3. (x=x) ®(y=x) – MP, (1) и (2); 4. ("x)(x=x) – НЛ1; 5. ("x)(x=x) ® (x=x) – правило инд. при t=x; 6. (x=x) – MP, (4) и (5); 7. (y=x) – MP, (3) и (6).