Language:
[ つぎ | うえ | まえ ]

論理式

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

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

などである．これらを考慮して，論理式を定義してみよう．

論理式は，変数(正確には，命題変数という)，論理記号および，括弧 (，) から成り立つ．論理記号は，￢，⊃ のみである (他の論理記号は，これらの論理記号を使って表すことができる)． また，この制限にかなった論理式を 素論理式 という． 素論理式の集合をよく P で表す．

そのため，以下では変数(命題変数)を p,q,r など小文字で表す．

これをより簡単に表すと， 

  P ::= ￢P
    ||  P ⊃ P
    ||  ( P )

となる．このように，文法を表すことを BNF 形式 という．

わかりやすい方のみを覚えればよい．また，よく論理式を総称して， α，β で表す．例えば，p ⊃ q を α で，Q を βで表して，α ∪ β と書いたりする．そのため，α，βを メタ変数 という．

これだけの定義である．この論理式に，真「T」，偽「F」などの， 値を使って，説明したり，P に「太郎」とか，q を割り当てて， 説明するとき，その割り当てを，解釈 という． ここで，重要なのは，このような解釈を与えなくても， 絶対的に論理式は決まった形があり，それらを，無味乾燥した形 で表現していることである．例えば，何が真「T」とか，偽「F」とか 与えなくても，p ⊃ ￢￢p，p ⊃ p は，絶対的に成り立つとすることができる．

以上のような，考察から，コンピュータで論理式を処理するとき， いちいち，真「T」，偽「F」とか，値を代入したりして，いわゆる「解釈」 を与えなくても，無味乾燥した式の変形で，結果として，トートロジーを チャックすることができる．

実は，元となるトートロジーを使って変形を行い，論理式がトートロジー であるかどうかをチェックすることができる．この元となるトートロジー を，絶対的，普遍的な論理式という意味で公理 といい，その「公理」 を使って，変形することを推論 という．さらに，ある論理式が， トートロジーかどうかをチェックすることを，証明という． 我々が，よく使う，証明というのは，ほとんどを論理式で表現することが でき，ここでいう，推論を行って，トートロジーかどうか，「正しい」かどうか， をチェックする処理と同じである．人間は，無意識のうちに， コンピュータと同じ推論を行っている．

公理

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

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

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

モーダス・ポーネンス

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

証明，帰結，定理

論理式の集合 G を，公理か，

Copyright © 2000-2013 Hosei University.
Last update: Thu Aug 15 16:27:08 PDT 2013 by yasu@i.hosei.ac.jp