Math Power 2017
キューネンの本を読む時間が増えてしまい（あとゲームのイベントとか）、ブログの更新が暫く滞ってしまっています。なんとかしなくては……。
数学の祭典、MATH POWER、今年はやらないのかなーと思ってたら普通に10月7日にやるみたいです。今年の耐久企画は正65537角形の作図だそうです。体育館借りるとかしないと無理なんじゃないかなぁ。
↓が公式サイト
↓がニコ生入口
映画「ダンケルク」を見てきた
クリストファー・ノーラン監督兼脚本による、第二次世界大戦のダイナモ作戦（ダンケルク撤退戦）を描いた作品「ダンケルク」を見てきた。迫力ある音響と、緊張感が常に張りつめているような演出で、あっという間の2時間だった。述べたいことは沢山ある一方で、まだ上手く言葉に纏められない感じだけど、感想を書いてみる。
まず言えるのは、物語の背景は本編中に一切描写されないので、ある程度前提知識を頭に入れておくべきだということだ。ダンケルクはフランスの北端、ベルギーとの国境付近に位置する港であり、そこに逃げ込んだイギリス及びフランスの連合軍をドイツ軍の包囲から救出するという歴史的事実に基づいたお話。救出作戦には膨大な数の民間船が徴用され、最終的には30万以上の兵士を救出することに成功した。作品では一隻の船（海）、及び一人の兵士（陸）、そして一人のパイロット（空）という三つの視点から、緊張感ある救出劇を描いている。
ちなみに史実だとフランス兵が数千名捕虜になってる。劇中でも言及されてるけどイギリス兵が優先されたのもありフランスは恨んでるらしい（ため息）。もっとも、ごっそり軍需品を放棄したのでイギリスはアメリカに財布を握られることになる。
さて、視聴後に気付いて驚いたのは、この作品ではドイツ兵の姿が直接的に全く描かれていないという点だ。無論、空戦（本作品の見所さん）では相手の機体にもちろん兵士はいるだろう。しかしその姿が全く見えない。激しい銃撃を受ける場面がある。しかし発砲音のみで敵の姿はどこにもない。あるいは潜水艦による魚雷攻撃で船が沈められる。やはり敵の姿はない。このように間接的に敵の存在を描くことで、いつ襲われるかもしれないという恐怖、緊張をずっと感じていた。
緊張感という点においては、音という情報も欠かせない。まず音楽は、全編に渡り時計の針が進むような音が込められている。焦燥感を煽られている印象を受ける。それと飛行機のエンジン音。船長のおじいさんが劇中で言及しているように、音で敵か味方かが分かる。ドイツ空軍が来れば不安な音が鳴り、味方が来れば頼もしく聞こえる。その音を印象付けるためか、台詞が少なく、また登場人物の個性も控えめになっていた。
基本的に雰囲気を楽しむような映画なので、スペクタクルを求めて見るのはお勧めしない。空戦は魅力的だったけど、緊張と弛緩を繰り返すという点ではむしろホラー映画に近い。音響に拘った作品なので、設備の整った映画館で見た方がずっと楽しめる作品だろう。見て損はない映画。
終盤、海から陸を眺める場面があったけど、あれはドーバーの白い断崖かな。
キューネン「数学基礎論講義」感想（途中）
本棚の肥やし崩し企画第二弾
一年以上前に買って放置してたので、ちゃんと読んでしまおうというお話。
基礎論が気になり眠れない件 『キューネン 数学基礎論講義』 - arXiv探訪
↑では、ざっと読んだとか書いたけど嘘。今回は丁寧に一行ずつ読み砕くことを目的としている。
全体的な印象
まずこの本は非常に丁寧な本だということだ。記述の正確さは当然のことながら、その精密さに驚く。随所に著者による注意が散りばめられ、何が重要なのかを示唆してくれる。またフォーマルとインフォーマルの区別が必ず文章の頭にあって、混乱がなるべく生じないように配慮があるのも嬉しい。一方で冗長と感じる部分もままある。特に邦訳特有の長回しが可読性をほんの少し、僅かながら下げていると言えなくもない。ただそれ以上に誤植が殆ど無いのが優秀。可読性について補足しておくと、「フォーマル」「インフォーマル」とか「セクション」「サブセクション」、「シンタックス」「セマンティクス」とかカタカナが原理上多くなってしまうとかいう程度の話。
著者のサイトは→なげやりアカデミア
第I章 集合論
一章の内容は公理的に集合論を展開することなのだが、一つづつ公理を増やしていく構成が面白い。併せて順序数や基数について一般的な理論が展開される。加えて、ここまで書くかと思うところまで書いてあるし、足りない部分は参考文献をしっかり挙げてくれるのが嬉しい。
個人的に一番大事だなと感じた部分は、「順序数上の原始再帰」だろう。ざっくり言えば関数の再帰的定義がwell-definedということだが、論理式のレベルで厳密に構成できるというのが偉大な点。証明もそこそこ込み入っていて、一つの山場という感じ。この定理があるから我々は数学することができるといっても過言ではないと思う。このような記述は普通の数学をやっているとあまり気にしない点なので貴重に感じた。
基数の節から重要な話が続くのだが、演習問題が増えるためか、結果として内容は比較的あっさりしている。一章が長くなり過ぎたことを懸念したのかもしれないが、難度の高い部分なのでもう少し詳しく述べて欲しかったかもしれない。やり過ぎても本書の目的からは遠ざかるのかもしれないけど。
第II章 モデル理論と証明論
前半はI章で得た集合論の結果を前提に、シンタックスとセマンティクスの間に成り立つ完全性定理を証明することが一つの山場となっている。まずはシンタックスで使う用語の定義から始まるのはどの本も同じだが、こちらは置き換え・割り当てについてかなり丁寧な記載がある。形式的な記号の列に解釈を与えてセマンティクスを議論するときに大事なのは真理値表。先にコンパクト性定理やレーヴェンハイム・スコーレムの定理などが紹介されている。形式証明は推論規則にモーダス・ポーネンスのみを採用するヒルベルト流だけど、全ての命題論理のトートロジーを公理に加えるなど、キューネンなりの工夫が加えられている。いずれにせよ動機や具体例などの記述は多く、細部に渡る配慮はI章と変わらない。完全性定理の証明も具体例から必要な要素を取り出して、それらを解決する形で構成されていて面白い。
ちなみに172ページの1行目
は
の誤植だろう。他にも誤植は二か所あるが、これらは著者のサイトに載っていた。
