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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

Γ, A ` B (введ.⇒) A, A ⇒ B ` B (удал.⇒, или MP)
Γ ` A ⇒ B
A, B ` A ∧ B (введ.∧) A ∧ B ` A (удал.∧)
A ∧ B ` B
A ` A ∨ B (введ.∨) Γ, A ` C; (удал.∨, или
B ` A ∨ B Γ, B ` C разбор случаев)
Γ, A ∨ B ` C
Γ, A ` B; (введ.¬, или ¬¬A ` A (удал.¬¬)
Γ, A ` ¬B приведение
Γ ` ¬A к абсурду) A, ¬A ` B (удал.¬)
A ⇒ B, B ⇒ A ` A ⇔ B A ⇔ B ` A ⇒ B(удал.⇔)
(введ.⇔) A ⇔ B ` B ⇒ A
/ Введение ⇒ имеет место в силу теоремы дедукции. Удаление
⇒ выражает собой правило отделения. Введение ∧, ∨, ⇔ и удаление
∧, ¬¬, ⇔ непосредственно вытекают из аксиом и теоремы 3 § 5.
Докажем, например, введение ∧:
1. ` A ⇒ (B ⇒ A ∧ B) (аксиома 5).
2. A ` B ⇒ A ∧ B (теорема 3 § 5, 1).
3. A, B ` A ∧ B (теорема 3 § 5, 2).
Докажем введение ∨:
1. ` A ⇒ A ∨ B (аксиома 6).
2. A ` A ∨ B (теорема 3 § 5, 1).
Упражнение 2. Докажите введение ⇔ и удаление ∧, ¬¬, ⇔.
Докажем удаление ∨ (правило разбора случаев):
1. Γ, A ` C (гипотеза 1).
2. Γ, B ` C (гипотеза 2).
3. Γ ` A ⇒ C (введ.⇒, 1).
4. Γ ` B ⇒ C (введ.⇒, 2).
5. A ⇒ C, B ⇒ C, A ∨ B ` C (по аксиоме 8, см. ниже).
6. Γ, A ∨ B ` C (транзитивность, 3,4,5).
Вывод формулы 5 произведем отдельно:
1
Названия правил поясняются следующим. Введение связки означает, что она
появляется в заключении секвенции; удаление — связка присутствовала в одной из
гипотез, но пропала в заключении.
45

Страницы