--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

04.15
Mon
こないだは命題論理の自然演繹について書いたので

今回は述語論理での自然演繹についてです

追加する推論規則は前回のに加え、量化子に関するものが四つあります

それぞれ

∀除去、∃導入、∀導入、∃除去です

ちなみに後ろのやつになればなるほどめんどいです


1.∀除去(∀除去)

∀ζ.Ψ という論理式があったら Ψ[α/ζ] にしていい規則です。

全ての物事についてなんちゃらと言ってるのだから任意の個体定項でも言えてるはずですよね。わかりやすいですね

例) ∀x(P(x)⊃Q(x)) |- P(a)⊃Q(a)


2.∃導入(∃intro)

Ψ[α / ζ] という論理式があったら ∃ζ.Ψにしていい規則です

例えばある個体定項がPという性質を持つって書いてあったら(P(a))、Pであるような何かが存在すると考えるわけです

例) P(a) |- ∃xP(x)


3.∀導入(∀intro)

Ψ[α / ζ] という論理式があったら、 ∀ζ.Ψにしていい規則です。

でもこのままだとどう考えてもおかしいです。限定的に言えてることがすべてについて言えるわけないですよね。

なので条件があります。

論理式 Ψ に現れる α は ∀introを使う以前の導出において仮定されていてはいけません。

仮定されていたとしたらキャンセルされていなければいけません。

例)

plogic_example1.png

定項のaは ∀elim で出てきたわけで仮定されてるわけじゃないので、この場合∀introが使えます

もちろん閉鎖タブローが生じます

tabro_example2.png


4.∃除去(∃elim)

(個人的にどのへんが除去なのかよくわかんないんですけど)

ちょっとむずいです. A∨B のときと同じように、AかBだ!とかなんかわかんないけど存在する!

とか言われてもそれ以上なにもわからないわけですなのでほかの式に頼るかんじです

具体的には、∃ζ.Ψ という式があった時に Ψ[α / ζ] を仮定してそこで論理式φが導かれたら、

そいつを上位導出にもってきていい規則です

但しαについて条件があって、まだキャンセルされてない有効なαを使うのはだめです

さらに、導かれる式φにαが入っていてはだめです。

いい感じの例が思いつかないので省略


ということで新しく追加された4つの規則をもとに述語論理の自然演繹をやってみます

ドモルガン的なやつ二つです

ded_demorgan1.png


ded_demorgan2.png

もし間違いがありましたら教えていただけると嬉しいです


で、話は変わりますが、なぜ論理学なのか。

コンピュータ系のカテゴリに登録しているこのブログでなぜ論理学なのかということですが

論理学が、数学とかコンピュータとすごいかかわりが深いからです

例えば最近話題の関数型言語は、ラムダ計算という計算モデルをもとに作られていますが

それが論理学と関連していたりします

論理学にもいろいろな分野がありますが、(命題論理、述語論理、直観主義論理、様相論理、ファジー論理...etc)

なかでも直観主義論理というのが、プログラム(ラムダ計算)に関連しているようです
(勉強してないので詳しくは言えませんが)

特に直にプログラミング言語に関連するものとしては一階述語論理に基ずくPrologとかの論理型言語があります

他にも人工知能の思考の部分を作るために使われる事もあります

もとは論理って人間が物事を考え推論し結論を出す過程を形式化したような学問ですしね
(ただ記号処理をもとに人工知能とかを実現しようという試みは少し古いのかもしれません)

ということで論理学について、まだまだ知らないことが多いので書いていけたらと思います
スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/169-ece9b3c9
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。