本の感想その001「コンピュータは数学者になれるのか？」

-数学基礎論から証明とプログラムの理論へ-

照井一成 著

以下メモみたいなもの．

コンピュータ数学なれるか本，形式系Qの導入まで読んだ．

ここまでの感想．

人口の数学者に対して「彼女」なのか．

有界論理式のうち，自由変数を含まないものを有界文と言う．有界文と有界論理式がごっちゃになってたので3分ぐらい定理1.2がわからなかった．

(∀i) 規則の重要性が古代ギリシャ人すごいとともに説明されているがわからない．「任意=>すべて」がわかってない．推論規則なので記号の上では理解できるが意味があんまりわからない．

わかったようなわからんような．

てきとーにとってきたxについてA(x)が成立するので∀x.A(x)です，は数学の証明でよくやるのでそれか．なんか意識してなかったかも．

Qの歴史的事情ってなんだろう．

以上p.44まで．

どっかに正解ないのか～って探したがなかった．

どんな関数ですか？って言われてこれは説明できるけど，一般にはよくわからなくなるので定義式のとおりですとしか言えなくなる．

アッカーマン関数とかは名前しか知らない．

寿司でやべーことになってたやつとかも知ってる．

PA⊦FLTかもしれないってまじか～（FLT：フェルマーの最終定理

⊦記号はどうやってだすのかわからんから

から取ってきた．なんていうんだろう？そもそもあってる？

"解析学"って2階ペアノ算術だったのか

つよつよ数学者をつくろうになってる

つよつよ数学者．「数理科学」でみたことあるな．

多分こいつ強いです

https://gyazo.com/3f30d2a154d57079500921e0e806e775

https://gyazo.com/abcacf1f127d69650e19cce6c78fedbd

「コンピュータは数学者になれるのか」読んでるけれど，前提として前原「記号論理入門」と戸田山「論理学をつくる」（半分）は頭におおよそ入ってます．

https://gyazo.com/b4019e08e650f9737d5ad0ea5eb08564

なくても読めるけれど練習問題数時間は証明図書いてます．もう昔の話だけれど．

よくわからないのだけれど，前原は上のような証明図のスタイルで戸田山さんま右の証明の書き方してた．その時によってかき分けてた．

どっちが一般的とかはわからない．上かなとは思う．

てきとーに出てきたやつを貼っただけで合ってるかは見てないです．

変なこと言ってたらおるうぇくんが指摘してくれるだろうと思っている．

上の画像については記号の定義がないので何も言えないですね．

雰囲気だけ．

twitter に証明図書いてくれる bot いたなあ．

算術とか算術的って言葉がわからない．

なんかもう10年前だから覚えてないけれど右側方式はあとから付け加えたりとかが出来なくてメンドーってなったきがする．

全く同じことやってるんだけれどまあ表現方法の良し悪し．

算術．なんか数学できる体系？みたいな．雰囲気．これで生きてきてしまった．

数学まではいかなくて算数でもいいよ

キューネンの和書2冊持ってるのでまあ大丈夫やろと思っている．

当然読もうとして買ったんだけれどどっかで止めてるんだよな．コンピュータ数学なれるか本読んだら読むのでどこで躓いたか言うことにするよ．

覚えてたら

高橋「計算論」はアホくさい理由で申し訳ないがプログラムとか出てきて証明を追うのが面倒になった．それだけだ．

今のところ，「コンピュータは数学者になれるのか」はいい本です．

厳密に定義するとまあまあ面倒なところを上手く省いて面白いところを伝えられている気がする．（前原「記号論理入門」，戸田山「論理学をつくる」で読んだ範囲では面倒だったので．論理式とか．）

とりあえず60ページまで読んだ．

きょうは雑な定義の元で⊦の使用例が見れて良かった．

似たようなやつに⊧みたいなのあるじゃないですか．あれの意味を雑で良いので知りたい．

この本で入門書読む準備はできるんじゃないかなと思う（期待している）．

itmz153（みーくん） — 昨日 20:59

コンピュータ数学なれるか本読んでしまおう。

いきなりわからん定理2.8。

たとえがわからん。

無限大学の合格発表で合格者はまあ有限時間内に発表されるから良いけれど不合格者にとっても不都合がわからん。

あー書いててわかってきたかも。

合格者もずーっと待たされるから不合格者と同じでは？って思ったけれど合格者はある時刻tが存在してその時刻で合格がわかるのに対して、不合格者はその否定だから不合格の時刻が存在しないのか。

それで苦情が来て合格者掲示板の隣に不合格者掲示板を配置を配置することで対応したのか。なるほどね。

それなら不合格者も不合格が決まる時刻が存在することはわかるから安心だね。

で定理2.8は計算課題Xを自然数の集合で表す。このとき

「Xは決定可能」⇔「Xとその補集合X^cはどちらも半決定可能」

だそうだ。ふーんって思うことにする。

このディオファントス方程式のやつってヒルベルトの第なんとか問題だったよね。10っぽい。

Wikipediaのディオファントス方程式のページ、キモいことしか書いてないな

俄には信じられん

ディオファントス方程式

