Элементы математической логики. Фролов И.С. - 71 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

Формальная теория первого порядка называется эквациональной
теорией (или теорией с равенством), если в ней присутствует специ-
альный функциональный символ = и следующие специальные схемы
аксиом:
E1) x = x (рефлексивность равенства);
E2) x = y ⇒ (A(x/z) ⇒ A(y/z)) (подстановочность равенства).
В аксиоме E2) под A(z) понимается произвольная формула, выразимая
над заданным алфавитом; переменные x и y свободны для z в A(z). Вы-
ражения A(x/z), A(y/z), напомним, обозначают результат подстановки
в A(z) переменной x и, соответственно, y вместо z.
Теорема 3. Во всякой эквациональной теории:
1) ` ∀x(x = x);
2) ` ∀x∀y(x = y ⇒ y = x);
3) ` ∀x∀y∀z(x = y ∧ y = z ⇒ x = z).
Утверждение 1) получается из E1) по правилу обобщения.
Для доказательства 2) возьмем в качестве A(z) формулу z = x.
Тогда из E2) получим x = y ⇒ (x = x ⇒ y = x). Легко доказываемое
правило перестановки посылок A ⇒ (B ⇒ C) ` B ⇒ (A ⇒ C)
приводит к x = x ⇒ (x = y ⇒ y = x). Остается применить аксиому
E1) и правила MP и Gen.
Для доказательства 3) возьмем в качестве A(z) формулу v = z.
Из E2) получим x = y ⇒ (v = x ⇒ v = y). Пользуясь легко доказыва-
емым правилом объединения посылок A ⇒ (B ⇒ C) ` B ∧A ⇒ C, по-
лучим v = x∧x = y ⇒ v = y. Остается теперь применить правило Gen и
правило переименования связанных переменных ∀xA(x) ` ∀yA(y) (ср.
пример 1).
Следствие 1. Во всякой эквациональной теории для любых тер-
мов t, t
1
, t
2
:
1) ` (t = t);
2) ` (t = t
1
⇒ t
1
= t);
3) ` (t = t
1
∧ t
1
= t
2
⇒ t = t
2
).
Следствие 2. Во всякой модели эквациональной теории преди-
кат, соответствующий символу =, есть отношение эквивалентности.
Если в модели эквациональной теории символу = соответству-
ет предикат тождественного равенства, то эта модель называется нор-
мальной.
70

Страницы