ブログ「サイバー少年」

ブログ「サイバー少年」へようこそ!
小学六年生ごろからプログラミングを趣味にしている高校生のブログです。
勉強したことについての記事などを書いています。フリーソフトも制作、公開しています。
(当ブログについて詳しくは「ブログ概要紹介」を参照)

サイバー少年が作ったフリーソフトは「サイバー少年の作品展示場」へ

形式論理と自然演繹の紹介

論理学の勉強で自然演繹を学んだので、とうとうご紹介したいと思います。

論理学といえば自然演繹、自然演繹といえば論理学ですね。
いや、そんなにでもないか…。


自然演繹を紹介するとは言っても正直なところ、健全性や完全性の証明とかそんな深入りして紹介するのは大規模過ぎて難しいので、
さらっと規則を紹介したり、具体例を示したり、で済まそうと思いますが。

あと、述語論理での扱いも入れたかったのですが、面倒なのと、固有変数条件あたり熱弁して空回りするクソ解説を生産しそうなので、命題論理にとどめておきました。


自然演繹は論理学の形式的証明の方法のひとつで、自然演繹の他には、
ヒルベルト式と呼ばれる矢印だらけの気色の悪い、仕組みは単純だけど使うのが難しいものとか、

シークエント計算という、これはまだ勉強中なのでコメントしづらいんですが、シークエントというものに対してゴニョゴニョしていくものなどがあります。

ちなみに、自然演繹とシークエント計算は、同じゲンツェンという人が発明したそうです。


さて、今回の記事は前編と後編ではなく、ひとつの記事で完結しますが、執筆には2日間かけています。





形式的証明の基本


そもそも自然演繹などの形式的証明はどのように進めるのかというとですが、

まず、形式的証明ではない意味論的な証明の場合、論理式に対して解釈を行った上で証明を行います。


つまり、φ = a∧(a→b)という論理式が、ある解釈MにおいてM[φ] = Tとなるときには、一般にx∧yがTとなるのはxもyもTのときだから、M[a] = T、M[a→b] = T、
aがTのときにa→bがTになるのは、bもTのときだからM[b] = T、よってφが真ならbも真、というような証明の方法となります。

このように、意味論的な証明は自由すぎて、自由で大変よろしいじゃないかと言いたいところなのですが、
「証明」という作業を数学的に考察したいときに、こんな特にルールのない証明では考察しづらい、もっと証明というものを定型化したいという要請が起こるだろうと、いうわけです。


さらには、命題を証明するときに、わざわざモデルを考えて前提の命題がTなら帰結もT…なんて考え方をする人はあんまりいません。

モデルなんて別に考えずに、a∧(a→b)ならaかつa→bであって、a→bに対してaだから、帰結としてbである、みたいな証明を行うのが普通で、
これは論理式を日本語的に解釈して行う証明だと考えられます。


ただし形式的証明は別に論理式を日本語的に解釈して行う証明ではないのですが、

日本語的に解釈する証明というのは、パターンによる証明となる側面があるのではないかと、私は今適当に思いました。

xxxのときyyyであって、xxxであるなら、yyyだ、みたいな証明は、少なくともモデルという考えは無くなっているし、
さらに、これは日本語の意味を持ち込むのではなくて、日本語の言葉の並びによるパターン処理なのだと思うことも可能ですね。

最初のほうは日本語の意味を考えるでしょうが、慣れてくると音とか文字の流れで「xxxならyyy」みたいな推論を行うようになると思います。


ようするに、何が言いたいのかというと、普段やる証明というのは、意味を考えているというより、パターン処理を行っていることに近いということです。


そこで、これの日本語ではなく論理式を使ったバージョンにおいて、パターン処理を原則とする証明の方法が、形式的証明です。

つまり、まず「a∧bならa、b」、「a→b、aならb」みたいなパターンをいくつか作っておいて、
a∧(a→b)ならa、(a→b)そしてbみたいなパターン適用の繰り返しを行います。

ここでa∧bがaかつbなんだ、とかa→bがaならばbなんだ、などの意味解釈は一切ありません。

ただ単にa∧bという文字の並びがあればa、bであるとか、a→bとaならbであるとしているだけです。


なお、注意しなければならないのは、パターンを適用するとき、一部に適用するということはできないということです。

つまり、a→(b∧c)という論理式の(b∧c)というところだけを取り上げてb、cであるみたいにすることはできません。

パターンは論理式全体に対して適用するものです。
そうしないと正しい証明にならないからです。


上のようなパターン処理が正しいのかどうかを考えるときには意味論を使います。

