ВУЗ:
Составители:
Рубрика:
I. Рассмотрим случай, когда A = ¬B. Так как B содержит на
одну связку меньше, чем A, по предположению индукции справедливо
L
0
1
, . . . , L
0
k
` B
0
. Проверим, что B
0
` A
0
. Возможны два варианта:
|B| = 0, тогда |A| = 1, B
0
= ¬B, A
0
= A = ¬B, и нужно прове-
рить ¬B ` ¬B;
|B| = 1, тогда |A| = 0, B
0
= B, A
0
= ¬A = ¬¬B, и нужно
проверить B ` ¬¬B.
Обе проверяемые секвенции верны; первая в силу рефлексивно-
сти, вторая — согласно лемме 1.
II. Для каждого из случаев A = (B ∧ C), A = ( B ∨ C), A =
= (B ⇒ C), A = (B ⇔ C) по предположению индукции справедливо
L
0
1
, . . . , L
0
k
` B
0
и L
0
1
, . . . , L
0
k
` C
0
(так как и B, и C содержат мень-
ше связок, чем A). Поэтому проверке подлежат следующие секвенции
1
(учитываем здесь различные значения B и C):
B C A = (B ∧ C) A = (B ∨ C) A = (B ⇒ C)
0 0 ¬B, ¬C ` ¬(B ∧ C) ¬B, ¬C ` ¬(B ∨ C) ¬B, ¬C ` B ⇒ C
0 1 ¬B, C ` ¬(B ∧C) ¬B, C ` B ∨C ¬B, C ` B ⇒ C
1 0 B, ¬C ` ¬(B ∧C) B, ¬C ` B ∨C B, ¬C ` ¬(B ⇒ C)
1 1 B, C ` B ∧C B, C ` B ∨C B, C ` B ⇒ C
Проверка каждой из 16 секвенций проводится с помощью свойств
выводимости и правил введения и удаления логических связок. Напри-
мер, докажем ¬B, ¬C ` ¬(B ∧ C):
¬B, ¬C, B ∧ C ` B ∧ C ` B
¬B, ¬C, B ∧ C ` ¬B
¾
¬B, ¬C ` ¬(B ∧ C).
Докажем еще ¬B, ¬C ` ¬(B ∨ C), пользуясь неоднократно правилом
приведения к абсурду и один раз правилом разбора случаев:
¬B, ¬C, B, B ∨ C ` B
¬B, ¬C, B, B ∨ C ` ¬B
¾
¬B, ¬C, B ` ¬(B ∨ C)
аналогично ¬B, ¬C, C ` ¬(B ∨ C)
,
добавим к ¬B, ¬C, B ∨ C ` ¬(B ∨ C)
секвенцию ¬B, ¬C, B ∨ C ` B ∨ C
¾
¬B, ¬C ` ¬(B ∨ C).
Проверка остальных секвенций не представляет сложностей.
Упражнение 3. Докажите все секвенции, выписанные в приведенной выше
таблице, а также секвенции, относящиеся к случаю A = (B ⇔ C).
1
А также 4 секвенции для A = (B ⇔ C), не уместившиеся в таблице.
48
Страницы
- « первая
- ‹ предыдущая
- …
- 47
- 48
- 49
- 50
- 51
- …
- следующая ›
- последняя »
