後件否定:p→q, ¬q ⊨ ¬p は妥当か?

p → q が成り立ち q が偽なら p も偽です。p を真にするものは q も真にするからです。後件を否定すれば前件が否定されます。

妥当p→q, ¬q ⊨ ¬p

タブローのすべての枝が閉じるので、前提が真で結論が偽になる割り当ては存在しません。

証明(意味論的タブロー)

  1. 1: p→q前提
    1. 2: ¬q前提
      1. 3: ¬p結論の否定
        1. 4: q2 行目から
          1. 5: p3 行目から
            1. 6: p1 行目から

              枝が閉じました: 6 行目は 5 行目と矛盾します。

            2. 7: q1 行目から

              枝が閉じました: 7 行目は 4 行目と矛盾します。

閉じた枝

意味論的タブローの仕組み →

計算機で試す

ほかの証明例