Math Power 2017
キューネンの本を読む時間が増えてしまい(あとゲームのイベントとか)、ブログの更新が暫く滞ってしまっています。なんとかしなくては……。
数学の祭典、MATH POWER、今年はやらないのかなーと思ってたら普通に10月7日にやるみたいです。今年の耐久企画は正65537角形の作図だそうです。体育館借りるとかしないと無理なんじゃないかなぁ。
↓が公式サイト
↓がニコ生入口
キューネン「数学基礎論講義」感想(途中)
本棚の肥やし崩し企画第二弾
一年以上前に買って放置してたので、ちゃんと読んでしまおうというお話。
基礎論が気になり眠れない件 『キューネン 数学基礎論講義』 - arXiv探訪
↑では、ざっと読んだとか書いたけど嘘。今回は丁寧に一行ずつ読み砕くことを目的としている。
全体的な印象
まずこの本は非常に丁寧な本だということだ。記述の正確さは当然のことながら、その精密さに驚く。随所に著者による注意が散りばめられ、何が重要なのかを示唆してくれる。またフォーマルとインフォーマルの区別が必ず文章の頭にあって、混乱がなるべく生じないように配慮があるのも嬉しい。一方で冗長と感じる部分もままある。特に邦訳特有の長回しが可読性をほんの少し、僅かながら下げていると言えなくもない。ただそれ以上に誤植が殆ど無いのが優秀。可読性について補足しておくと、「フォーマル」「インフォーマル」とか「セクション」「サブセクション」、「シンタックス」「セマンティクス」とかカタカナが原理上多くなってしまうとかいう程度の話。
著者のサイトは→なげやりアカデミア
第I章 集合論
一章の内容は公理的に集合論を展開することなのだが、一つづつ公理を増やしていく構成が面白い。併せて順序数や基数について一般的な理論が展開される。加えて、ここまで書くかと思うところまで書いてあるし、足りない部分は参考文献をしっかり挙げてくれるのが嬉しい。
個人的に一番大事だなと感じた部分は、「順序数上の原始再帰」だろう。ざっくり言えば関数の再帰的定義がwell-definedということだが、論理式のレベルで厳密に構成できるというのが偉大な点。証明もそこそこ込み入っていて、一つの山場という感じ。この定理があるから我々は数学することができるといっても過言ではないと思う。このような記述は普通の数学をやっているとあまり気にしない点なので貴重に感じた。
基数の節から重要な話が続くのだが、演習問題が増えるためか、結果として内容は比較的あっさりしている。一章が長くなり過ぎたことを懸念したのかもしれないが、難度の高い部分なのでもう少し詳しく述べて欲しかったかもしれない。やり過ぎても本書の目的からは遠ざかるのかもしれないけど。
第II章 モデル理論と証明論
前半はI章で得た集合論の結果を前提に、シンタックスとセマンティクスの間に成り立つ完全性定理を証明することが一つの山場となっている。まずはシンタックスで使う用語の定義から始まるのはどの本も同じだが、こちらは置き換え・割り当てについてかなり丁寧な記載がある。形式的な記号の列に解釈を与えてセマンティクスを議論するときに大事なのは真理値表。先にコンパクト性定理やレーヴェンハイム・スコーレムの定理などが紹介されている。形式証明は推論規則にモーダス・ポーネンスのみを採用するヒルベルト流だけど、全ての命題論理のトートロジーを公理に加えるなど、キューネンなりの工夫が加えられている。いずれにせよ動機や具体例などの記述は多く、細部に渡る配慮はI章と変わらない。完全性定理の証明も具体例から必要な要素を取り出して、それらを解決する形で構成されていて面白い。
ちなみに172ページの1行目
は
の誤植だろう。他にも誤植は二か所あるが、これらは著者のサイトに載っていた。
38.ブッフバーガーのアルゴリズム
用語とかもう少し整理した方が良いのかもしれない。以下はその変更案。
生成の記号は、全体空間がほぼ自明なのでで書く。
のによる割り算アルゴリズムの余り(remainder)をのによる簡約(reduction)と呼ぶ。特にがグレブナー基底なら、適当な組による簡約をのによる簡約と呼ぶ。またをと書く。
-多項式と標準表示
多重指数に対し、と定める。
で定める。これはとの先頭項を打ち消し合うように「掛けて」揃えたものである。
例えばの-多項式は、のdeglex()では
となる。一方grevlexではが「降べき」の順だから、
となる。このように-多項式も項順序によって異なる。
次に多項式の標準表示を定義し、グレブナー基底の判定法を求めよう。
に対し、多項式のによる標準表示(standard representation)とは、 であってが成り立つものをいう。
つまり高次の項が打ち消し合うような表示は標準表示ではない。
定理 (標準表示による判定法) とする。が生成するイデアルに対し、以下は同値である。
(証明)がグレブナー基底なら、のによる簡約はゼロとなり、従っての標準表示を与える。
一方が標準表示を持てばと表せて、更にとなるが存在する。このときが成り立つので、つまりが成り立つ。この逆は明らかなのではのグレブナー基底である。
ブッフバーガーのアルゴリズム
BuchbergerはGrobnerの弟子であり、Grobner基底を初めて導入した偉い人。つまり師の名前を取って名付けたらしい。
定理 とする。が生成するイデアルに対し、以下は同値である。
以下の証明はHassettに依る。
(証明)以下と置く。をグレブナー基底とすれば、のによる簡約はゼロとなる。従ってと表せる。特にが成り立つ。ところでとすればの定義は最高次の項を打ち消し合って出来るのでが成り立つ。これはLCM表示である。
-多項式達が上記の表示を持つとする。先の定理より任意のがの標準表示を持つことを示せば良い。そこで
と置く。だから項順序の整列性よりが存在する。これが等号となることを示せば良い。を取る表示を取り、更にとなるの個数が最小の個となる表示を取る。を仮定する。の元を並び替えて、ならとしてよい。特によりとなることに注意する。さてとしよう。このとき
であり、が成り立つ。ここでより、は共にを割り切る。よってであり、と表せる。そこでと置き、上の式にを掛け、更ににを掛けたものを加えてについて解く。すると
と表せる。これをと置く。
まずであり、である。よってが成り立つ。同様にしてが分かる。またに対してはであり、に対してはも分かる。これはの最小性に反する。
以上で、与えられた生成元からグレブナー基底を構成する準備が整った。Buchbergerのアイディアは、生成元から得られる-多項式を加え続けることでグレブナー基底を得ようというものである。
定理 (Buchbergerのアルゴリズム) とする。をで生成されるイデアルとする。以下の手順は有限回で終了し、出力はのグレブナー基底となる。
- 入力はであり、出力はである。
- まずにを代入する。
- を考え、それをに加えたものをとする。
- 加えた多項式がないとき、つまりであればを出力する。そうでないときは上の操作を繰り返す。
(証明)-多項式達は何れもイデアルに属するから、定理より出力がのグレブナー基底となることは良い。のときであることを示そう。今、新たにが加わったとする。割り算アルゴリズムよりである。ところがよりである。もし真の増大列が存在すれば、はネーター環であるから上昇列は停留するはずなので矛盾する。
所感
-多項式の定義を掛け算のみで定義しようと思ったら最後の証明と合わなくなって意味が無くなった。なかなか簡潔に書けないものだなぁ。