ВУЗ:
Составители:
Рубрика:
Теорема 4. Во всякой эквациональной теории:
1) ` x
1
= y
1
∧ . . . ∧ x
n
= y
n
⇒ t(x
1
/z
1
, . . . , x
n
/z
n
) = t(y
1
/z
1
, . . . , y
n
/z
n
);
2) ` x
1
= y
1
∧ . . . ∧ x
n
= y
n
⇒
⇒ (A(x
1
/z
1
, . . . , x
n
/z
n
) ⇒ A(y
1
/z
1
, . . . , y
n
/z
n
));
где t — произвольный терм, A — произвольная формула, а переменные
x
i
, y
i
свободны для z
i
(1 6 i 6 n) в t(z
1
, . . . , z
n
) и A(z
1
, . . . , z
n
).
Утверждение 1) докажем в случае n = 1: x = y ⇒ t(x) = t(y),
где t(x) — это, конечно, t(x/z). В качестве A(z) в схеме аксиом E2)
возьмем формулу t(x) = t(z) и воспользуемся правилом перестановки
посылок, следствием 1(1) и правилом MP.
Утверждение 2) в случае n = 1 совпадает с E2), а при n = 2 имеет
вид: x
1
= y
1
∧ x
2
= y
2
⇒ A(x
1
, x
2
) ⇒ A(y
1
, y
2
) и выводится из двух
частных случаев схемы аксиом E2):
x
1
= y
1
⇒ (A(x
1
, x
2
) ⇒ A(y
1
, x
2
)),
x
2
= y
2
⇒ (A(y
1
, x
2
) ⇒ A(y
1
, y
2
))
путем применения правил
A
1
⇒ B
1
, A
2
⇒ B
2
` A
1
∧ A
2
⇒ B
1
∧ B
2
,
(A ⇒ B) ∧ (B ⇒ C) ` A ⇒ C
и транзитивности отношения выводимости.
Аналогично проводится доказательство для произвольного n.
Теорема 5. Если эквациональная теория имеет модель, то она
имеет и нормальную модель.
Пусть M — модель эквациональной теории, D — предметное мно-
жество, R — предикат, соответствующий символу «=» (т.е. R = | =
|
M
). Согласно следствию 2, R есть отношение эквивалентности на D,
поэтому можно определить фактор-множество D/R, состоящее из клас-
сов эквивалентности [α] (α ∈ D). Определим новую интерпретацию M
∗
с предметным множеством D/R и отображением оценки |·|
∗
, заданным
для любой константы a, любого функционального символа f, любого
предикатного символа P и символа «=» следующим образом:
1) | = |
∗
есть предикат тождественного равенства;
2) если |a| = α ∈ D, то |a|
∗
= [α];
3) если |f| = ϕ — функция из D
n
в D, то |f|
∗
= ϕ
∗
— функ-
ция, определенная на классах эквивалентности следующим образом:
ϕ
∗
([α
1
], . . . , [α
n
]) = [ϕ(α
1
, . . . , α
n
)]. Это определение не зависит от выбо-
ра представителей в классах, поскольку, согласно теореме 4(1), дока-
зуема формула
x
1
= y
1
∧ . . . ∧ x
n
= y
n
⇒ f(x
1
, . . . , x
n
) = f(y
1
, . . . , y
n
),
71
Страницы
- « первая
- ‹ предыдущая
- …
- 70
- 71
- 72
- 73
- 74
- …
- следующая ›
- последняя »