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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

Теорема 3. Всякая общезначимая формула исчисления выска-
зываний доказуема.
Предположим, что |= A. Пусть L
1
, . . . , L
k
— атомы, входящие в
A. При любой интерпретации I имеем |A|
I
= 1; тогда A
0
= A и в
силу леммы 3 L
0
1
, . . . , L
0
k
` A. В качестве L
0
k
можно выбрать и L
k
, и
¬L
k
; следовательно, справедливо и L
0
1
, . . . , L
k
` A, и L
0
1
, . . . , ¬L
k
`
A. По правилу введения ⇒ отсюда следует L
0
1
, . . . , L
0
k −1
` L
k
⇒ A,
и L
0
1
, . . . , L
0
k −1
` ¬L
k
⇒ A, но в силу леммы 2 L
k
⇒ A, ¬L
k
⇒
A ` A; поэтому по свойству транзитивности L
0
1
, . . . , L
0
k −1
` A. Число
гипотез уменьшилось; повторение этого рассуждения последовательно
приводит к секвенциям L
0
1
, . . . , L
0
k −2
` A; . . .; L
0
1
` A; и, наконец, ` A.
Пример 2. Мы знаем, что |= A ∨ ¬A. Чтобы доказать формулу
A ∨ ¬A, будем исходить из атома A и секвенций A ` A ∨¬A и ¬A `
A ∨¬A, очевидно, верных по правилу введения ∨. Можно взять теперь
` A ⇒ A ∨ ¬A и ` ¬A ⇒ A ∨ ¬A (в данном случае это даже
аксиомы, получаемые из схем аксиом 6 и 7) и применить лемму 2, что
даст ` A ∨ ¬A.
Другой способ основан на применении правила приведения к аб-
сурду:
¬(A ∨ ¬A), A ` A ` A ∨ ¬A
¬(A ∨ ¬A), A ` ¬(A ∨ ¬A)
¾
¬(A ∨ ¬A) ` ¬A,
¬(A ∨ ¬A), ¬A ` ¬A ` A ∨ ¬A
¬(A ∨ ¬A), ¬A ` ¬(A ∨ ¬A)
¾
¬(A ∨ ¬A) ` ¬¬A.
Следовательно, ` ¬¬(A ∨ ¬A), и после удаления ¬¬ получим
` A ∨ ¬A.
49

Страницы