|
|
情報証明論 |
|
目次
第１章 論理式と証明の構造
|
情報証明論というのは新しい分野です。従来、「証明」というと数学の分野のものでした。他の分野でもこの言葉は使われなかった訳ではありませんが、「証明とは何だろうか？」という疑問が人々の意識に昇ることは無かったように思えます。 数学者は「厳密」という言葉が好きですが、その数学者でさえ「厳密に」証明とは何かを知っている人は少ないのです。 世の中には「厳密」でないことが横行しています。高校の教科書の指導要領などで、「論理性を養う」などということがうたわれていますが、もし論理性に優れた生徒が世に出ていったとしたら、この世は不合理なことばかりで生きていけないでしょう。 人の上に立つ人ほど、非論理的である傾向があります。「朝令暮改」というのは当たり前で、「君子豹変す」など権力者は好き勝手を言えるのです。 上の人のでたらめの犠牲になるのは、下積みの人達です。彼等は自分の持てる力を総動員して、上の人のでたらめからくる組織のデメリットをカバーしようとします。 従ってむしろ下積みの人達の方が論理的であったりします。工事現場の監督は無理な重機の置き方をすると危険であることを予知できます。その場合経験も役だっていますが、かなり論理的な推論をしているようです。 また技術者達は己の分野においてはやはりかなり論理的な思考をします。 法律の分野においても地裁の方が論理的な判断をし、上にゆくほど、「高度に政治的な事項」であるということで判断を避けてしまうこともあります。３権分立、と教わったのは嘘だったのでしょう。 残念ながら厳密に論理的な人達は今までは恵まれませんでした。 それなのに、なぜここでそれをあらためて学ばなければいけないのでしょうか？ 実は今まではそうであったかもしれませんが、これからはそうでない、と確信できるからです。その理由はコンピュータの発達によって、世の中でコンピュータの出番が増えたことに起因しています。 コンピュータ自体何百万という論理素子からなっています。またそこで動くソフトはやはり何百万ステップという厳密に定義されたコードからなっています。 人類は「人は死ぬものである。ソクラテスは人である。ゆえにソクラテスは死ぬ」程度の論理から、いきなり人の思考能力の限界を超えたような論理の世界に放り込まれつつあるのです。 数学者は「厳密」が好き、という話をしましたが、実は数学者はコンピュータの厳密性からいったらちっとも厳密ではありません。 コンピュータプログラムの正しさを数学的に証明しようとする試みはずいぶん前からありましたが、実用的ではありませんでした。紙と鉛筆を使って数学者がする証明なんてかなりいい加減なもので、証明の結果はほとんど信用できなかったし、また本当に簡単なプログラムについてしか証明できなかったのが原因です。 しかし、現代は大変な、証明用の道具を手にしました。それはｐｒｏｏｆ ｃｈｅｃｋｅｒというソフトです。その代表的なものがＭｉｚａｒです。 この道具なら何百万ステップの証明でも厳密にチェックしてくれます。そしてコンピュータを使うことから、ＬＳＩ設計やプログラム開発の環境と親和性がいいのです。 その上、証明された命題はインターネット上で公開されているため、正しい命題やソフトや回路を、世界中のボランティアによって積み上げてゆくことができるのです。 もしこの優れた道具を使いこなせれば、高度なプロダクツを設計製造でき、また競争相手に対し優位に立てる有形無形の財を手にすることになるでしょう。 また論理性とそれをチェックする道具は、技術的な優位性を与えるばかりでなく、人間の精神にも影響を及ぼしてゆくでしょう。他者についての理解のために、論理性というものが実は重要なのです。 「他人であればなぐってもよい」などと公言する人がいたとします。論理的に言うと、それに同意する人は彼を自由になぐって良い訳です。 Ｍｉｚａｒのライブラリーは人類共有の財産です。ということは最も公共性のある思想の集まりである、ということです。皮膚の色の違いや性別や貧富の違いに拘わらず利用・適用可能な考えの集まりなのです。 論理によって人を説得することは、一般的にはこれからもむずかしいでしょう。しかしあなたの行動を決するようなとき、それは役立つでしょう。また世界中には多数でなくても論理性を大切にする有力な人達がいてあなたの味方になるでしょう。人は論理によって動かせない、といっても悲観することはないのです。そういう論理で動かない人はエサに寄ってきて捕まるけものとあまり変わらない、と思ってください。 それでは、皆さんを「証明」という「厳密な」世界に案内します。もしＭｉｚａｒについてより深く学びたい人、またここでの説明だけではよく分からない、という人は「Ｍｉｚａｒ講義録」という教科書を併せ読んでください。
|