top  Index  Search  Changes  RSS  Login

不完全性定理

以下は旧版です. 新版をご覧ください.




不完全性定理のLisp, Mathematicaによる記述ゲーデルの証明 が理解できませんでした(is-unprovable なんて「実装」できるわけないやん). そこで, 「こんな解釈なのかなあ?」というメモを晒してみます. 口調は解説風ですが山勘で書いているだけですから, つっこみをお待ちしています. (理解のあやしさは, 同趣旨のモナドと比べてもずっとひどいです)

※ lisp と言いつつ文法が scheme 風なのは, 私の趣味


仮想言語 lisp+

一般に, 論理式を S 式に翻訳して表現することができます.

  • a∨b …… (or a b)
  • ¬(a∨b) → (¬a)∧(¬b) …… (imply (not (or a b)) (and (not a) (not b)))

特に, ∧(かつ), ∨(または), ¬(でない), →(ならば), だけを扱った論理式なら, lisp プログラムとして解釈することも可能 です*1.

次に, 普通の lisp をちょっと拡張した lisp+ という言語を考えます. 拡張はただ一点, 「all?」という組み込み関数を持つことだけです. (all? (lambda (x) …)) は, 「x にどんな S 式を代入しても『…』が真」なら真を, さもなくば偽を返します.

もちろん, こんな処理系を「実装」することは不可能です. でも, 「仕様」として, ともかく考えるだけ考えてみます.

「all?」を持つおかげで, ∀(全ての)や∃(或る)を含む論理式でも, lisp+ プログラムとみなすことが可能に なります*2.

  • ∀x p(x) …… (all? (lambda (x) (p x))) もしくは (all? p)
  • ∀x ∃y q(x,y) …… (all? (lambda (x) (exist? (lambda (y) (q x y)))))

我々は lisp+ 処理系を持っていないので, lisp+ での評価結果を 機械的に求めることはできません. それでも, 人間が頭で考えることにより, 評価結果がわかる場合もあります. たとえば,

(all? (lambda (x) (list? (list x))))
(exist? (lambda (x) (not (list? x))))

などは見るからに真です. また,

(exist? (lambda (x)
          (exist? (lambda (y)
                    (exist? (lambda (z)
                              (exist? (lambda (n)
                                        (and (integer? x) (integer? y)
                                             (integer? z) (integer? n)
                                             (> x 0) (> y 0) (> z 0) (> n 2)
                                             (= (+ (power x n) (power y n))
                                                (power z n)))))))))))

は, 偽であることが最近わかったそうです(フェルマーの最終予想). 一方,

(all? (lambda (x)
        (imply (and (integer? x) (>= x 2))
               (exist? (lambda (p)
                         (exist? (lambda (q)
                                   (and (prime? p) (prime? q)
                                        (= (* 2 x) (+ p q))))))))))

は, 真か偽かまだわかっていないそうです(ゴールドバッハ予想).

このような「人間による判定」とは, 要するに数学的な「証明」のことです. 後ほど不完全性定理を論じるためには, 証明とは何かをはっきりさせておかないと いけません.

証明とは

「証明」のためには, 前提となる「公理」と「推論規則」とが必要です.

  • 公理の例: (equal? x (car (cons x y))) は常に真
  • 推論規則の例: 論理式 A と論理式 A→B から論理式 B を導いてよい

公理と推論規則をあわせたものを「体系」と呼びます. ふつうの数学とふつうの lisp で想像されるような体系が, いまは与えられているとします*3.

体系という言葉は日常語っぽくて目立ちにくいですが, ここで言った意味での「体系」は, 今後いつも重要なキーワードになります. 心に留めておいてください.

さて, 証明とは, 論理式の列のことです. もちろん, どんな列でもいいわけではなく, 各論理式が,

  • 公理であるか, または
  • それまでに出た論理式たちから推論規則によって導かれるか