a、a→bならbというパターンが正しいことは、任意のモデルでM[a] = T、M[a→b] = TのときM[b] = Tなので示せるわけです。


つまり、解釈したら真である論理式に、正しいパターンを適用して出てきた論理式は、同じ解釈において真です。

このようなパターンの性質を妥当であると呼びます。

あと、パターンを、一般的には推論規則と呼びます。
(以後、推論規則という呼称を用います。)




前提、公理、帰結、定理


妥当な推論規則とは、適用する前の論理式を解釈したら真であるとき、適用後の論理式も同じ解釈において真であるというものでした。

推論規則を適用した後の論理式に、さらに推論規則を適用しても、最初の論理式が真なら真となります。


つまり、まず最初に証明なしに真とするいくつかの命題の集合を前提としておけば、
その命題ズを元として推論規則を適用して出てきた命題は、前提が真である場合に真となります。

この出てきた命題を帰結と呼びますが、あらゆるそれを帰結と呼ぶというよりか、特別関心の対象となるようなそれだけを帰結と呼ぶのが普通です。

帰結を出すことを証明と呼びますが、普通はゴールとなる出したい命題が先にあって、前提からそれを出すことを証明と呼びます。


また、このように、命題の集合Γから、いくつか推論規則を適用してφという命題を出せるときに

Γ ⊦ φと書きます。


記事「命題論理の意味論まとめ (前編)」で登場したのは
Γ ⊧ φという、横棒が二本のものです。

こちらは、意味論的にΓの命題がすべて解釈したら真であるとき、同じ解釈においてφは真となるというものでした。


今回の横棒が一本のΓ ⊦ φは、命題の集合に推論規則を適用してφを出せるという形式的証明のものであることに注意してください。


さらに、前提の集合が空なのに出てくる帰結があります。
⊦ φと書くことができます。

これは、前提がないのにどのように推論規則を適用するのかというところですが、
公理というものがあって、それに推論規則を適用します。

(なお、今回紹介する自然演繹には、仮定という種類の命題もあって、これに推論規則を適用して命題を出すこともあります。)


公理は前提と関係なく存在するので、いつでも使えます。

公理というのは、こちらも証明なしに正しいとする命題のことで、何を公理とするのかは、何を推論規則とするのかということとセットで与えられます。

前提はコロコロ変わりますが、公理は固定的に存在しています。

この公理と推論規則のセットを形式体系と呼びます。
(実際は、論理式がどのように構成されるかというものも含むようで。)


このように、ある形式体系において、前提なしに証明できるもの、
つまり⊦φとなるφを定理と呼びます。




自然演繹

いよいよ自然演繹とはどのような推論規則と公理で成り立つものか紹介します。

しかし実は、自然演繹という形式体系があるわけではなく、NKという形式体系とNJという形式体系があって、これらを自然演繹と総称しています。

NKとNJの違いはほんの僅かなものなので、ここではNKを軸に解説します。


・NKの公理

排中律: φ∨¬φ


この1つだけです。

厳密にいうと、φがあらゆる式であっても成り立つということですので、あらゆる場合において無限に同じような公理があるということかもしれないですが、厳密にどうなっているのかは知らないです。

でも結局はすべてφ∨¬φというパターンになるということですね。


・NKの推論規則

連言導入: φ, ψ ⊦ φ∧ψ
連言除去: φ∧ψ ⊦ φ および φ∧ψ ⊦ ψ
選言導入: φ ⊦ φ∨ψ および ψ ⊦ φ∨ψ
選言除去: φ∨ψ, [φ]...χ, [ψ]...χ ⊦ χ
仮言導入: [φ]...ψ ⊦ φ→ψ
仮言除去: φ, φ→ψ ⊦ ψ
否定導入: [φ]...⊥ ⊦ ¬φ
否定除去: φ, ¬φ ⊦ ⊥
矛盾: ⊥ ⊦ φ


この9つの推論規則となります。

⊦はこれの左にある論理式(複数ある場合はコンマで区切っている)から右にある論理式を出す推論規則であるという意味で、

さっき解説した⊦の使い方とは若干違うと思うんですが、意味が似てるので使いました。
本来の⊦の意味はさっき解説したものですので、ご注意ください。


⊥は、解釈すればFですが、ここではφ, ¬φから否定導入により生まれた矛盾状態を示しますね。

矛盾している状態というのはありえないので、ありえないということを利用して、ありえないような論理式でも矛盾からは出すことができます。
それが矛盾の推論規則です。