ディオファントス方程式（ディオファントスほうていしき、Diophantine equation）とは、整係数多変数高次不定方程式である。文脈として、整数解や有理数解を問題にしたい場合に用いられる用語であり、主に数論の研究課題と考えられている。古代アレクサンドリアの数学者ディオファントスの著作『算術』で、その有理数解が研究されたのにちなんだ名称である。

ペル方程式まではわかる、楕円曲線きもちわるっ

105ページ注に解析機関って書いてあるけれど気になる。

数学者の能力を拡張していけば実数を扱えることは前に見たが実際扱えたところでどれだけ彼女はわかり得るのか？

106ページ。「ヒルベルトの23問題」出てきたね。まじかよ10問題が解かれたのって1970年！？最近じゃん。

なんで第3問題を取り上げたんだろう。なんか異質に見える。

日本語読んでました

第13問題おもしろそうじゃん

ヒルベルトの23の問題

ヒルベルトの23の問題（ヒルベルトの23のもんだい、英: Hilbert(’s) 23 problems）は、ドイツ人の数学者であるダフィット・ヒルベルトによりまとめられた、当時未解決だった23の数学問題である。ヒルベルト問題 (Hilbert(’s) problems) とも呼ばれる。

まだ明確には4つ未解決があるね

解決は肯定的解決ってことかな。

第17問題も気になる。

本に戻る

108ページの注釈なんだよ！？

「計算可能であることはラムダ定義可能なことである（従ってチューリング機械で計算可能なことである）」

がチャーチ・チューリングのテーゼ。（なんで「テーゼ」って言ってるの？）

あー忘れることか。難しそう。

110ページ。ノイマン型コンピュータがさらっと書いてある。よく言われることだがわからない。

119ページ。もうお腹いっぱいです。ロッサー化。

流石にこの辺までくると論理が追えない。

「自動定理証明」か。時間あるときに調べるよ。

133ページ最高だな。

IΣ_1氏・・・すごいんだかすごくないんだかわからなくなってきた。

（少なくとも初見で第二不完全性定理が理解できなかったので中高生以下ではある。）

論証の一つ一つはとても簡単なことはわかる。その作業がたいへんなのだ。

145ページ。超限の国の話。似たようなこと考えたことあるな。考えたことがあるだけ。

多重集合っていうのか。

定理3.3。「直感的には正しそうだが、数学であまり直感にばかり頼っていると、ときにしっぺ返しをくらうこともあるので、この定理についてはきっちりと証明を与えておきたい。」

はい・・・

アッカーマン関数は原始再帰的でない。きたな。まってたよ。

定理3.10。ようは整列可能定理。わかる実数気持ち悪すぎる。

そう言われると選択公理認めたくない気持ちもわかる（気がする）。

実数の部分集合全体の集合も気持ち悪すぎるんだよな。詳しくないけど。

164ページ。

「これを“数学における必要悪”と言ったら言い過ぎだろうか。」

だそうだ。私は専門家ではないので何も言えない立場だがそう言い得るぐらいなんだね。

順序数来た。本当にこの本のように書いてくれよ。正確ではないはわかるが普通の教科書だと意味分かんないんだよなあ。

ε_0とかいう“非常に小さな数”。名前からして小さそうなのにデカすぎだろ。だけど順序数世界ではイプシロンなんだろうなあ。

173ページ。ごめん。これ無量空処じゃんって思ってしまった。

累積帰納法。なんか解析接続みたいねって思った。思っただけ。

PAさんすげー（無矛盾性）論。ゲンツェンの立場のあり方で哲学論争になるのか・・・

192ページ。竹内の基本予想。

196ページ。身近すぎる話題で笑う。

2次ディオファントス方程式の可解性がNP完全であることを示すことは相当難しいらしい。

この本の著者説明うますぎない？

246ページあたり。わからなくなる。

覚えてる！2002年の素数判定はPに属するって証明。

『第2回P対NP世論調査』（Gasarch 2012）の存在に草。

初めてラムダ計算理解できたんだけど。（（この理解が何を意味するのかわからないが。）もちろん詳しくは専門書を読む必要がある。）

BHK解釈（ブラウワー・ハイティング・コルモゴロフ解釈）のコルモゴロフって乱流の理論で出てくるコルモゴロフさんとは違うよね？ってぐぐったらアンドレイ・コルモゴロフで同じ人だった。すごすぎ

自然演繹の証明図にラムダ項をぶちこんで頭がうおうおフィッシュライフ

カリー・ハワード対応って出版は1980年なの？！最近じゃん

型の力

302ページ。難しくなってきてわからない部分あり

証明支援系、触ってみようかな

文献一覧助かる

読了！

https://gyazo.com/a68399cf7ce0df2c6f75cdfda16604ad

世界が広がってわからないことが増えたがわくわくするな

勧めてくれたおるうぇくんありがとう。

この本で今までもやもやしてたところが結構解消されたんだが。

「型システム入門」読めるかもしれん。プログラミングの基礎の本、集合の教科書読んで順序数あたりからわからなかった人、数学基礎論のはじめで挫折した人は読んだほうが良い。入り口にはなる。

今年のベスト本かもしれん。