Работает над логикой - система Фитча

Question

Борясь с логикой и системой подбора,

Я пытаюсь, учитывая (p ⇒ ¬q) и (¬q ∧ p ⇒ r) и p, использовать систему Fitch для доказательства r.

Есть идеи, как мне поступить?

Answer 1

Вы также можете попробовать другие формальные системы проверки правописания, которые доступны как компьютерные контрольные проверки. Используя язык структурированных доказательств Изабель, вы можете написать свое доказательство так:

theory Scratch
imports Main
begin

notepad
begin
  assume 1: "p ⟶ ¬ q"
    and 2: "¬ q ∧ p ⟶ r"
    and 3: p
  have "¬ q" using 1 and 3 ..
  then have "¬ q ∧ p" using 3 ..
  with 2 have r ..
end

end

Answer 2

1. (p ⇒ ¬q)
2. (¬q ∧ p ⇒ r)
3. п
4. ¬q (1 3 Устранение последствий)
5. ¬q ^ p (2 4 А Введение)
6. r (2 5 Устранение последствий) ---> КОНЕЦ

Answer 3

В следующем доказательстве используется проверка естественного вычитания в стиле Flement от Klement. Объяснение правил доступно в forallx.

Первые три строки - это помещения. Строка 4 является результатом условного исключения (→E), строка 5 - введением соединения (∧I), а последняя строка - условным исключением.

---

Рекомендации

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

П.Д. Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикс и рецензия Аарона Томаса-Болдука, Ричарда Зака, forallx Калгари Ремикс: Введение в формальную логику, зима 2018. http://forallx.openlogicproject.org/