不完全性定理の数式をなるべく使わない入門を作成中。公開済みこちら
今日は数学セミナー1月号の発刊日なので、昨日、送ってくれたものが着いたが、数式はそれより少ない位にする予定。
今はどうして不完全性定理は誤解されやすいか書いている。誤解しやすのは数理論理学の形式性・機械性を理解するのが難しいからだが、情報系の学生で形式言語処理などを行うプログラムを自分で作成したことがないと、これは中々理解できない。
実は、そういう私も論理学からコンピュータ・サイエンスに転向して、そういうソフトである PX system というものを作って、それまでの数理論理学者だったころの形式的体系の理解がザルのようで駄々洩れだったことに気がついて驚いたという経験がある。
それで、そういうことが良くわかるような情報系の数理露理学の講義の様な解説を書くことにしたのだが、そのために括弧の扱いをどうするか色々考えていて、実は気軽に書いてる推論規則
A A->B/B
もいい加減な書き方であることに気が付いて驚いた。
論理式の定義をするときには「AとBが論理式ならば(A)->(B)も論理式である」とか「AとBが論理式ならば(A->B)も論理式である」という風に括弧をつけまくるのだが、ということは、この規則を正確に書くとすると
A (A)->(B)/B
か
A (A->B)/B
でないといけない。
なんと、今まで気が付かなかった…。普通に書くように書くためには、メタ言語における括弧の省略の規則まで定義しないといけないことになる。それより、これらの二つの様に書いた方が形式性が強調されて良い様な気がしてきている。