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

10.21
Mon
お久しぶりです.

ブログ始めて以来の長さで更新をサボってしまいました.ので今回はちょっと長め

さて今回も論理学をつくるを参考に演繹定理について書いてみようかと思います.

演繹定理はある公理系が持つ性質というか、"その公理系の中で証明することができる

定理"ではなく、こういうものをメタ定理といいますがその中でも非常に重要なものです.

今回はAPLという命題論理の公理系で演繹定理を証明してみたいと思います.


APLは以下の公理図式(Axiom Schema)を持つ





ここで注意するのは公理図式には任意の論理式を代入して良い点です

公理を構成するA,B,Cというメタ的な記号を原子論理式に読みかえれば

それもひとつの公理になりますし、またそこに任意の論理式を代入してもそれは公理になります

つまり、どのように論理式が記号によって繋がっているかという形のみが重要なのです.

そして推論規則としてModus Ponensを持ちます

演繹定理の証明は所謂、証明図の長さについての帰納法により行うので

公理系における証明や演繹の概念を明確に定義しておきます


定義(1)
の証明とは論理式の有限個の列, であり(但しとなりこれを特に定理という)
は以下の何れかの条件を満たす
(1)はAPLの公理である
(2)のMPにより推論された論理式である.
このときと表す

定義(2)
の演繹とは論理式の有限個の列, であり(但し)
は以下の何れかの条件を満たす
(1)はAPLの公理である
(2)を仮定の集合として
(3)のMPにより推論された論理式である.
このときと表す

例えばAPLでの証明をしてみます







とかなりキモい感じですがこんなになります.
ここで最後の がこの証明で定理となります.よって が言えます

さて演繹定理ですがどのようなものかと言いますと



という命題です

これを示すためにまずいくつかの補題というほどでも無いですが命題を示しておきます


(1)
噛み砕いて言えばAが定理ならそこに仮定を付け加えてもAは演繹できるというものですね

だから Aの証明となる有限個の論理式の列が存在するが何れの

も定義(2)の演繹の条件をみたす(なのだからわざわざ仮定を使う必要はないので)

ゆえに


(2)

かつ より

からへの演繹となる論理式の列

が存在する

それらを合わせた の列を考えると

から推論規則MPによりである.よって



さて演繹定理を証明します.

の証明

より からへの演繹となる論理式の列 が存在する

この時仮定の集合にAを加えれば、証明の列は

とかけるが、ここからMPによりCnとAからBとなる.よって


で逆の方は面倒


帰納法により証明を行いますが、方針としてはまず

より Bへの演繹となる論理式の列 が存在することが言えます.

で、任意のについての仮定のもとで であることを示します.

の時に となるからという事です.

これだけだと、なんかもやもやとしてどうしてそのような方針に至ったのかわからないので

私なりに考えてみました(こっから先は本当は書かないほうがいいのかもしれない)

例えば自然演繹には含意導入の際に仮定が落ちるという概念があります。

つまりAを仮定していてそこでなにかが導けたらとして仮定はキャンセルされます.

これと同じ様に考えて、ターンスタイルの左側には仮定を置いているので

仮定をなくすには、ターンスタイルの右辺、演繹される論理式に含意(ならば)で条件をつけてやらなきゃいけない

みたいな感じです.では証明します。


の証明

よりが存在する。方針にしたがって、を証明する.

1. の時

を証明の列に書けるのは
(1)APLの公理である
(2)である
(3)であるの
何れかの条件を満たしているはずである

(1)の時

は公理であるから である.よって補題1より

またAPLの公理A1よりである。

よって補題1より

これらと補題2を考えると


(2)の時

は仮定の要素であるから なぜなら演繹の定義の条件2を満たしているからです.

また APLの公理 A1 より であるから

よって(1)の場合と同じく


(3)の時

APLにおいて は定理である(上のAPLの証明の例で証明した)

であるのでよって

これで帰納法のベース部分が証明できました


2. として n未満のk に於いては を満たしていると仮定する(帰納法の仮定)

を証明の列に書けるのは
(1)APLの公理である
(2)である
(3)
(4)とのMPにより
何れかの条件を満たしているはずである


(1)~(3)の場合はi = 1の時と全く同様に証明できるので省略


(4)のとき

の2つの式からのMPによりが出てくる場合である

ここでがどんな形をした式であるかはわからないけど、

少なくともにMPを適用することでが出てくるのはわかっている.

つまりの形になっている以外ありえない(もしくはの場合)

帰納法の仮定より かつ であるので

となる.
(の形をしていると考えて置き換えた.またなのでそれも置き換えた)

この上記の式と、APLの公理A2の式

で補題2を考えると

さらに帰納法の仮定のもうひとつの式 と上記の式を使って

となります

よって①,②から



が言えます.

こんな感じです。グダグダクドクドと無駄が多いしちょっと端折ったところがありますが

お疲れ様でした
スポンサーサイト

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