ZKセミナー・サロンコミュの数論・神々による審判090822

BBQにて久々に山崎・横山両氏（yy二神と名付けよう）と再会．口頭で質問，議論をし，アドバイスをもらった．

FLTがPAで証明可能であることは「まず当然」のことで，確認するだけの作業になるのでやる価値はあまりないだろう，ということでした．
その感覚の根拠は，大雑把に言うと，FLTがΠ^0_1という非常に単純な形の命題であることと，FLTの証明に特殊な操作は用いられていないだろう，ということのようです．
「特殊な操作」というのは，たぶん，抽象的な現代集合論で使われるようなテクニックを指すのでしょう．

で，もっと弱い体系でのFLTの証明可能性を追うのは面白そうだ，ということでした．
山崎先生は，IΣ_1で証明可能でないならば，PAにまで上げないと証明可能にならないのではないか，と直感的に予想していました（根拠はぼくには理解できませんでしたが）．
また，IΣ_1より弱い体系で証明できる可能性もありそうだ，ということでした．
このようなことを調べるなら，FLTの形の不定方程式に拘らないほうがいいかもしれない，とのことです．

実際，IΣ_1より弱い体系と（適当なベースセオリーにおいて）同値になる数学の命題を探す，という研究も行われているそうです（自分の考えていたことが価値のあることだったようで，嬉しい）．
例えば，

・D'aquinoは1980年代にフェルマーの小定理が，ある弱い計算体系（たしか，E_1論理式に対する帰納法？　E_1論理式というのは開論理式存在記号が1個だけついてるやつ？　曖昧ですまん）と同値であることを示したとか．

・Pell方程式の解の存在と，指数関数の全域性が同値になるとか．

そういう結果が出ているそうです．

他にも，一見，証明にΣ_1くらいの帰納法が必要に思える具体的な数学的命題はいくつかあるので，それらを分析するのは面白いかもしれません．
しかし，このくらい弱くなると，算術的階層がほとんど意味を持たなくなり，強さの尺度が煩雑になってしまうようです．
ぼくとしては，指数関数の値がないかもしれないくらいの弱いところは細かすぎて，いまのところあまり興味が持てない感じがします．
「現実的に計算可能か，指数時間，多項式時間」とか，あんまり興味ないんです．

次に，類体論についてですが，これは対象がかなり具体的な理論なので，数学自体が難しくとも，逆数学的な意味での抽象度はかなり低いのではないか，ということでした．
やるのであれば「すべて計算可能である」というつもりで取り組むべきでしょうが，成果が上がるかどうかは神々の雰囲気的に微妙です．
ただ，類体論自体を理解したい，という目標はあるので，ぼくとしては今後の一つの目標として持ち続けたいと思います．

逆代数に関しては，むしろ，もっと抽象的なもので，ただし，基本路線として（行列による計算などの）具体的な手法で進めているもの，を対象にするとよい，とのことでした．
例えば，ヒルベルトの不変式論などです．
実際，山崎先生はその古典的な部分については形式化を終え，もう少し進めて論文に仕上げるところだ，ということでした（ぼくの名前も共著で載せてもらえるということでした．うーん，なんか複雑な気分だ……）．
また，ネター環についても（下のほうのトピックにも書きましたが）エフェクティブ・ネター環という対象を導入し（このアイディアは計算可能代数からは自然に要請されるものでしょう），研究が進んでいるらしいです．