このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

「わたしはウソをつきません」と言い張る命題やプログラムを書けるのか?

エイプリルフールに「わたしはウソをつきません。」と書きました。たいした意味はなくて、すぐにウソだと分かるようなひと言のつもり。

そしたら、id:sasa2718さんに、

「この文は証明可能である」という命題を構成するとその命題は証明可能でしょうか?

というクイズ(?)を出されてしまいました

「私はウソつきです」が矛盾を引き起こしそうなことは誰でも感じるでしょう。一方、「私はウソをつきません」だと、矛盾する言明かどうかは分からないですが、直感的に胡散臭い気はしますよね。「私はウソをつきません」と言っている人を信じますか? ふつう信じないでしょ。

さて、「この文は証明可能である」という命題も、「私はウソをつきません」と言っている人みたいなもので、どうも胡散臭い。「この文は証明可能である」はホントなんでしょうか、ウソなんでしょうか?

ある程度ちゃんとした形に定式化してみます。このテの話題は何度も扱ったことがあるので説明は手短にしますがね。まず「この文は証明可能である」を、なるべく正確に表現してみます。うまく表現できたら、それが証明可能かどうかを調べることになります。実は枠組みだけで息切れしてるので、続きは皆さん考えてください。

内容:

形式的な演繹系と証明可能性

命題を表現するために、言語体系LLを考えます。Lightweight Language じゃなくて Logical Language です。LLで普通に論理式を定義できるとしましょう。自由変数を持たない論理式を論理文(logical sentence)とか命題(proposition)と呼び、その全体を Prop(LL) とします。

LLには、単に論理式だけでなく、推論や証明(を形式化したモノ)を備えているとします。つまり、LLは演繹系です。A∈Prop(LL) が、(LLの演繹系で)証明可能なことを |- A と書きます。

命題Aが「この文は証明可能である」という意味を持つとして:

  • |- A ⇔ 「この文は証明可能である」という命題は証明可能
  • |- A ではない ⇔ 「この文は証明可能である」という命題は証明不可能

ということになります。

プログラミング言語と処理系/実行系

LLのなかで「xは証明可能である」という命題を構成しなくてはなりません。そのために、演繹系としてのLLを、なんかのプログラミング言語で実装することにします。「なんかのプログラミング言語」をPLとします。Programming LanguageからPLと、ベタですね。

PLのソースコードの全体をProg(PL)とします。PLには実行系も備わっているとします。その実行系を以下に定義します。

まず、DをPLのデータ領域としましょう。Dは、自然数とか二分木とかバイト列とかの領域です。単なる集合ではなくて、Dの上に演算や関係が存在するとします。それらの演算や関係に対応する記号は、PLの構文に含まれているとします。また、Dの要素は、PLの定数記号(リテラル)として表現可能だとして、Dの要素と定数記号は同一視しちゃいます。

PLのコンパイラは Compile:Prog(PL)→D という関数だとします。データ領域Dは、コード領域も含んでいて、コンパイル結果はDに入ります。Dがバイト列の領域なら、これは自然なことです。

PLのインタプリタ(あるいは仮想機械、ハードウェアでもいいです)をExecとしましょう。ApplyとかEvalと書くこともあります。Execは D×D→D という関数です。正確に言えば部分関数で、未定義部分があるかもしれません。Execの第1引数はコンパイル済みコードで、第二引数は入力です。Execの戻り値はプログラム実行後の状態=出力です。ここで、入力と出力は、適当なレジスタ群とかメモリブロックの値だと思ってください。

次の等式は、「プログラミング言語とその処理系の基本原理」とも言える大事な等式です。もっとも、後の話に深く関わるわけじゃないですが*1、僕の好みな話題なので。

  • p∈Prog(PL)、x∈D に対して、Exec(Compile(p), x) = 【p】(x)

ここで【p】は、プログラムソースコードpの超越的表示的な意味を与える関数です。【p】をFと置くと、数学的な関数 F:D→D が、F(x) := Exec(Compile(p), x) として定義されるとも言えます。(関数は部分的かもしれませんからね。要注意。)

LLとPLを関連付ける

LLの演繹系としての機能を、PLのプログラムとして実現することにします。そのために、LLとPLを関連付けます。次の2つの方法を使って関連付けるのです。

  1. LLの論理式や証明を、データ領域Dのなかにマップする関数 Code:Formula(LL) + Proof(LL) → D
  2. PLのプログラムに名前を付けてLLの関数記号として使えるようにするメカニズム

Codeは、Dへのゲーデルコード化です。Formula(LL)はLLの論理式の集合です。Prop(LL)⊆Formula(LL) なので、LLの命題はFormula(LL)に含まれます。Proof(LL)は、LLのなかで証明と認めるられる図形(証明図)の集合です。Formula(LL)とProof(LL)のCodeによる像は、プログラミング言語PLで書いた関数で識別できるとします。

つまり、isFormula, isProofがPLで書いた1変数関数だとして:

  • x∈Code(Formula(LL)) ⇔ isFormula(x) ⇔ Exec(Compile(isFormulaのソース), x) = true
  • x∈Code(Proof(LL)) ⇔ isProof(x) ⇔ Exec(Compile(isProofのソース), x) = true

「PLのプログラムに名前を付けてLLの関数記号として使える」とは次にようなことです; LLのなかに関数記号がたくさん準備されていて、その1つfをp∈Prog(PL)にバインドします。すると、関数記号fの意味が f(x) := Exec(Compile(p), x) という数学的な関数として決まるのです。LLの項や論理式の意味を定義するとき、PLの関数の意味をそのまま使用できることになります。あと、Dの要素(=PLの定数記号)はLLでも定数記号に使えることにします。

