Докажите A ∨ D из A ∨ (B ∧ C) и (¬ B ∨ ¬ C) ∨ D (LPL Q6.26), не используя --> или материальную импликацию.

|  1) A ∨ (B ∧ C) --- premise
|_ 2) (¬ B ∨ ¬ C) ∨ D --- premise
|  |_ 3) A --- assumed [a] from 1) for ∨-elim
|  |  4) A ∨ D --- from 3) by ∨-intro
|  /
|  |_ 5) (B ∧ C) --- assumed [b] [from 1) for ∨-elim
|  |  |_ 6) D --- assumed [c] from 2) for ∨-elim
|  |  |  7) A ∨ D --- from 6) by ∨-intro
|  |  /
|  |  |_ 8) (¬ B ∨ ¬ C) --- assumed [d] from 2) for ∨-elim
|  |  |  9) B --- from 5) by ∧-elim
|  |  | 10) C --- from 5) by ∧-elim

Теперь, используя третий ∨-elim, мы получаем ⊥ (противоречие) как из 8), 9), так и из 8), 10); таким образом :

|  |  | 11) ⊥ --- from 8) by ∨-elim
|  |  | 12) A ∨ D --- from 11) by ⊥-elim

Получив A ∨ D как из 6) D, так и из 8) (¬ B ∨ ¬ C), мы имеем:

|  | 13)  A ∨ D --- from 2) by ∨-elim discharging assumptions [c] and [d]

Получив A ∨ D как из 3) A, так и из 5) (B ∧ C), мы имеем:

| >14)  A ∨ D --- from 1) by ∨-elim discharging assumptions [a] and [b].

Вывод :

A ∨ (B ∧ C), (¬ B ∨ ¬ C) ∨ D ⊢ A ∨ D --- из 1), 2) и 14).

Доказательство будет большим v-выбором на A v (B ^ C). Однако вы могли бы легко выполнить v-elim на (~B v ~C) v D. Я пытался привести обозначения в соответствие с тем, что есть в учебнике, хотя признаю, что они довольно отвратительны. Возможно, стоит скопировать его вручную, чтобы вы могли увидеть, как работает область видимости для подкорректировок.

 1. |A v (B ^ C)         Premise
 2. |(~B v ~C) v D       Premise
    ---------------
 3. ||A                  Assumption for v-elim
    ---------------
 4. ||A v D              3, v-intro
    |
 5. ||B ^ C              Assumption
    ---------------
 6. ||B                  5, ^-elim
 7. ||C                  6, ^-elim
 8. |||D                 Assumtion
    ---------------
 9. |||A v D             8, v-intro
    ||
10. |||~B v ~C           Assumption
    ---------------
11. ||||~B               Assumption
    ---------------
12. ||||| ~D             Assumption (for reductio)
    ---------------
13. ||||| falsum         falsum-intro, 6, 11
14. ||||~~D              ~-intro, 12 - 13
15. |||| D               ~-elim, 14
16. ||||~C               Assumption
    --------------
17. |||||~D              Assumption (for reductio)
    --------------
18. ||||| falsum         falsum-intro, 7, 16
19. ||||~~D              ~-intro, 17-18
20. |||| D               ~-elim, 19
21. |||D                 v-elim, 10, 11-15, 16-20
22. |||A v D             v-intro, 21
23. || A v D             v-elim, 2, 8-9, 10-22
24. |A v D               v-elim, 1, 3-4, 5 - 23

Это доказательство похоже на то, что предоставлено PossibleWorld , за исключением того, что оно начинается со второй предпосылки, а не с первой, и иллюстрируется другим средством проверки доказательств в стиле Fitch.

Доказательство использует введение дизъюнкции (∨I), устранение конъюнкции (∧E), введение противоречия (⊥I), взрыв (X) и устранение конъюнкции (∨E). Для получения подробной информации об этих правилах см. Forall x: Calgary Remix .

Использование взрыва может сделать это не ответом, но ОП говорит, что разрешено «Противоречие intro, elim». Из-за этого я предполагаю, что взрыв также разрешен. Если нет, это дает еще одну иллюстрацию того, как можно поступить с добавлением правила взрыва.

использованная литература

Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/

PD Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикшированный и отредактированный Аароном Томасом-Болдуком, Ричардом Заком, forallx Calgary Remix: An Introduction to Formal Logic, зима 2018 г. http://forallx.openlogicproject.org/