シークエントを活用した反例モデルの抽出

今回はものすごーくマニアックですが感じたことなのでまとめておこうと思います。論理学についてです。高校数学では"集合論"の分野で"命題と証明"があると思いますが，特に証明の分野で"反例"という言葉が教えられるはずです。ある命題に対して反例が存在するとは，その命題を偽にする要素があり，その要素を含めたものを反例モデルといいます。少し曖昧ですが本来は帰納的に定義されています。

反例モデルの抽出法

・真理表　単純に起こりうるすべての可能性を書き出す方法。反例を直観的に認識できるが手間がかかりやすい。
・タブロー　規則の適用により論理式を分解する方法。反例モデルだけを算出できるが，規則の順序が異なると答えの出方が変わる。
・証明図　結論を真と仮定して前提を偽とした後に真理値を反転させる方法。証明図にそのまま落とし込めるが，論理式に前提を持たせる必要がある。

他には意味木とか証明探索体系を使う方法があります。

e.g. A→B

LaTeXだと結構大変なので手書きですがすみません。

それぞれから反例モデルは得られるはずです。真理表の場合はA→Bの値が0のときのAとBの値が反例モデルです。計算方法は|A→B|=max(1-|A|,|B|)です。タブローの場合は¬AとBがともに偽となる場合にそれが反例となります。A→Bは同値変形すると¬A∨Bになります。自然演繹とシークエントの場合はAからBが直接的には証明されないことが明らかです。

このようにして反例モデルが得られます。

シークエントの活用

前述したシークエントでの抽出法は証明を得るための前提が必須でしたが，前提がない論理式の反例モデルを得る方法もあります。

e.g. A∨B，A∧B

このように連言と選言の規則さえ決めてしまえば反例モデルが得られることがわかります。ターンスタイル記号のAやBがそれぞれ偽の場合それが反例モデルとなります。A∧BとA∨Bの計算方法はそれぞれ|A∧B|=min(|A|,|B|)と|A∨B|=max(|A|,|B|)です。もしターンスタイル記号の後件に矛盾(例えばpと¬p)がある場合それを消去していきます。最後まで残らなかった場合はその論理式が恒真式(トートロジー)であることを表しています。

論理和標準形

¬，∧，∨以外の論理記号を含む論理式の反例モデルを得るためには同値変形が必要です。A→B≡¬A∨Bを定義すればおおよその論理式は同値変形できます。そして，同値変形が完了した論理式は∨(論理和)でつながれているので論理和標準形と言われています。同様に反例モデルを抽出することが可能になります。

---

反例モデルを得るにはシークエントを活用した方法が最適だと私は思います。やはり規則が2通りしかないということが私には合います。簡単だからですけどね...

今回は古典命題論理を前提とした話題なので，抵抗のある方は直観主義論理や最小論理でも似たような方法が使えます。また次の機会に紹介します。