そして、一部に[φ]...ψみたいなものがありますが、これは自然演繹で特徴的な仮定というものです。

[φ]...ψは、φを前提としてψを証明できるということを示しています。
前提としてと言っても、必ずしもφを使ってψを証明しなければならないわけではなく、単にφのもとでψが成り立てば大丈夫です。

そして、この[φ]を仮定と呼びます。
仮定がある推論規則では、なんと仮定が成り立たないとしても、推論規則で出てきた論理式は成り立つものとされます。

つまり、たとえば仮言導入であれば、
φのもとでψを証明できるのだとしたら、実際にφであるかどうかによらずφ→ψであるということになります。

考えてみたら当然のことですね。


私が勉強したソースのウェブサイトを丸パクリして説明すると、

日本語の証明からパターンを抽出するという話を冒頭のほうでしましたが、
自然演繹というのは、数学者が自然言語で行っていた証明をそのまま推論規則にしてしまったというものなのだそうです。


その自然言語の証明で特徴的なのが仮定だというわけです。

たとえば、場合分け論法というのがあって、
xxxと仮定するとzzz、yyyと仮定してもzzzである、ここでxxxまたはyyyなので、いずれにせよ仮定によらずzzzであるという論法になりますが、

これはそのまま選言除去という推論規則になっていますね。

私はこの説明を読んだときに自然演繹のカッコよさにシビレたのですが、分かるーって人いますかね…。


あと、背理法ですね。
xxxと仮定すると矛盾する、よってxxxでない、というものと
xxxでないと仮定すると矛盾する、よってxxxである、というものがありますが、

自然演繹において推論規則となっているのは前者(否定導入)だけです。

後者がいわゆる背理法ですが、こちらは自然演繹(NK)では排中律と否定導入を用いて証明できます。


余談ですが、数学の証明でもうひとつ代表的なものに、数学的帰納法がありますね。
これは論理自体の性質というより自然数の性質なので、推論規則にはなりませんでした。

自然数の性質を述べているペアノの公理というところに、数学的帰納法の論理学的な裏付けとなる公理があります。


話を戻すと、仮定というのはどういうふうに使うのかというと、自然言語による証明と同じように、
前提に関係なく、いきなり適当にこうであると仮定してしまっていいということです。

そして、その仮定のもとで何かが成り立つという論理の関連を見つけたときに、実際に仮定が成り立っていなくても証明できるような論理式が出てくる推論規則というのが、仮定を使う推論規則です。

推論規則で論理式を出してしまったあとは、仮定は無かったものとしてしまって大丈夫なわけですね。




健全性と完全性


上のほうで、解釈したら真である論理式に推論規則を適用したら出てきた論理式も同じ解釈において真である、というとき推論規則は妥当である、と書きました。

推論規則が妥当であることによって、解釈して真になる前提に何回か推論規則を適用して出てきた帰結は、同じ解釈において真であるとも書きました。

このようなものを健全な形式体系であるといいます。

記号で書けば、
Γ ⊦ φ のとき Γ ⊧ φであるという性質です。

自然演繹(NK)は意味論によって健全であることが証明できます。


一方で、自然演繹は
Γ ⊧ φ のとき Γ ⊦ φであるという性質も持ちます。

これは、あらゆる解釈においてΓがすべて真ならφも真であるというとき、つまり簡潔に言うとΓならφだというとき、
自然演繹の操作を用いてもΓを前提としてφを証明できるということです。

これを完全であるといいます。
これも証明できます。

私が知ってるのは、
⊧ φ のとき ⊦ φ という、Γが空の場合の証明だけですが…。


完全性はすなわち、意味論において正しいとされる推論はすべて形式体系において証明できるということなので、かなり大事な性質となります。




証明の例


ここでは非常に簡単にですが、自然演繹による証明の例を示します。


対偶の法則: φ→ψ ⊦¬ψ→¬φ

1: φ→ψ (前提)
2: [¬ψ] (仮定)
3: [φ] (仮定)
4: ψ (3, 1に仮言除去)
5: ⊥ (4, 2に否定除去)
6: ¬φ ([3]...5に否定導入)
7: ¬ψ→¬φ ([2]...6に仮言導入)

となります。
(仮定)と書いたものは、結局のところ前提としては残らないですね。


ドモルガンの法則のひとつ: ¬φ∨¬ψ ⊦ ¬(φ∧ψ)
1: ¬φ∨¬ψ (前提)
2: [φ∧ψ] (仮定)
3: [¬φ] (仮定)
4: φ (2に連言除去)
5: ⊥ (4, 3に否定除去)
6: [¬ψ] (仮定)
7: ψ (2に連言除去)
8: ⊥ (7, 6に否定除去)
9: ⊥ (1, [3]...5, [6]...8に選言除去)
10: ¬(φ∧ψ) ([2]...9に否定導入)

