論理式の形式化

第2章 No.2 ／ コンピュータが扱える形にする

論理式自身をコンピュータで扱い、トートロジーかチェックしたり、さまざまな論理を証明するためには、論理式自身をもう少し正確に定義する必要がある。コンピュータの中で常に真理表を書くわけにもいかない。

真理表を書くことによりわかったのは：

• 論理式は変数や論理記号から成り立つ。
• 実は ⊃ などは別の論理記号を使って表現することができる。例えば p ⊃ q は ￢p ∪ q と同等。

論理式の定義

論理式は変数 (正確には、命題変数という)、論理記号、および括弧 ( と ) から成り立つ。論理記号は ￢, ⊃ のみとする (他の論理記号はこれらを使って表すことができる)。

変数 (命題変数) は p, q, r など小文字で表す。BNF 形式で書くと：

P ::= 命題変数
   |  ￢P
   |  P ⊃ P
   |  ( P )

これだけの定義である。この論理式に 真「T」、偽「F」などの値を割り当てるとき、その割り当てを 解釈 という。重要なのは、解釈を与えなくても論理式は決まった形があり、それらを無味乾燥した形で表現していることである。

公理

元となる論理式 (トートロジー) である公理を示そう。以下の 3 つの形をしている論理式である。

1. α ⊃ (β ⊃ α)
2. (α ⊃ (β ⊃ γ)) ⊃ ((α ⊃ β) ⊃ (α ⊃ γ))
3. (￢β ⊃ ￢α) ⊃ ((￢β ⊃ α) ⊃ β)

ここで α, β, γ は論理式を表している (メタ変数)。上の形をした論理式は無限にあることに注意。

モーダス・ポーネンス

論理式 α がトートロジーで、α ⊃ β がトートロジーであれば、β もトートロジーである。この処理を モーダス・ポーネンス という。

証明・帰結・定理

論理式の集合 G を、公理またはモーダス・ポーネンスで導かれる論理式と定義し、これに従って導出された論理式を 定理 という。我々が普段「証明」と呼んでいるものは、ほとんどが論理式で表現でき、ここでいう「推論」を行ってトートロジーかどうかをチェックする処理と同じである。