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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

Теорема 2. Для любых формул A, B и любого множества фор-
мул Γ, если переменная y не является свободной в Γ и B, а терм t
свободен для x в A, то имеют место следующие правила вывода:
Γ ` A(y)
Γ ` ∀yA(y)
(введ.∀);
Γ ` ∀xA(x)
Γ ` A(t)
(удал.∀);
Γ ` A(t)
Γ ` ∃xA(x)
(введ.∃);
Γ, A(y) ` B
Γ, ∃yA(y) ` B
(удал.∃).
/ Докажем, для примера, правило удаления ∃:
1. Γ, A(y) ` B (исходная посылка).
2. Γ ` A(y) ⇒ B (теорема дедукции).
3. Γ ` ∀y(A(y) ⇒ B) (Gen, 2 — т.к. y не своб. в Γ).
4. ∀y(A(y) ⇒ B) ⇒ (∃yA(y) ⇒ B) (акс. Q4 — т.к. y не своб. в B).
5. Γ ` ∃yA(y) ⇒ B (MP, 3, 4).
6.
Γ
,
∃
yA
(
y
)
`
B
(теор.3, § 5).
.
Пример 2. Докажем ` ∃xA(x) ⇒ ¬∀x¬A(x):
1. A(x), ∀x¬A(x) ` A(x) (рефлексивность).
2. A(x), ∀x¬A(x) ` ∀x¬A(x) (рефлексивность).
3. A(x), ∀x¬A(x) ` ¬A(x) (удал.∀, 2).
4. A(x) ` ¬∀x¬A(x) (прив. к абсурду, 1, 3).
5. ∃xA(x) ` ¬∀x¬A(x) (удал.∃, 4).
2. Эквациональные теории
Ограниченное исчисление предикатов определяется так же, как
обычное исчисление предикатов, за исключением того, что ограничи-
вается его алфавит: требуется, чтобы множества предметных, функци-
ональных и предикатных символов были не более чем счетны (в част-
ности, конечны или пусты), но должен быть хотя бы один предикатный
символ.
Формальная теория (или исчисление) первого порядка представ-
ляет собой расширение ограниченного исчисления предикатов, при
котором к аксиомам исчисления предикатов (называемых логически-
ми аксиомами) добавляются специальные (или нелогические) аксио-
мы. Как правило, в формальной теории фиксируется ряд предметных,
функциональных и предикатных символов, называемых специальны-
ми. Моделью теории называется интерпретация множества ее формул,
в которой истинны все теоремы этой теории.
69

Страницы