のどちらかであることが要求されます. さらに, 最後の論理式は, 証明したい論理式そのものに一致しないといけません. このような論理式の列を「証明列」と呼ぶことにします.

最初に述べたとおり, 論理式は S 式で表現できますから, 証明列は S 式のリストとしても表現可能です. S 式のリストは S 式なので, 結局, 証明も S 式で表現できることになります.

ここで興味深いのが, 「証明が正しいかどうか」を lisp で 機械的にチェックできるという事実 です*4.

;; S 式 p が S 式 z の証明となっていれば真, さもなくば偽
(define (proof? p z)
  p の各要素について
  ・公理か?
  ・あるいは, それより前の要素から推論規則で導かれるか?
  をチェック.
  さらに, p の最後の要素が z と等しいかもチェック)

proof? はただの関数であって, 特殊形式やマクロではありません. 引数はどれもふつうに評価されます.

(proof? p '(= (+ 2 2) 4))  ;; 「'」が必要

証明可能とは

「S 式 z が証明可能である」という主張は, 「(proof? x z) が真となる S 式 x が存在する」と言いかえられます. lisp+ でなら, 次のように書けます.

(define (provable? z)
  (exist? (lambda (x) (proof? x z))))

短く「証明可能」と言っていますが, 正確には

「その S 式を lisp+ で評価すると真になる」という主張が,
与えられた体系において証明可能

の意味です.

証明可能でないときは証明不可能と呼びます.

(define (unprovable? z)
  (not (provable? z)))  ;; つまり (all? (lambda (x) (not (proof? x z))))

なお, provable? や unprovable? もやはりただの関数です.

(provable? '(= (+ 2 2) 4))  ;; 引数は評価されるから, 「'」が必要

さて, 証明不可能なこと自体は, 別にやばくはありません. 実際, 次の S 式はどう見ても証明不可能です.

(list? 'a)

この S 式(を lisp+ で評価した結果)は偽に決まっていますから, 「真であることを証明してみろ」と言われても無理な相談.

今のは, むしろ否定 (not (list? 'a)) の側が証明可能となっている例でした. こんなのは何もやばくない. やばいのは,

  • ある S 式 (…) が証明不可能
  • しかも, その否定 (not (…)) も証明不可能

という状況です. こんなやばい S 式を, 後ほど組み立ててみせます.

しつこく注意しておきますが, 「証明可能」や「証明不可能」は, 体系しだいで変わってきます. 今後もこれらの用語にはすべて, 「いま与えられている体系のもとで」 という但し書きをつけて読んでください.

大前提

証明可能性に関して, 押さえておかないといけない大切なことがあります. もし仮に, 「z と『z の否定』がどちらも証明可能」となったら, これはとんでもなくまずいでしょう. そんな困った体系のもとでまともな話ができるとは思えません. ですから, 「…」のようなことが決しておきないような体系(無矛盾な体系)が 与えられていることは, 大前提とします.

念のため S 式でも書いておくと…

(provable? z)
(provable? `(not ,z))

「この両者は決して同時に真とはならない」という性質が「無矛盾性」です.

さらにもう一つ, 押さえておくべき前提があります. 次の二つが同時に成立することはない, という前提(ω無矛盾性)です.

  • □ のところにどんな S 式を書いても, S 式 (f '□) は証明可能
  • なのに, S 式 (exist? (lambda (x) (not (f x)))) も証明可能

後者は反例の存在を主張しているのだから, 前者と両立しないのは一見「あたりまえやんけ」ですが…

両者をこう書き直すと, そうストレートに「あたりまえ」でもないのが 見えるでしょうか.

(all? (lambda (x) (provable? `(f ',x))))      ;; ア
(provable? '(not (all? (lambda (x) (f x)))))  ;; イ

「この両者は決して同時に真とはならない」という性質が「ω無矛盾性」です. 単なる無矛盾性とは違うことを確認してください.

それでもまだ「あたりまえやんけ」という気がするなら, 「証明とは」からもう一度読み直すとよいかもしれません. 我々はいま, 何か「体系」が一つ与えられているとして, その体系のもとで証明可能かどうかを議論しています. ですから, provable? の振舞いも, 体系しだいです. でたらめに作った体系だと, provable? もでたらめな振舞いとなり, 上の両者が同時に真となるおそれがあります.

こんなわけで, ω無矛盾性が成り立つかどうかは体系しだいです. 以下では, 体系がω無矛盾なことも大前提とします.

※ ω無矛盾なら自動的に, 無矛盾性も保証されます. 理由は, もし体系に矛盾があるなら, (背理法を使って)何でも証明できてしまうから. つまり, 矛盾のある体系では provable? が常に真なため, アもイも真でω矛盾となるから です*5. 上の保証はこの対偶.

「証明可能」 = 「証明可能なことが証明可能」

ω無矛盾性から, ちょっと禅問答めいた定理が導かれ ます*6. (後で使います)

定理 1: 体系がω無矛盾なら,
「S 式 z が証明可能」なことと,
「S 式 (provable? z) が証明可能」なこととは同値.

言いかえれば, 以下の二つの S 式(を lisp+ で評価した結果)の値が 必ず一致するという主張です.

  • ウ. (provable? z)
  • エ. (provable? '(provable? z))

この主張が成り立つことは以下のように示されます. (つらければスキップしてください. おもしろくなるのは次節からなので.)

まず, ウが真ならエも真なことを示しましょう. ウが真ということは, ある S 式 p が存在して, (proof? p z) が真になると いうことです(∵provable? の定義). 問題は, この (proof? p z) が真なことを, 「与えられた体系で」 証明できるかどうかですが…

proof? は, (lisp+ でなく) lisp の関数でしたから, 機械的に計算が可能です. すると, (proof? p z) を機械的に計算してみせることで, これが真なことを示す証明列が得られる(つまり証明できる)ことになります.

(proof? p z) が導かれれば, そこからさらに「推論規則」を使って

(exist? (lambda (x) (proof? x z)))

を導けます. これは要するに (provable? z) です. こうして, 「(provable? z) に至る証明列」ができました. つまり, 「(provable? z) は証明可能」と言えたわけです. 以上で, 「エが真なこと」が示されました.

次に, ウが偽ならエも偽なことを示しましょう. これにはω無矛盾性が必要となります.

ウが偽ということは, どんな S 式 q を持ってきても (proof? q z) が 偽になるということです. 言いかえれば, (not (proof? q z)) が真です. ここで, 先ほどと同じ理由(proof? は機械的に計算可能)から,

(not (proof? q z)) が真なら,
(not (proof? q z)) は証明可能

と言えることに注意しましょう. こうして, 「どんな S 式 q を持ってきても (not (proof? q z)) が証明可能」 という結果が得られました.

ω無矛盾性の定義を思いだせば, 上の結果「…」は

(exist? (lambda (x) (proof? x z))) は証明不可能

を意味することになります. すなわち,

(provable? z) は証明不可能

こうして「エが偽なこと」が言えました.

やばい S 式の組み立て

不完全性定理は, 真だとも偽だとも証明できないような S 式 baz が 存在することを主張します. くどく言えば…

  • S 式 baz (を lisp+ で評価した結果)の値が真なことは証明不可能
  • 一方, この値が偽なことも証明不可能

ここからは, lisp を使って, そんなやばい S 式を実際に 組み立てます*7. ただし, 気の効いた処理系だとかえって見にくいので, 50 行ほどの即席 lisp もどきインタプリタ (後述)をでっちあげて実行しています.

まずは, S 式 x から「x を x 自身に適用させる」 という S 式を作ってみます.

(define w (lambda (x) (list x x)))
; ==> (lambda (x) (list x x))
(w 'hoge)
; ==> (hoge hoge)

この関数 w を w 自身に適用すると, おもしろい S 式 foo ができます.

(define foo (w w))
; ==> ((lambda (x) (list x x)) (lambda (x) (list x x)))

foo を評価した結果は, foo 自身と同じです.

(equal? foo (eval foo))
; ==> #t

foo はこの先使いませんが, 練習ということで.

次に, S 式 x から 「x を評価して得られる S 式は証明不可能だ」という S 式を作る 関数 u を用意 します*8.

(define u (lambda (x) (list 'unprovable? x)))
; ==> (lambda (x) (list 'unprovable? x))
(u '(hoge fuga))
; ==> (unprovable? (hoge fuga))

同様に, 「(x x) を評価して得られる S 式は証明不可能だ」という S 式を作る 関数 uw も書いておきます.

(define uw (lambda (x) (u (w x))))
; ==> (lambda (x) (u (w x)))
(uw 'hoge)
; ==> (unprovable? (hoge hoge))

これらを使って, やばい S 式を組み立てます.

(define bar (w uw))
; ==> ((lambda (x) (u (w x))) (lambda (x) (u (w x))))
(define baz (uw uw))
; ==> (unprovable? ((lambda (x) (u (w x))) (lambda (x) (u (w x)))))

何がやばいかというと, こうなっていることがやばい.

  • baz = `(unprovable? ,bar)
  • (eval bar) = baz

実際, 次の二つが同時に成り立っていることを確認できます.

(equal? baz (u bar))
; ==> #t
(equal? baz (eval bar))
; ==> #t

だめ押しで, 生の姿でも書いておきます.

((lambda (x) (u (w x))) (lambda (x) (u (w x)))) ;; bar の S 式を評価すると…
; ==> (unprovable? ((lambda (x) (u (w x))) (lambda (x) (u (w x))))) ;; baz に

この結果を吟味するにつれて, やばさがこみあげてきます. …が, いまの段階であまり悩みはじめない方が良いでしょう. この結果を言葉で解釈しようとすると, ついつい「体系」のことを忘れてしまい, 勘違いにはまりがちです. この先やるように, lisp での表現を活かしながら議論する方が, 混乱を予防できます.

なお, 後で使うため, baz の否定には not-baz という名前をつけておきます.

(define not-baz (list 'not baz))
; ==> (not (unprovable? ((lambda (x) (u (w x))) (lambda (x) (u (w x))))))

eval と eval+

吟味をはじめる前に, 一点だけ確認しておきましょう. lisp での eval と区別するために, lisp+ での評価は eval+ と書くことにします. lisp の eval では, もし途中で (all? …) の評価が必要になると, エラーが発生します(「all?」が未定義). この場合には (eval x) と (eval+ x) とは結果が異なります. 一方, エラーにならないような S 式 x では, 両者の結果は等しく なります*9.

eval の方はただの lisp だから実際のインタプリタで確認できます (いまやってみせたとおりです). しかし, eval+ の結果がどうなるかは, 人間が頭で考えないといけません.

定理 2: (eval+ baz) の値は (unprovable? baz) の値と等しい.

これは以下のように示せます.

baz, すなわち S 式

(unprovable? ((lambda (x) (u (w x))) (lambda (x) (u (w x)))))

を eval+ したいわけですが, 頭を楽にするために

(let ((arg ((lambda (x) (u (w x))) (lambda (x) (u (w x))))))
  (unprovable? arg))

と変形しておきましょう. 式中に bar が見えていますから,

(let ((arg (eval+ bar)))
  (unprovable? arg))

と書き直すこともできます. さらに, (eval+ bar) = (eval bar) = baz でしたから,

(let ((arg baz))
  (unprovable? arg))

としても同じです. これならいっそ, はじめから

(unprovable? baz)

と書けばよい.

定理 3: (eval+ not-baz) の値は (provable? baz) の値と等しい.

これは当然です. not-baz の定義から, (eval+ not-baz) の値は

(not (eval+ baz))

の値と等しい. そしてこの式は, 定理 2 から

(not (unprovable? baz))

と展開されます. これを

(provable? baz)

と書き直せるのは, unprovable? の定義から自明でしょう.

定理 4: 定理 2 も定理 3 も, (与えられた体系で)証明可能.
すなわち, 次の式の値はどちらも真.
(provable? '(equal? (eval+ baz) (unprovable? baz)))
(provable? '(equal? (eval+ not-baz) (provable? baz)))

なぜなら, (eval bar) が baz なことは機械的に計算すれば確かめられるし (定理 1 の証明中でも使ったロジック), それに基づく定理 2 や定理 3 の証明でも, やったことは自明な式変形だけだったからです*10.

どうやばいか

さて, では本題に入ります. 本題(ゲーデルの第一不完全性定理)は,

  • baz は証明不可能である
  • not-baz も証明不可能である

という二つの定理です.

本題(前半)

定理 5: baz は証明不可能である.

これは以下のように背理法で示されます.

もし仮に baz が証明可能だったとしてみましょう. つまり, (provable? baz) が真だというわけです. 定理 1 より, これは

(provable? '(provable? baz))

が真なことを意味します.

ところが一方, 定理 2 によれば, (eval+ baz) の値は (unprovable? baz) の値と等しい, つまり (eval+ '(unprovable? baz)) の値とも等しいのでした. しかも, そのことは証明可能でした(定理 4). よって, (provable? baz) が真なら

(provable? '(unprovable? baz))

も真となります.

与えられた体系において, ある式 (provable? baz) と その否定 (unprovable? baz) とがどちらも証明可能という結果に なってしまいました. これは, 大前提である「体系の無矛盾性」に反します. よって, 背理法により, baz は証明不可能なことが示されました.

本題(後半)

定理 6: not-baz も証明不可能である.

これもまた背理法で示します.

もし仮に not-baz が証明可能だったとしてみましょう. つまり,

(provable? not-baz)

が真だというわけです.

定理 4 によると (provable? not-baz) が真なら

(provable? '(provable? baz))

も真になります. さらに定理 1 より, この値は

(provable? baz)

とも同じです. つまり, この式も真でないといけません.

与えられた体系において, ある式 baz とその否定 not-baz とが どちらも証明可能という結果になってしまいました. これは, 大前提である「体系の無矛盾性」に反します. したがって, 背理法により, not-baz は証明不可能なことが示されました.

それがどうした

「結論はわかった. でも, ありもしない言語 lisp+ を勝手に想像して, その言語に妙な挙動が みつかったからといって, それがどうした. お前の考えた lisp+ とやらが筋悪だっただけじゃないのか」 という声が聞こえてきそうです. ここまでの話だけでは, 確かにそう感じてしまうかもしれません.

しかし実は, …

(まだ. っていうか理解できてない. おそらく, S 式から論理式に翻訳し戻すと 「lisp を記述できるくらいにリッチな体系では, 常にこんな症状が生じる」 ということになって, 「我々が普段やっている数学でも, 実はそれくらいリッチな体系を常用している」 のような方向に行くんだと思うけど…)

感想

「ゲーデル数」を S 式におきかえると, 確かに話がぐっと身近になりますね (lisp を知っている人にとっては).

  • ゲーデル数を具体的に書いてみせることは実質無理だし, 書いても意味は見えない. S 式なら, やばい式 baz を具体的に書いて, 内容を読むことができる.
  • さらに, lisp の eval によって, やばさっぷり(の一部)を実際に実行して確かめられる.

という二点のおかげで, 「手が届く」感が高まります.


おわりに

くり返しますが, 講義口調や断定文にだまされないでください. あくまで「こういうことかなあ」というメモであって, 理解して書いているわけではありません.

特に, 次の点がわかっていません: ゲーデル数を使うふつうの証明での「自然数」の役割を 「S 式」に負わせている. それはいい. じゃあ, S 式の「eval」に対応するものは, ゲーデル数では何? 「S 式をエバると別の S 式が作られる」に対応して, 「ゲーデル数から別のゲーデル数を作る操作」があるのか? それとも, eval は S 式ならではの機能で, ゲーデル数には対応物はないのか?

他にも, 勘違いや考察不十分なところがきっとあるでしょう. 理解している方に教えていただければ幸いです.


付録: 即席インタプリタ

「やばい S 式」の組み立てに使った即席 metacircular interpreter のソース. Gauche 上で実行できます.

  • ラムダ式がそのまま表示される
  • いちいち funcall を書かなくてよい

という希望に合う lisp/scheme 処理系が手元になかったので, でっちあげました.


;;; 即席インタプリタと,
;;; それを使った不完全性定理の証明(…に出てくる「やばい S 式」の組み立て).
;;; gosh を起動して, 以下をそのままコピー&貼りつけで OK

;;; インタプリタ

(define (mc lis)
  (for-each (lambda (expr)
              (display (format "~a~%; ==> ~a~%" expr (mc1 expr))))
            lis))
(define (mc1 expr)
  (mc-eval expr *mc-global-env*))

(define (mc-eval expr env)
  (let ((proc (cond ((symbol? expr) mc-eval-symbol)
                    ((eq? (car expr) 'define) mc-eval-define)
                    ((eq? (car expr) 'lambda) mc-eval-lambda)
                    ((eq? (car expr) 'quote)  mc-eval-quote)
                    (else mc-eval-funcall))))
    (proc expr env)))

(define (mc-eval-symbol expr env)
  (mc-get expr env))
(define (mc-eval-define expr env)
  (let ((symbol (cadr expr))
        (val (mc-eval (caddr expr) env)))
    (mc-put! symbol val env)
    val))
(define (mc-eval-lambda expr env)
  expr) ;; 環境? 何それ :p
(define (mc-eval-quote expr env)
  (cadr expr))
(define (mc-eval-funcall expr env)
  (let ((func (mc-eval (car expr) env))
        (args (map (lambda (arg) (mc-eval arg env)) (cdr expr))))
    (mc-apply func args env)))

(define (mc-apply func args env)
  (cond ((procedure? func) (mc-apply-procedure func args env))
        (else (mc-apply-lambda func args env))))

(define (mc-apply-procedure func args env)
  (apply func args))
(define (mc-apply-lambda func args env)
  (let ((vars (cadr func))
        (body (caddr func))
        (local-env (mc-make-env env)))
    (for-each (lambda (v a) (mc-put! v a local-env)) vars args)
    (mc-eval body local-env)))

(define *mc-global-env* '(()))
(define (mc-make-env parent-env)
  (cons '() parent-env))
(define (mc-get symbol env)
  (cdr (assoc symbol (apply append env))))
(define (mc-put! symbol val env)
  (set-car! env (cons (cons symbol val) (car env))))

(for-each (lambda (p) (mc-put! (car p) (cdr p) *mc-global-env*))
          `((list . ,list) (equal? . ,equal?) (eval . ,mc1)))

;;; 動作確認

;(mc1 '(quote a))
;(mc1 '(define x 'a))
;(mc1 'x)
;(mc1 '(list 'b 'c))
;(mc1 '(lambda (x y) (list x y)))
;(mc1 '(define f (lambda (x y) (list x y))))
;(mc1 '(f 'b 'c))
;(mc1 '(equal? (list 'b 'c) (list 'b 'c)))
;(mc1 '(eval '(f 'b 'c)))

;;; 不完全性定理

(begin
  (newline) (display "---- begin mc-interpreter ----") (newline)
  (mc '(
        ;; 練習
        (define w (lambda (x) (list x x)))
        (w 'hoge)
        (define foo (w w))
        (equal? foo (eval foo))
        ;; 本番
        (define u (lambda (x) (list 'unprovable? x)))
        (u '(hoge fuga))
        (define uw (lambda (x) (u (w x))))
        (uw 'hoge)
        (define bar (w uw))
        (define baz (uw uw))
        ;; 確認
        (equal? baz (u bar))
        (equal? baz (eval bar))
        ((lambda (x) (u (w x))) (lambda (x) (u (w x))))
        ;; 補足
        (define not-baz (list 'not baz))
        ))
  (display "---- end mc-interpreter ----") (newline))

コメント



  • 2005-12-26 (月) 18:57:49 Anonymous : 途中見れてませんが、『S 式の「eval」に対応するものは, ゲーデル数では何? 』について、単に「自然数についての論理式に自然数(特にゲーデル数)を代入する」という操作なのでは?
  • 2005-12-26 (月) 19:02:27 Anonymous : 関連して、そもそもゲーデルの証明では、ここでいう「体系」として、述語論理+自然数(ペアノの公理系)を考えてます。で、その後、ω-無矛盾性のωはとれることが証明されているので、「lisp を記述できるくらいにリッチな体系では」という但し書きは実際には不要になるはず。
  • 2005-12-26 (月) 19:02:58 Anonymous : ただし古の記憶なので、↑は勘違いしている可能性あり。
  • thx. なるほど. 「2+2」のゲーデル数を「4」のゲーデル数に変換することが eval にあたるということですか.
  • 2005-12-27 (火) 09:16:17 Anonymous : むしろ、たとえば「2nは偶数」という命題のゲーデル数をnにぶち込む、という感じの操作かと。
  • 2005-12-27 (火) 09:22:30 Anonymous : (きちんと確認せずに記憶でコメントしてるんで、ノイズになってたらごめんなさい)
  • たぶん通じてる…と思います>むしろ. 「∀などを含まない『機械的に計算可能』な式 e」のゲーデル数 g から「その式の計算結果 e'」のゲーデル数 g' への mapping ηが, lisp の eval に相当. 不完全性定理の証明では, このηを使って「…ぶち込む」みたいな操作を構成. ミソは, (1)「機械的」なおかげで「η(g) = g'」が証明可能なこと, (2)「○○は××の証明列である」のゲーデル数がηの定義域に属すこと. という位置づけを想像しています.
  • もしかして, 元ネタのコードが「わざわざクオートしといて結局 eval」っていうまどろっこしいスタイルなのは, eval をどこで使ってるのか陽に示すためなのかな…

(Please LogIn to post comments.)

Last modified:2010/11/12 19:51:03
Keyword(s):
References:[なんでも] [不完全性定理.改]

*1 「a→b」は, 「(¬a)∨b」を単に略記したものです. つまり, (define (imply a b) (or (not a) b)). なお, 評価順の問題までは気が回っていません.

*2 「∃x p(x)」は, 「¬(∀x ¬p(x))」を単に略記したものです. つまり, (define (exist? p) (not (all? (lambda (x) (not (p x))))))

*3 このへん, よくわかってません.

*4 lisp+ じゃなくて lisp でできそうですよね? 確かめてないけど…

*5 …ということでいいのでしょうか? それとも, (define f (lambda (x) (eval+ z))) という例(eval+ は lisp+ での評価)をまじめに検討する必要があるでしょうか?

*6 このあたりからは, 数学と論理 のスライドを参考にさせていただきました.

*7 組み立て方は, 不完全性定理のLisp, Mathematicaによる記述ゲーデルの証明から丸ぱくり. その際, lisp としてより自然になるよう, 省ける quote は取り除きました.

*8 この段階では (unprovable? …) の評価はしていないため, lisp で実行可能です.

*9 …と思うんだけど未確認.

*10 …じゃないかと思う. たぶん. そもそも「体系」を明示していないから厳密な話はできるわけないんだけど.