日記（2022/2/6）長い記事を終えたので久々に肩の力を抜いて近況を書く_2（この回は日記というか読書）
5.『キューネン数学基礎論講義』
そして、また新しい数学の本を読み始めました。
『キューネン数学基礎論講義』です。
＊＊＊
この本のいいところは、形式主義的観点にのっとった論理学に基づいているところです。
20世紀前半、「数学を論理学で基礎づけたい」運動、ヒルベルト・プログラムのために考えられた、ヒルベルト流の数学的な形式主義というのがあります。
かなりラフな言い方になりますが、形式主義では、ある理論が無矛盾かどうかは、外から「別の理論によって」判定する、という戦術を採ります。
この、ある理論を外から判定するためのラフな理論を、「メタ理論」と言います。
＊＊＊
「理論の中だけで無矛盾かどうか判定できないのか？」
そこなんですよ。ここにうまくいく場合といかない場合があるんです。
全てうまくいくなら、形式主義は方便であって、究極的には要らなくなるのでしょう。
が、うまくいかない場合があるので、形式主義、未だに使わざるを得ない。
＊＊＊
平たく言うと、論理学に求められる性質として、
「証明できる推論は全部真偽が確定できる（健全性）」
「真偽が確定できる推論は全て証明可能である（完全性）」
というのがあるのです。
そりゃそうでない体系は、証明できても真偽は分からないし、真偽がはっきりしていてもなぜだか説明できないんだから、かなり困る。
（真偽以外の値を持つ論理学の話もありますが、気が遠くなるのでやめておきます。いつかは触れざるを得なくなるだろう）
＊＊＊
ゲーデルの完全性定理では、デファクトスタンダードの論理体系、一階述語論理が完全かつ健全であることが証明されました。
つまり、デファクトスタンダードの論理体系を使うなら、証明できるなら真偽は必ず分かるし、真偽が分かるものは全部なぜ真なのか、またはなぜ偽なのかを説明できる。
デファクトスタンダードの論理体系、安心して使える。
＊＊＊
が、ゲーデルの不完全性定理の方では、何らかの理論を説明するために、理論の中の語彙だけでは、理論の無矛盾について正当化できない（また、上の2つが成り立たなくなる）体系が存在することが証明されました。
具体的には、馴染み深い自然数論がそうです。
なので、「完全かつ健全な」ヒルベルト・プログラムの徹底というのは、実はできないのです。
ここがうまくいけば、メタ理論は全部要らなくなるかも知れなかったのですが、そうはならないので、方便であったはずのメタ理論の話からは逃げられなくなります。
＊＊＊
この本は、ほっとくと怪しげなものにしか見えないメタ理論の扱いについて、ある程度章と節を割いて、割としっかりと説明をしています。そういう意味ではとてもいい本ですね。
これを読破すればきっと、一時期の私みたいに
「理論の中の語彙だけで、理論の無矛盾について正当化できんか」
などという罠に、もう引っかからずに済む。
何でもかんでも
「これは何に基礎づけられているのか。そしてその行きつく先に在る究極のオブジェクトとは何か」
と考えたがる、基礎づけ中二病の私にとって、
「理論の中の語彙だけで、理論の無矛盾について正当化できんか。できないだとぉ！？」
となると、
「これを世間ではどう解決しているんだ？ まだ遡らなければならないのだろう。じゃあ、その遡った先の、メタ理論とは、一体何か？」
ということについて、説明が欲しくなる訳です。
これがうまく分かれば、基礎づけ中二病、なんかまだイケるんじゃないか？
＊＊＊
（メタ理論の妥当性はどこに由来するのか？ という問題が当然浮かんできますが、それもきっと書いてあることと期待しています。
もし、書いてなかった場合、おそらく数学の哲学者でもあったヴィトゲンシュタインの後期著作群、『哲学探究』をやらざるを得なくなるはずです。
おそらく『哲学探究』は、
「メタ理論は相互参照しまくってループしているものだ。
そして、メタ理論全体で妥当性が保証されていれば、理論の妥当性はあると認めてよい。
しかも、メタ理論は行為（説明として使い物になる）と価値（説明上の使い勝手が効率的であり幅広い範囲をカバーできる）で恣意的に作ってよい。
だから、メタ理論の基礎は「使い物になる」「使い勝手が良い」という、「機能」に帰着することになるだろう。
機能は現にあったりなかったりするもので、これを究極存在と考えることは特に妨げられない。
あるいは、機能のさらに先があるとしたら、そこの説明も、聞きたくないか？」
という話をしているのではないかと考えられるので、その辺当たってみたいところですね）
＊＊＊
あと、数学基礎論のデファクトスタンダードであるZFC集合論を学ぶのにも、とてもいい本です。
ただし、「集合存在公理」と「内包公理」という、今流通しているZFC公理系にはふつう含まれていないものも、便宜上含まれています。
また、「言及の範囲」「宇宙」「万有集合」「万有クラス」と呼ばれる（おそらく全部同じ意味）、存在はできないが仮定されたなんかの話が、集合論の抜きがたい一部として出てきます。
読んでいる限り、使われている理由はよく分かるし、便利であるとも認められるので、そういうものだと思って受け入れています。
私は彌永昌吉・彌永健一『集合と位相』Iから入ったし、これも集合論の導入にはいい本なのですが、たぶんキューネン本の方が平易です。
（とはいえ彌永昌吉・彌永健一『集合と位相』Iの価値を損ねるものではない）
6.一太郎Padで超高速OCR読書行為
さて、今回の読書では、AndroidやiPadで使えるアプリ、『一太郎Pad』に非常に助けられました。
ブックスタンドに本を立てて、十数分間、各ページの写真を撮る（少し位置合わせに癖があるが、何度か試行錯誤して慣れていく）。
文字列が文字データに変換される（OCR技術）。
誤字脱字もあるので、結局そこは紙の本を見ながら直さなければならないのですが、全部写経めいて手でデータ入力するよりはるかに早い。
＊＊＊
何せ、手でベタ打ちをすると、ガチでやったら数日間、数週間、場合によっては数ヶ月間かかるんだからな。
一太郎Padだと十数分、多くても数時間。
となると、これは格段の差だ。
この前、3年間かかりで読み終えた本があったが、これがあったら1年もかからず終わってたかもしれないな。もったいないことをした（まーしょーがねー）。
＊＊＊
こうして出来た文字データは、要約の際に非常に使い勝手が良くなる。
具体的には、全データをEvernoteに複写して（これも十数分かかる。が、手でデータ入力するあの非効率的な時間を考えれば、お釣りがくるくらいだ）、「原本」から「要約用」を複写して、「要約用」を縦横無尽に使う。ということになります。
紙の本はもちろん何かあると参照することになるのですが（特に図が載っている時は紙の本に頼らざるを得ない。また、誤字脱字を完全に取り切れている保証はいつだってないのだから）、とにかく作業はとてつもなく楽になります。
体感的には、「数学本の要約において、3倍程度の効率向上が見られた」という手ごたえです。
ただでさえ時間がかかる数学本の要約を、1/3の時間で片付けられるのなら、これほど嬉しいことはない。
＊＊＊
読み飛ばすところがあまりない数学の教本などを、丹念に読んで要約するには、一太郎Pad、たいへん強烈な効果があります。オススメです。
（続く）
（日記ではなく読書感想文とアプリ紹介記事なのでは？ 俺は訝しんだ）
いいなと思ったら応援しよう！
