« 「ごくろうさまでした」は逆尊敬語? | トップページ | S.I.C. 匠魂 vol.4 キカイダー+サイドマシーン&ビジンダー »

2006年1月31日 (火)

メタ論理: 演驛と帰納

「演驛」とは論理的に命題を導くことである。

「帰納法」は演驛の一つである。しかし、帰納法を学ぶことで、人は帰納のなんたるかを知る。それが「帰納」である。
我々は英語を習うときに日本語を使う。これをやや専問的には英語を対象言語として日本語というメタ言語上で扱うという。ここで「上位」ぐらいの意味で「メタ」という言葉を使っているが、英語よりも日本語が高級であると言えないように、対象言語がメタ言語に劣るということはない。

また、モンゴル語の「馬」にはいろいろな表現があるが、日本語に相当する単語がなくても長い表現を使えば日本語でだいたいの意味が説明できるように、対象言語のほうがメタ言語よりも表現力があってもメタ言語として機能できることもある。


記号論理を教えるときも日本語のような自然言語を使うが、ある時期、記号論理をコンピュータに教えようという話になった。最初は、人が解くようにプログラミングをしていたわけだが、そのうち、特定の論理ではなく、論理体系そのものを論じたり、論理体系に汎用なシステムを作りましょうという話になってきた。

Logical Frameworks とか Generic Theorem Prover などと呼ばれるプロジェクトである。

そうとはいえ、せっかく、汎用な論理体系を扱っているっていっても、そのシステムそのものに矛盾があるならどうしようもない。そこで、そのシステムをできるだけ、フォーマルに記述しようという努力がなされ、その中の一つとして論理を論理で記述しちゃいましょう。すなわち「メタ論理」を作りましょうという話があった。


実はその「メタ論理」を使うと、我々が演驛として行なっていた対象論理上の証明(forward proof)も、帰納として行なっていた対象論理上の証明(backward proof)も、メタ論理上の演驛として記述できる。

メタ論理として使うのはある種機能の制限された「高階論理」である。論理学入門で習う一階述語論理では、変数は、関数や述語の引数になるが、関数や述語の部分は変数として扱えない。それを扱えるようにしたのが「高階論理」だ。

高階論理は当然のごとく、一階述語論理を含み、高い表現力があるため、論理体系を高階論理で包括的に扱えることは知られていた。

しかし、その高階論理を制限的に使うことで、対象論理の操作を見通し良く示せることがわかったのである。


我々は高階論理だけでも、対象論理だけでもつかみにくい対象論理の姿を「メタ論理」という概念を通して帰納的に知るようになったのである。


参考文献


証明支援システム(Proof Assistant)でメタ論理を導入した Isabelle http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

高階論理については Higher-Order Logic や Higher-Order Calculus、 Type Theory などで検索してみてください。新判があるようですが、私が持ってるのは、 “An Introduction to Mathematical Logic and Type Theory: To Truth through Proof” (Peter B. Andrews, Academic Press 1986)
更新: 06/01/13,06/01/30
初公開: 2006年01月30日 15:17:18

2006-01-31 15:46:30 (JST) in ストーリー, 論理学 | | コメント (0) | トラックバック (0)

ストーリー」カテゴリ内の最近の記事

2006-08-24 絶対性

論理学」カテゴリ内の最近の記事

2006-08-24 絶対性

批評や挨拶のためのネットコミュニティ

  • はてなブックマーク(って何?) このエントリーをはてなブックマークに追加 このエントリーを含むはてなブックマーク このエントリーを含むはてなブックマーク
  • Twitter (って何?)

トラックバック

この記事のトラックバックURL:
http://app.cocolog-nifty.com/t/trackback/93568/8416062

トラックバックのポリシー

他サイトなどからこの記事に自薦された関連記事(トラックバック)はまだありません。
» JRF の私見:雑記:メタ論理: 演驛と帰納 (この記事)

コメント

コメントを書く



(メールアドレス形式)


※匿名投稿を許可しています。ゆるめのコメント管理のポリシーを持っています。この記事にまったく関係のないコメントはこのリンク先で受け付けています。
※暗号化パスワードを設定すれば、後に「削除」、すなわち JavaScript で非表示に設定できます。暗号解読者を気にしないならメールアドレスでもかまいません。この設定は平文のメールで管理者に届きます。
※コメントを書くために<b>ボールド</b>、<pre>詩文やソースコード</pre>、<a href="">リンク</a>、その他のHTMLタグが使えます。また、漢字[かんじ]でルビが、[google: キーワード] で検索指定が使えます。


ランダムことわざ: 鶴は千年、亀は萬年。