演繹系をプログラミングする

演繹系LLの論理式や証明は、Codeを経由してデータ領域D上のデータとなります。データ領域D上で動くプログラミング言語PLを使って、次のような関数を実装しましょう。

  • isProvedBy(x, y) -- xは命題を表すデータ、yは証明を表すデータで、yはxの証明となっている(か調べる)。
  • findProof(x) -- xは命題を表すデータ、isProvedBy(x, y) であるようなy(を探して出力する)。
  • provable(x) -- xは命題を表すデータ、isProvedBy(x, y) であるようなyが存在する(か調べる)。

isProovedBy:D×D→boolean、findProof:D→D、provable:D→boolean です。ペアリングD×D→Dがあって、booleanもDに埋め込めば、isProovedBy:D→D、provable:D→D とみなしてもかまいません。なんでも D→D と思えるってことね。ただし、くどいけど、これらは部分関数かもしれません。

さて、がんばってこういうプログラムを書いたとすると:

  • provable(Code(A)) = true ⇔ |- A

演繹系と命題に関するメタな言明 |- A が、PLで書いたプログラムprovableを、データ領域Dの特定データに対して走らせることによって判定できることになりました。えーとですね、provableが部分関数かもしれないですけどね(ほんとにクドイ)。

自己言及してみる

LLの命題Aがあったとして、この命題Aを「わたし」だとします。Code(A)はデータ領域Dのデータですが、まー、Code(A)も「わたし」だと言っていいでしょう。念のため a = Code(A) としておきます。Aがホントの「わたし」、aはコード化された「わたし」。

somePredicate:D→boolean がプログラミング言語PLで書かれた述語(boolean値の関数)だとします。PLで書かれた関数は、LLのなかの関数記号にバインドしていいのでした。同じ記号somePredicateをLLの関数記号(述語記号)としても使ってしまいます。データ領域Dの具体的なデータaを取ってきて、somePredicate(a) をLL内で考えると、これはLLの命題です。この命題をAと置いてみれば:

  • A ≡ somePredicate(a)

もし、命題Aのコード化がデータaだとすると、これは次のような意味を持つでしょう。

  • わたしは「『コード化されたわたし』はナントカです」という命題です。

somePredicateとしてprovable(証明可能)を使えば:

  • わたしは「『コード化されたわたし』は証明可能です」という命題です。

別な言い方をすると:

  • この命題は「この命題は証明可能です」という命題です。

不動点を探せ

なんか狐につままれたような気がしますね。もう一度確認してみましょう。

我々は論理言語/演繹系をデータとしたプログラミングにより、provableというプログラムを作りました。ですから、λx∈D.(Exec(Compile(provableのソースコード), x)) という関数が定義されます。この関数に'provable'という記号で名前を付けます。記号'provable'が論理言語LLの関数記号だとして、provable(x) = true は論理言語LLの論理式です。xは変数記号で、trueは定数記号(Dの特定の要素)。

provable(x) = true が単なる論理言語LLの構文的対象であることを強調するために引用符を付けて 'provable(x) = true' とも書くことにします。

'provable(x) = true' の変数xをDの具体的な要素aで置き換えると(置き換えは構文的な操作)'provable(a) = true' となります。これは自由変数を持たないので命題です。LLの論理式(命題も含む)は、ゲーデルコード化CodeでDのなかにマップできてCode('provable(a) = true') はDの具体的な要素です。

データ領域Dの要素 Code('provable(a) = true') が、最初のaと一致することは一般には期待できませんが、たまたま一致した状況では:

  • a = Code('provable(a) = true') がDで成立する。

aは命題のコードですが、aのもとになっている命題をAと置けば、Aの内容的な意味は:

  • Aのコード化が証明できるかどうか判断したらtrueとなる

もっと簡略にいえば「Aは証明できる」です。

λy∈D.(Code('provable(x)'のxをyで置き換えた命題)) という関数を考えると、これは D→D の関数(部分関数)です。f = λy∈D.(Code('provable(x)'のxをyで置き換えた命題)) とおけば、a = Code('provable(a) = true') は次の形にかけます。

  • a = f(a)

つまり、aはfの不動点です。ただし、不動点方程式をDのイコールで考える必要はなくて、D上の同値関係〜で、次の条件を満たすものでもOKです。

  • AとBが論理的に同値 ⇔ Code(A)〜Code(B) Code(A)〜Code(B) ⇒ AとBが論理的に同値

この性質を持つ同値関係に対して不動点方程式を考えます。

  • a 〜 f(a)

この不動点方程式に解があれば、それが「この文は証明できる」に対応します。

息切れ

これで枠組みは述べました。しかし、論理言語LL、プログラミング言語PL、データ領域D、D上の同値関係〜などについて、実際のところは何も述べてません。不動点の存在は、これらの言語とデータの構成の仕方に依存します。

「証明できる」の解釈は、演繹系における関係 |- 、あるいはプログラムprovableですが、これをどう作ろうと「オレ的にはこれが証明」と言い張れば容易に不動点を探せるかもしれません。形式化された証明が「証明」と呼ぶにふさわしかいかどうかは、非形式的・常識的に判断するしかないのでしょう。

というところで息切れしたので、今日はここまでです(続きはたぶんないです)。

*1:コンパイルがプログラムの世界のゲーデルコード化だ、という意味で、論理と同じ構造をしています。