logic - ロジックの作業 - フィッチ システム

Question

ロジックやフィッチ系に苦戦し、

(p ⇒ ¬q) と (¬q ∧ p ⇒ r) と p が与えられたとき、r を証明するためにフィッチ システムを使用しようとしています。

どのように進めるべきかについてのアイデアはありますか？

Answer 1

1. (p ⇒ ¬q)
2. (¬q ∧ p ⇒ r)
3. p
4. ¬q (1 3 含意消去)
5. ¬q ^ p (2 4 And Introduction)
6. r (2 5 含意消去) ---> END

Answer 2

また、コンピューターで実装された証明チェッカーとして利用できる他の正式な証明システムを試すこともできます。Isabelleの構造化証明言語を使用すると、次のように証明を書くことができます。

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