長いですね。
こちらは排中律を使わないですが、前提と帰結を逆にした下の例では排中律を使います。


ドモルガンの法則のひとつ: ¬(φ∧ψ) ⊦ ¬φ∨¬ψ

1: ¬(φ∧ψ) (前提)
2: [φ] (仮定)
3: [ψ] (仮定)
4: φ∧ψ (2, 3に連言導入)
5: ⊥ (4, 1に否定除去)
6: ¬ψ ([3]...5に否定導入)
7: ¬φ∨¬ψ (6に選言導入)
8: [¬φ] (仮定)
9: ¬φ∨¬ψ (8に選言導入)
10: φ∨¬φ (公理:排中律)
11: ¬φ∨¬ψ (10, [2]...7, [8]...9に選言除去)

難しい例を持ってきました。

ここで特徴的なのは、10行目で排中律を使用している点です。
すぐに後述しますが、これはNKでは証明できて、NJでは不可です。




直観主義論理(NJ)


先ほどまでNKを軸に解説すると言っていましたが、NJではどう違ってくるのでしょうか。

NKとNJの違いはたった1つだけで、NKにあった排中律が、NJでは存在しません。

つまり、NJのほうが証明に制限がかかっている状態となります。
具体的に言えば排中律を使う証明がNJでは不可能となります。


この制限は地味に大きくて、NJでは二重否定の除去、すなわち¬¬φからφを証明することができません。

xxxではないということはない、というのはxxxである、とはまた別物だということです。…深いですね。


さっきも題材にしましたが、いわゆる背理法は
xxxでないと仮定すると矛盾する、よってxxxであるという論法です。

これを自然演繹で証明すると、xxxでないというのは¬φで、¬φのとき矛盾するから否定導入で¬¬φとなって、

これに二重否定の除去を適用して最終的にφが導けるということなんですが、NJでは最後の二重否定の除去ができないので、いわゆる背理法の証明はNJでは不可能なのです。

背理法が無理というのは大きいですね。


また、NJの健全性や完全性を支える意味論においても、NKのように例の{T,F}の集合で解釈するのではなく、論理式はハイティング代数というもので解釈します。

ハイティング代数というのは総称なので実際には色々あって、あらゆるハイティング代数についての事を考えて解釈するそうなのですが、

その一例として三値論理のようなものが考えられますね。


つまり、細かい話は知らないので省略しますが、NJというのは命題に真でも偽でもない状態があることを考える形式体系だと思います。

ちなみにNJのことを直観主義論理の体系とも呼んだりします。
これはある命題を主張するなら、それが直接証明できないと駄目だというものです。

ようするに二重否定の除去みたいな、裏の裏だから表、という論法は駄目なわけですね。





というわけで、自然演繹の概要的なものをさらっと紹介したつもり(さらっとになっていないかもしれない)なのですが、いかがでしたか。

あとシークエント計算の勉強が残っていますが、さすがにシークエント計算のまとめ記事は書かないですね。

少なくとも私が現在勉強している京大教授の方のサイトの内容に沿った論理学の記事は、これが最後になると思います。


そして、シークエント計算の勉強を終えたあとも論理学の勉強をしているかと言ったら、そんなこともないんじゃないかと思いますね~。

数学関連でなにか勉強できたらなぁと思うんですが、未定です。


しかし数学は難しいですが面白いですね。
紙とペンという小さな世界に、底知れなく広がる知性。

人間の脳みそのすごさを実感できますね。


ちなみに、数学者の人は数学のことを宇宙的な真理だと言いますが、
哲学者の人は、数学というのは人間の脳の中に展開されるゲームみたいなものだと言うのが多いようですね。

人間が考える論理には限界だとか穴があると思うので、私は哲学者のほうが言っていること正しいと思います。


という今の理論もまた穴があるのかもしれないわけで、メタ発言にメタ発言を重ねて、もうわけわからんですが…。

tag: 数学 論理学 構文論 論理式 証明 命題論理 直観主義 自然演繹 形式 勉強

コメント

コメントの投稿

トラックバック

トラックバック URL
http://cyberboy6.blog.fc2.com/tb.php/462-7863f562
この記事にトラックバックする(FC2ブログユーザー)

当ブログをご利用(閲覧等)になる場合は必ず「当ブログの利用規定」をお守りください。