- ベストアンサー
命題計算の形式的体系Ｈｐに関する質問
- 命題計算の形式的体系Ｈｐにおいて、無矛盾なのに￢AとAが同時に成立することはあり得ない
- 松本和夫著「数理論理学」には、命題計算の形式的体系Ｈｐに関する具体的な公理と推論規則が記載されている
- 質問者は松本和夫著「数理論理学」を勉強中であり、一部理解できない箇所がある
- karitunakisu
- お礼率100% (5/5)
- 数学・算数
- 回答数3
- ありがとう数3
- みんなの回答 （3）
- 専門家の回答
質問者が選んだベストアンサー
回答No2の者ですが、質問者さんの意図をきちんと汲み取れていない回答になってしまっていたように思います。 もう一度、簡単に説明させてください。 （これも、相変わらず意図が汲み取れていないものでしたら、本当に申し訳ないです。） まず、ざっくばらんに、￢Ａ⇒（Ａ⇒Ｂ）という論理式の意味を確認すると、￢Ａが正しく、Ａが正しいならばＢが正しい、という感じになります。 Ａも￢Ａも正しいと仮定すると矛盾が生じるから、何でも好きな結論Ｂを導くことが出来てしまう、という意味です。 この意味に従うと、Ａと￢Ａを仮定してＢを証明することが出来た、よって￢Ａ⇒（Ａ⇒Ｂ）は正しい命題だ、という形の推論はごく自然なものだといえます。 しかし、今考えている体系はＨｐです。Ｈｐは、仮定（公理）として使っていいものは３つの形をしたトートロジーだけであり、推論規則もトートロジーからはトートロジーしか推論されないＭＰしかありません。このことによって、Ｈｐは無矛盾性を保証しているのでした。 ところが、問題の証明では、いきなり仮定として公理でないもの、あまつさえ矛盾しているようなものを持ってきています。 これはＨｐにおける証明とはいいがたく（Ｈｐが保証する無矛盾性の理念にすら反しており）、よって、この解法は無意味なのではないか?というのが質問の意図だと思います。（正しいでしょうか?） ここで理解の鍵になるのはやはり演繹定理です。 まず、教科書の解答は、たしかにＨｐの証明を直接的に書いたものではありません。勝手にＨｐの公理以外の仮定を持ち出してきてますから。 ここで、いったんＨｐの公理を変更して、好きな論理式を仮定（公理）として使ってよいとした形式的体系Ｈｐ’を考えることにします。 Ｈｐ’はめちゃくちゃな体系です。 何を仮定してもよいのだから、結論も矛盾するような論理式でも何でも導けてしまいます。 しかし、演繹定理はすごいことを主張します。 Ｈｐ’で証明を書いたとき、使った仮定をＡ、でてきた結論をＢとします。 すると、実はＨｐではＡ⇒Ｂを証明することが出来る、というのです。 教科書の解答は、Ｈｐ’での証明を与えて、よって演繹定理よりＨｐの証明も存在するはずだ、と述べているのです。 ですから、￢Ａ⇒（Ａ⇒Ｂ）のＨｐでの直接的な証明を与えているわけではなく、演繹定理によって間接的に存在を示しているだけです。 しかし、Ｈｐでの証明が存在するはずなら、実際それを書いて欲しいというのが人情だと思います。 実は演繹定理の証明は、Ｈｐ’で与えられたＡを仮定してＢを導く証明を、ＨｐでのＡ⇒Ｂの証明に書き換える一般的な方法を与えています。 ですから、演繹定理の証明を参考にしながらじっくり考えれば、￢Ａ⇒（Ａ⇒Ｂ）のＨｐでの直接的な証明も具体的に書くことが出来ますよ。ただし、結果は非常に長ったらしくて、あまり何度も書きたいと思うようなものではないでしょう。 とくに、教科書を書く人にとっては、長い証明より、間接的でも演繹定理を使ったシンプルな証明のほうがずっと嬉しいわけです。 勉強するうえでのご参考になっていれば幸いです。
その他の回答 (2)
- kbjsh17
- ベストアンサー率75% (3/4)
形式的体系とは何なのかをもう少しきちんと理解する必要があります。 まず、「論理」「意味」「矛盾」等といったことを全て忘れて頭を空っぽにします。 つぎに、Ｈｐの公理に書かれている論理式を何か意味を持つ「論理式」ではなく、単なる（ある法則にしたがって並べられた）文字列、記号列だと思ってください。 さて、推論規則は、この文字列の変形規則を与えています。その意味は何も問われていないことが重要です。 つまり、形式的体系とは、与えられた記号列（公理）を、記号変形のルール（推論規則）にのっとって変形していくだけの体系に過ぎないわけです。（厳密には、証明図の概念をどう定義するかによってやや途中経過が異なりますが、このように考えるのが、もっとも自然で理解の助けになります。） ￢Ａ⇒（Ａ⇒Ｂ）がＨｐから証明されるというのは、公理を満たす記号列をルールに従って変形すると、￢Ａ⇒（Ａ⇒Ｂ）にたどり着くということを意味するだけです！ このように、形式的体系は意味を考えなくても論理推論が出来るようにするために開発されたものです。 しかし、実際に記号変形（証明図）をかかれたことがあるならわかると思いますが、この記号変形、すごく長くて大変ですよね? そこで、記号変形の法則を調べることによって、便利な判定法を準備しようと言うのが演繹定理です。 演繹定理が主張することは、 「出発となる公理をふやして、（たとえば）Ａ、Ｂという形の記号列もスタートとして認めよう。ここからスタートして変形していったけっか、Ｃと言う形の記号列にたどり着いたとしよう。すると、じつは、何も公理を変えないもともとのＨｐの体系で、初めの公理からスタートしてうまく記号変形をしていくとＡ⇒（Ｂ⇒Ｃ）にたどり着くことが出来る。」 というものです。 証明を読まれたらわかると思いますが、実際にＡを公理としてＨｐに付け足した体系で、例えば Ｘ１ ； Ｘ２ ； ・・・ ； Ｘｎ；Ｃ という記号変形の列が得られたとしたら、実はもともとのＨｐの体系で ・・・ ； Ａ⇒Ｘ１ ； ・・・ ； Ａ⇒Ｘ２ ； ・・・ ；Ａ⇒Ｘｎ ；・・・ ； A⇒Ｃ という、Ｈｐのもともとの公理のみからスタートして記号変形ルールにのっとった証明図を作ることが出来ます。 （実際に今の問題について、演繹定理を使わない証明をやってみてください。やり方は、演繹定理の証明を参考にすれば出来ます。） つまり、公理を増やすと言うのが、上の証明で言う「仮定」に相当することです。 ここで、何を「仮定」として使ってよいか悪いかなどは演繹定理の条件には何も入っていません。 「仮定」として我々は好きな文字列を選んでよいのです。 くどく書いているので、いいかげんわかってきたと思いますが、形式体系では、何をしていいか、何をしてはいけないかが厳密に決まっており、また、それらは論理式の意味とはなんの関係もなく定義されています！ 形式体系が、論理式の意味とどういう関係にあるか、は完全性定理によって初めて数学的に示されることです。 それまでは、（形式的体系を扱うときは）論理式の意味を不用意に考えるのは混乱のもとです。 仮定が矛盾しているかどうかなんて問われていないのです。 実際に、他にも様々な形式的体系がありますが、出発が奇妙きまわりないものだって作れます。 その形式的体系が、（見かけは奇妙かもしれないが）結果として数学者の証明結果を同様に導く力を持っていると言うことを主張するのが、後ほど出てくるであろう完全性定理です。 （完全性定理＝トートロジーは全て形式的体系で証明可能） ちなみに、形式的体系が変な結果を導かない（矛盾記号を導かない）ことを示すのが、健全性定理と呼ばれるものです。 （健全性定理＝形式的体系で証明された論理式は全てトートロジー） （なお、意味としての矛盾と形式的体系における矛盾は異なるものです！きちんと区別をつけながら読んでください。完全性定理などによって、そられが実は一致していることが示されます。） 健全性と完全性が両方示されたら、その形式的体系は、論理の「意味」を余すところなく表現していると考えることが出来ます。 長くなりましたが、￢AとAを仮定して証明することなどは、「自然演繹」と呼ばれる形式体系を勉強されると、その（意味の上での）正当性がわかりやすくなると思います。自然演繹では、「仮定」を「落とす」と言う作業（演繹定理の適用に対応する）があり、この結果、仮定は初めからなかったかのように扱われることになります。 意味としては、 Ａを仮定してＢが導かれた、これはすなわちＡ⇒Ｂが（仮定なしに）正しいということである というのが簡単な説明です。 しかし、繰り返しますが、形式的体系で意味を考えるのは禁物です。 以上です。がんばってください
お礼
丁寧なご回答ありがとうございます。仮定に制約はない、というご指摘は目から鱗でした。Ｈｐが健全な体系ならば、仮定がトートロジーでなくとも、演繹定理から導かれる論理式はトートロジーなのですね。ありがとうございました。
自分は、約100前の形式的数学の記述しか読んでいないので、用語が古めかしいのは許して下さい。 ある形式系における真な関係を、定理と呼ぶ事にします。上記の証明方法は、次の「場合分けの方法」の特別なケースだと思います。 ［場合分けの方法］ ＡouＢが定理，Ａ⇒ＣとＢ⇒Ｃも定理。この時、Ｃは定理。 （ouは「または」，⇒は「ならば」です） ～ＡouＡは常に定理なので（～は「否定」）、～Ａ⇒ＣとＡ⇒Ｃが成り立てば、Ｃは定理です。 （実際には、～Ａを仮定してＣを示し、Ａを仮定してＣを示し・・・、とやります） Ａが定理なら、～Ａ⇒Ａも成立はご存知と思います。じつはこれ、形式論理の本質のような気がします。つまりＡが真なら、前提Ｂに関わらずＢ⇒Ａは成り立つ。背理法も（対偶も）、矛盾の定義も、みなこの路線で示せそうな気がします（気がするだけで、やった事はありません^^）。
お礼
ご回答ありがとうございます。場合分けの方法ですか。確かに関係がありそうな気がします。でもやはり、何故無矛盾な体系内でＡと￢Ａとを共に仮定できるのか分かりません。証明の最後に使う演繹定理に何か鍵があるのでしょうか。
お礼
度々のご回答ありがとうございます。私の質問文が拙劣なために、お手を煩わせしまい申し訳ありません。とても明快なご説明で解りやすかったです。私が演繹定理の証明を十分に理解していなかったが為の疑問だったようですね。仰るように、演繹定理の証明の裡に「証明の書き換え」の方法が示されていました。またその方法で書き換えられた論理式が必ずトートロジーになる事も理解できたと思います。しかし演繹定理というのは凄い定理ですね。勉強になりました。ありがとうございました。