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

03.12
Tue
自然演繹ってのがあります。

ある論理式から論理式が論理的に帰結するかどうかは

タブローとか真理値表書けばわかります

つまり、前提となる論理式を一斉に1にする時に導かれる論理式も1になるとか(反例がない)

閉鎖タブローが生じるとかです

これらの方法で調べることができるんですが

このように論理式の真偽値を気にして論理的帰結である事を確認するのを

意味論的帰結(Γ|=ψ)とかいいます

論理学ではよくこの意味論的にとか統語論的にとかいう考えをよく使います

誤解を恐れずざっくり簡単に言ってしまうなら

意味論的にってのは、論理式に真偽値を与えてみて考えるのに対し

統語論的(シンタックス)にってのはその論理式の形自体がどうなってるのかを考えたりします

ある公理系のもとでなんかを示す場合はこのシンタックス的な方にあるのですが

公理系にもいろいろあります

フレーゲの公理系とかAPLとかメレディスの公理系とか

これらの何らかの公理(出発点となる論理式)をおくものとか

自然演繹みたいに公理をおかない推論規則だけのものもあります

今回はこの自然演繹を使います

自然演繹でもいろいろゲンツェンのNKとかありますが[要出典]

フィッチスタイルと呼ばれるやつでやってみます

以下が推論規則です


1. →の導入規則 →intro
2. →の除去規則 →elim
3. ∧の導入規則 ∧intro
4. ∧の除去規則 ∧elim
5. ∨の導入規則 ∨intro
6. ∨の除去規則 ∨elim
7. ↔の導入規則  ↔intro
8. ↔の除去規則  ↔elim
9. ¬の導入規則 ¬intro
10. ¬の除去規則 ¬elim


1. なんか仮定して論理式がでたら仮定→論理式を上位導出に書いていい規則。

2. MP(モーダスポネンス)をつかう。つまり A → BとAからBにしていい規則

3. 同じ導出の過程にAとBが表れてたらA∧Bにしていい規則

4. A∧BからA若しくはBを導いていい規則

5. AもしくはBのどちらかさえみちびけてればA∨Bとしていい規則

6. A∨BがあってA→ψとB→ψがあるならψとしていい規則

7. A→BとB→AがあるならA↔Bを書いていい規則

8. A↔BのときAからB若しくはBからAを導いていい規則

9. Aと仮定して矛盾したら¬Aを上位導出に書いていい規則

10. 二重否定¬¬AをAにしていい規則


あと論理式自体に関する規則ではないですが

仮定を書くとこに仮定する論理式をかいてもいい規則(Prem)

上位導出で使った論理式を下位導出にもってきていい規則(Reit)

仮定を繰り返して書いていい規則(Rep)

があります



natded.png


今回は古典命題論理に限って早速やってみましょう


まず簡単なやつから

P→QとQ→RからP→Rを示します


natded1.png

P→Qから¬Q→¬P

natded2.png

パースの法則

((P→Q)→P)→P

natded3.png

(あってるよな...?)

トートロジーは仮定もクソもないですね

こういう前もって必要になる前提の式がなく導かれるのを定理といいます


述語論理もできんですがそれはまた後に


論理学をつくるを参考にしました
スポンサーサイト

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