ウカシェビッチの公理から論理計算の法則を証明する努力を延々とやってきたが、その目的は、すべてのトートロジーが証明可能な定理であるという狭義の完全性を直接的に証明するにはどうすればいいかを考えてみたからだ。
完全性定理とは公理系の定理と、トートロジーとが同値であることを意味するが、それには次の二つの方向性がある。 健全性:形式的体型で証明できることは、どんな意味(モデル)のもとでも正しい 完全性:どんな意味(モデル)のもとでも正しいことは、形式的体型で証明(導出)できる。 教科書の健全性の証明はすぐに納得できた。それは、公理が全てトートロジーであること。前件肯定 modus ponens によって証明される定理は全てトートロジーであることから、任意の命題がトートロジーであることを再帰的に証明することができる。 しかし、完全性の証明については、どうしても違和感を拭えなかった。それは、完全性定理の証明には、命題計算のトートロジーと公理系の定理が同値であるということについての言及がないからだ。 例えば、公理が A -> A だけで、推論規則が前件肯定である公理系を考えた時、明らかにこの公理系では、論理計算で得られるトートロジーの一部しか証明できない。 そこで、命題計算のトートロジーが全て公理系で演繹可能である直接の証明は出来ないかどうかを考えてみようと思ったのだ。 命題計算のトートロジーはその真理表を直接に計算することによって知ることができる。しかし、任意のトートロジーが証明可能であるかどうかを調べるためにはそれでは不十分であろ。そこで、任意のトートロジーを標準的なトートロジーに変換する方法はないかどうかを考えてみた。 まず、標準的なトートロジーとは何かということだが、それは、論理式に含まれる任意の個数の原子式について、選言標準形を作ることによって定めることができる。また、任意の命題は論理計算の法則によって、選言標準形に同値変換できる。そこである個数の原子式を含むすべての論理式は、それがトートロジーであれば、標準のトートロジーへ同値変換できる。したがって、標準的なトートロジーからは、同じ個数の原子式を含む任意のトートロジーへの逆変換が可能である。つまり標準的なトートロジーから演繹可能であると考えた。 そこで、標準的なトートロジーが証明可能であることと、論理計算の法則が証明可能であることを示せば、論理計算によるトートロジーは全て公理から証明可能であることになる。すなわち、命題論理の完全性は論理法則が公理から演繹可能であることを証明することによって、証明される。 これはこれで意味のあること(すでに証明されていると思われるとは言え)だと思うが、この試みの過程で、教科書の完全性定理の証明に対する違和感の原因がわかった。それはトートロジーの意味の取り方が違っていたのだ。 教科書の証明の真理関数はあくまで、論理式が証明可能であるかどうかを判別するための関数だったのだ。それをトートロジーとは真理表で計算される恒真命題であると考えたために教科書に記された完全性定理の意味を汲み取ることができなかったのだ。 例えば A -> A を公理とする公理系の場合、この公理系で演繹される定理の全てはトートロジーであるが、論理計算では、この公理系で証明できないたくさんのトートロジーがある。しかし、トートロジーの意味をこの公理系で証明可能な定理には真を、それ以外には偽を与える真理関数で与えられる論理式であると考えると、論理計算ではトートロジーであっても、この公理系ではトートロジーではない命題があっても良い。完全性定理はこのような真理関数によって判別されるトートロジーについての証明だったのだ。 このように真理関数を命題が定理であれば真、そうでなければ偽を与える関数であると考えると、教科書の完全性の証明の意味がわかる。公理系によって証明されるのは論理式が証明可能かどうかということだけで、論理式の持つ意味には言及しない。しかし、この公理系の定理に真理値を与えるモデルを与えることによって、その論理式の意味を論じることができる。この真理表によって与えられたモデルと証明可能性が同値であることが証明されたのだ。 例えば A -> A から演繹される定理について考えてみる。明らかに命題の文法規則から命題であると定義される命題の集合は、A -> A から演繹される命題と、そうでない命題の2つに分けられる。この時、公理からある命題を実際に演繹した時、その命題は定理であることがわかる。しかし、定理に属する命題の集合から任意に命題を取り出したとして、その命題の証明が得られないうちは、それが定理であるかどうかを言うことはできない。教科書の完全性の証明は、それが、その命題が定理の集合の命題であれば、直接的な証明がなくてもそれが定理であることは保証することができるということを証明しているのだ。 勘違いから結構大変な努力をする羽目になったのだが、そのおかげで公理系から定理を証明することのパズル的な面白さに気がついた。命題論理がゲーデルの完全性定理を理解するための単なる踏み台ではなくて、それ自身が奥深い面白い対象であることに気づかされた。誰か、ウカシェビッチの公理系の全てについての分かりやすい教科書を書いてくれないだろうかと思ったりする。
by tnomura9
| 2016-09-17 07:34
| 考えるということ
|
Comments(0)
|
カテゴリ
新型コロナウイルス 主インデックス Haskell 記事リスト 圏論記事リスト 考えるということのリスト 考えるということ ラッセルのパラドックス Haskell Prelude Ocaml ボーカロイド 圏論 jQuery デモ HTML Python ツールボックス XAMPP Ruby ubuntu WordPress 脳の話 話のネタ リンク 幸福論 キリスト教 心の話 メモ 電子カルテ Dojo JavaScript C# NetWalker ed と sed HTML Raspberry Pi C 言語 命題論理 以前の記事
最新のトラックバック
最新のコメント
ファン
記事ランキング
ブログジャンル
画像一覧
|
ファン申請 |
||