キューネン「数学基礎論講義」感想（2/3）
前回（1章と2章の前半まで）は以下の記事。
今回は2章の残りと3章まで読んだ。時間が掛かった割りには進捗がよろしくない模様。
第II章 モデル理論と証明論（後半）
完全性定理の証明は地味で面倒だったが、この定理は然るべき定義をすれば然るに成り立つべき言明だと個人的に思う。ともあれ証明できたということは、モデル理論のスタートラインに立ったということになる。以下の節で各論を述べて、全体像を俯瞰するような構成になっていた。
13節：モデルを扱うにあたり、いつものように、二つのモデルが「等しい」ことを定義することから始める。これが初等的同値である。これに関連するのが公理系の完全性（全ての命題について真偽を決定するということ）で、ウォシュ・ヴォート条件を満たせば完全な公理系が得られる。モーリーの定理などは紹介のみ。最後にヴォート予想にも触れる。これはまだ未解決、熱い。
14節：等式理論を含む全称ホーン理論入門。群は自由群を関係で割ったものだが、その抽象化、というよりはモデル理論の言葉での定式化をどうするか、という話題。多項式環を作りたいなと思ったら、多項式の表現する文を全部集めて、等しいことが形式的に証明できるものを同一視すれば良い。大胆。
15節：普段の数学では新しい用語を次々と定義して論理を展開していくけど、それは許されるのか？ 何か変なものを加えることにならないのか？ といった疑問を解決するのが、公理系の定義による拡大。つまり定義を定義し、拡大が保守的である（拡大における証明が、元の公理系における証明に書き直せる）ことなどを示す。
16節：初等部分構造の話題。この節で示される2つのレーヴェンハイム・スコーレム・タルスキの定理はモデル理論の最初の頂であろう。可算と非可算には大きな隔たりがある、といった感じだけど未だにしっくりこないのは自分が無学なせい。応用として超準解析が挙げられてるけど記述は簡素。
17節：具体的なモデルを集合論の枠組みで作ろうとしたとき、モデル内で定義される概念と、モデル外で定義される概念は、明確に区別されなければならない。例えば体のゼロ元は集合論のゼロ（空集合）とは何ら関係が無い。これくらいなら分かり易いが、空元（モデル内で、を満たす
）が、空集合（宇宙
における
）と一致するかどうかは分からない。これでは困るので、各々の解釈が一致するような絶対性を持つモデルのクラスとして推移的モデルを導入する。もちろん全ての論理式に言えるわけではなくて、論理式も
というクラスに限定される。補題II.17.6は地味だが非常に重要な命題だと思う。
18節：CSTやPASなどZFC以外の集合論の簡単な紹介。普通の数学をやる分にはZFCまでは要らないといった話題など。分からん。というのは言い過ぎだけど、演習問題やファクトばかりで退屈。
19節：完全なおまけ。コンピュータでの自動推論についての簡単な解説がある。
第III章 数学の哲学
3章は、数理論理学の哲学的側面について述べられた短い章となっている。数学を哲学する上での立場には、プラトニズム、有限主義、形式主義という三つの立場があるそうだ。それぞれの立場において、数理論理学の命題がどのように解釈され意義付けられるのか、何を真とするのかが丁寧に述べられている。特に大事なのは2節の内容で、「フォーマルな論理の展開は二度されればならない」という言明はかみ砕いて理解する必要があると思う。自分もずっと誤解していた点ではあるが、基礎論は無から何かを生み出す理論ではない。必ずメタな論理、特に有限的な論理が前提にあって、その上に形式的な論理が構成される。ここで構成された論理もまた有限的なものではるが、この形式に依ってZFC等が記述できる。そしてZFCという枠組みの中で、もう一度、形式的な論理を再構成する。このような二段階の構成を経て、晴れて自由にモデル理論を含む通常の数学が展開できる。
誤植と思われるもの
110ページ定義I.14.18
は
でないと集合にならない。
172ページ1行目(6)
は
の誤植。
219ページ下から9行目
は
の誤植。
235ページ例II.17.5(5)
は
の誤植。
238ページ3行目
は
の誤植。
243ページ下から3行目、「公理がであることは」は何か変。
253ページ補題II.18.6(2)
は
の誤植。
278ページ4行目、「異論の余地なしであるは」は変。「～であるとは」等。
所感
次が最後の章であり、いよいよ不完全性定理に立ち入るので楽しみ。
Math Power 2017
キューネンの本を読む時間が増えてしまい（あとゲームのイベントとか）、ブログの更新が暫く滞ってしまっています。なんとかしなくては……。
数学の祭典、MATH POWER、今年はやらないのかなーと思ってたら普通に10月7日にやるみたいです。今年の耐久企画は正65537角形の作図だそうです。体育館借りるとかしないと無理なんじゃないかなぁ。
↓が公式サイト
↓がニコ生入口
映画「ダンケルク」を見てきた
クリストファー・ノーラン監督兼脚本による、第二次世界大戦のダイナモ作戦（ダンケルク撤退戦）を描いた作品「ダンケルク」を見てきた。迫力ある音響と、緊張感が常に張りつめているような演出で、あっという間の2時間だった。述べたいことは沢山ある一方で、まだ上手く言葉に纏められない感じだけど、感想を書いてみる。
まず言えるのは、物語の背景は本編中に一切描写されないので、ある程度前提知識を頭に入れておくべきだということだ。ダンケルクはフランスの北端、ベルギーとの国境付近に位置する港であり、そこに逃げ込んだイギリス及びフランスの連合軍をドイツ軍の包囲から救出するという歴史的事実に基づいたお話。救出作戦には膨大な数の民間船が徴用され、最終的には30万以上の兵士を救出することに成功した。作品では一隻の船（海）、及び一人の兵士（陸）、そして一人のパイロット（空）という三つの視点から、緊張感ある救出劇を描いている。
ちなみに史実だとフランス兵が数千名捕虜になってる。劇中でも言及されてるけどイギリス兵が優先されたのもありフランスは恨んでるらしい（ため息）。もっとも、ごっそり軍需品を放棄したのでイギリスはアメリカに財布を握られることになる。
さて、視聴後に気付いて驚いたのは、この作品ではドイツ兵の姿が直接的に全く描かれていないという点だ。無論、空戦（本作品の見所さん）では相手の機体にもちろん兵士はいるだろう。しかしその姿が全く見えない。激しい銃撃を受ける場面がある。しかし発砲音のみで敵の姿はどこにもない。あるいは潜水艦による魚雷攻撃で船が沈められる。やはり敵の姿はない。このように間接的に敵の存在を描くことで、いつ襲われるかもしれないという恐怖、緊張をずっと感じていた。
緊張感という点においては、音という情報も欠かせない。まず音楽は、全編に渡り時計の針が進むような音が込められている。焦燥感を煽られている印象を受ける。それと飛行機のエンジン音。船長のおじいさんが劇中で言及しているように、音で敵か味方かが分かる。ドイツ空軍が来れば不安な音が鳴り、味方が来れば頼もしく聞こえる。その音を印象付けるためか、台詞が少なく、また登場人物の個性も控えめになっていた。
基本的に雰囲気を楽しむような映画なので、スペクタクルを求めて見るのはお勧めしない。空戦は魅力的だったけど、緊張と弛緩を繰り返すという点ではむしろホラー映画に近い。音響に拘った作品なので、設備の整った映画館で見た方がずっと楽しめる作品だろう。見て損はない映画。
終盤、海から陸を眺める場面があったけど、あれはドーバーの白い断崖かな。
