ZKセミナー・サロンコミュの数論セミナー第11回090623

ソースはwikipedia．やっぱ，でかいとこでできることしかわかってないぽい．

この（フェルマーの最終定理の）証明はスキームの圏などの現代的な代数幾何の構成をもちいている。これはノイマン・ベルナイス・ゲーデル流の集合論（NBG集合論）という、通常の集合に加えて類 (class) を考え、ただし集合に対する言明の真偽（証明可能性）はZFC集合論と同じになる（ZFCの保存的拡大という）ようにした枠組みで定義される。NBG集合論は本質的にはZFC集合論と同じもので、ZFC集合論に到達不能基数の存在公理を付け加えてグロタンディーク宇宙の構成を可能にしたもので置き換えられると考えられている。このことから最終定理の証明のために本当はどれだけの公理が必要なのかについては疑問が呈されてもいて、ZFCよりは弱い体系でも十分なのではないかと言われている。

n=3の場合，n=4の場合はIΣ_1で証明できる（でしょう．書き出すのが面倒だけど）．n=3の場合は√-3，つまり代数的整数が出てきますが，この辺は一階算術で表現できる（でしょう）から．

で，逆はどうなんだ？フェルマーの最終定理から帰納法を導くとか，想像がつかん．
Hajek-PudlukのPHPとINDの同値の部分，Hati...なんとかさんのDisguises of...なんとかが参考になりそう．

余談だが，一階算術ってどこまで表現力があるのかね（ここらへんはそうとう研究がすすんでるんでしょう）．本来自然数を表すための体系だけど，整数，有理数，代数的数と，コーディングしてやっていけちゃうんだよね．すごいよね．まさにmetamathematics of 1st order arithmeticだよね．

こんなんありました．やっぱ世界には同じようなこと考える人がいるんですね！

FOM: Number theory and elementary arithmetic
Jeremy Avigad
Fri Jun 7 14:22:33 EDT 2002
A few weeks ago Harvey Friedman brought to my attention a posting by Matt
Frank (reproduced below) and prompted me to finish revising a draft of a
paper that is relevant to the posting. I have done so; it is called
"Number theory and elementary arithmetic," and it is posted on my web
page, http://www.andrew.cmu.edu/~avigad, under "surveys".

In this paper, I discuss Friedman's conjecture that FLT is derivable in
elementary arithmetic. Of course, there is little clear sense that one can
ascribe to notions like the "likelihood" that such a conjecture is true;
instead, I focus on explaining what can be done in elementary arithmetic
and conservative extensions, and how.

The short story is that Matt is absolutely right: one can carry out a
surprising amount of analysis in restricted fragments of arithmetic, but
we are a long way from having a sense as to whether one can
handle the kind of machinery that went into the proof of FLT.

In the paper I also try to clarify some general issues related to
Friedman's conjecture. One issue (that has, I think, befuddled past FOM
exchanges) has to do with varying senses of the word "need".

One sense of the word "need" is nicely captured by formal notions of
derivability. For example, if FLT is derivable in elementary arithmetic,
one might say that this shows that the proof of Fermat's last theorem does
not "need" infinitary notions.

But there is also vaguer (albeit no less interesting) sense of the word
"need". One might argue that even if FLT is derivable in elementary
arithmetic, such an elementary proof may really encode analytic or
infinitary notions, which are in fact "needed" to make the proof
understandable. It seems to me that neither formal logic nor the
philosophy of mathematics currently has a clear methodology for making
sense of this latter notion of necessity, or even the claim that analytic
or infinitary methods can be *useful* in proofs of number theoretic
statements. We can point to notions like length of proof; but while the
length of formal derivations certainly has something to do with it, it is
a fairly crude measure, and unlikely to provide much real insight.

Jeremy Avigad

（つづき）
Here is Matt Frank's posting (from May 10):

> On Tue, 30 Apr 2002, wiman lucas raymond wrote:
>
> > Wiles's proof of Fermat's last theorem has been pretty much accepted by
> > the experts in his field. His proof, however, uses very powerful
> > techniques in arithmetic algebraic geometry. Is is possible to
> > translate his proof into a strictly Peano arithmetic version, or is
> > this still an open question?
>
> I'm surprised no one has responded to this. Here's my impression of the
> state of things:
>
> The current proof of Fermat's last theorem appears to be predicative. For
> predicative systems like Feferman's (higher-order) or ACA_0 (second-order)
> there are procedures for translating proofs of arithmetic statements into
> proofs in Peano Arithmetic.
>
> So the real question is the predicativity of the proof. Knowledgeable
> mathematicians say that the proof does not rely crucially on discontinuous
> functions (this according to something I heard from Harvey Friedman, who
> interviewed some such mathematicians on this question). Since the
> mathematics of continuous functions is predicative, this is good evidence
> for the predicativity of the proof. On the other hand, the proof is still
> so long and hard to understand that it is hard to be confident of these
> claims.
>
> Harvey Friedman has made the conjecture that Fermat's last theorem is
> provable not just in Peano arithmetic but in the weaker system of
> exponential function arithmetic (whose provably total functions are
> bounded by towers of exponentials).
>
> A good comparison for all this is the complex-analytic proof of the Prime
> Number Theorem, and Takeuti's demonstration (in Two Applications of Logic
> to Mathematics) of how to reduce it to Peano arithmetic. If and when the
> algebraic geometry proving Fermat's Last Theorem becomes as well exposited
> and well known as the complex analysis proving the Prime Number Theorem,
> we presumably will be similarly confident that the proof of Fermat's Last
> Theorem can be rendered in Peano arithmetic. However, the wait promises
> to be long for that algebraic geometry to become so well known.
>
> --Matt
http://cs.nyu.edu/pipermail/fom/2002-June/005582.html

こんなんありました．

OXFORD UNIVERSITY COMPUTING LABORATORY

The issues around proving Fermat's Last Theorem in Peano Arithmetic (Joint with Logic Seminar of Maths Department)
Angus MacIntyre (School of Mathematics, Queen Mary University of London)

date
5th December 2008 (week 8, Michaelmas Term 2008)

abstract
I will outline the proof that Wiles's proof of Fermat's Last theorem can be done in first-order Peano arithmetic, and discuss the significance of such results. Some attention will be given to dissenting views which have appeared on the site FOM.
http://web.comlab.ox.ac.uk/seminars/128.html

いろいろでてくるな．

From: ENAYAT@american.edu
Newsgroups: sci.math.research
Subject: Re: [Q] Is proof of Fermat's Last Theorem within Peano Arithmetic?
Date: Sat, 06 Jun 98 16:39:41 EDT

In article <3576B90A.771C@win.tue.nl>
Tom Verhoeff <wstomv@win.tue.nl> writes:

>
>Is the (current) proof of Fermat's Last Theorem (FLT) by Wiles et al.,
>and subsequently simplified by others (?), a proof (that can,
>in principle, be reduced to a proof) from the axioms of Peano Arithmetic
>(PA) for natural numbers?
>
Your question is on many people's minds, and the answer seems to be unknown.
Many suspect that the current proof cannot be carried out in PA, but
the definitive answer is yet to emerge. On a recent visit of Wiles to our
campus last month I asked him the same question, and he simply said that he
does not know whether PA can prove FLT, and I suspect the question struck him
(as it seems to strike many non-logicians) as one which is of limited interest.
Although most mathematicians know of the so-called Peano's axioms, they know of
it as what logicians refer to as a "second order theory", i.e., one which
is couched in a formal language allowing not only quantification over elements
of the domain of discourse, but also subsets of the domain of discourse. On
the other hand, what logicians commonly refer to as Peano Arithmetic, is the
"first order projection" of the second order theory, i.e., one in which the
second order axiom of induction is replaced by the so-called induction scheme,
which consists of a set of first order axioms asserting that any first order
definable subset which includes 0 and is closed under successor is equal to the
whole set of natural numbers. The logicians move to the first order theory is
motivated by the fact that first order logic is "complete", in the sense that
there is a set of axioms and rules of inference for which the concepts
"provable" and "true in all models" coincide, but as a consequence of Godel's
incompleteness theorem, no such proof system exists for full-second order
logic.

There is a first order theory, confusingly referred to as "second order number
theory", which "should" be able to accomodate the existing proof of FLT. There
is a brief discussion of this theory in H. Enderton's classic text " A
Mathematical Introduction to Logic", at the very last section of the text
entitled "Models of Analysis" (In this usage, Analysis = Second Order Number
Theory"). Of course second order number theory is subject to Godelian
incompleteness. The definitive text on the subject is "Subsystems of Second
Order Arithmetic", by Stephen Simpson of Pennsylvania State University,
which is scheduled to be appear in 1998 (by Springer-Verlag).

Ali Enayat
Dept. of Math. and Stats.
American University
Washington, D.C. 20016-8050
e-mail: enayat@american.edu
http://www.math.niu.edu/~rusin/known-math/98/peano_arith

もはやどこにでもありますね．

That x^n + y^n == z^n has no integer solutions for n > 2 was suggested by Pierre Fermat around 1665. Fermat proved this for n=4 around 1660; Leonhard Euler for n=3 around 1750. It was proved for n=5 and n=7 in the early 1800s. Then in 1847 Ernst Kummer used ideas of factoring with algebraic integers to prove it for all n<37. Extensions of this method gradually allowed more cases to be covered, and by the 1990s computers had effectively given proofs for all n up to several million. Meanwhile, many connections had been found between the general case and other areas of mathematics--notably the theory of elliptic curves. And finally around 1995, building on extensive work in number theory, Andrew Wiles managed to give a complete proof of the result. His proof is long and complicated, and relies on sophisticated ideas from many areas of mathematics. But while the statement of the proof makes extensive use of concepts from areas like set theory, it seems quite likely that in the end a version of it could be given purely in terms of Peano arithmetic. (By the 1970s it had for example been shown that many classic proofs with a similar character in analytic number theory could at least in principle be carried out purely in Peano arithmetic.)
http://www.wolframscience.com/nksonline/page-1166d-text?firstview=1

Professor Stephen A. Cook (Department of Computer Science, University of Toronto)
Lecture Note (Computability and Logic, Fall, 2008) http://www.cs.toronto.edu/~sacook/csc438h/
Notes pp96-108 Peano ArithmeticにFermat's Last Theorem (FLTと略) についてのコメントがある．

>We will introduce a standard set of axioms for the language L_A. The theory generated by these axioms is denoted PA and called Peano Arithmetic. Since PA is a sound, axiomatizable theory, it follows by the corollaries to Tarski’s Theorem that it is incomplete. Nevertheless, it appears to be strong enough to prove all of the standard results in the field of number theory (including such things as the prime number theorem, whose standard proofs use analysis). Even Andrew Wiles’ proof of Fermat’s Last Theorem has been claimed to be formalizable in PA.

>Observed fact: All standard theorems of number theory are in PA. Even Wiles’ 1995 proof of “Fermat’s Last Theorem” apparently can be formalized in PA. So famous open problems, such as Goldbach’s conjecture and the prime pair conjecture, can probably be either proved or disproved in PA. Goldbach’s conjecture can certainly be disproved in PA if it is false: just present and verify a counter example. (Is the same true for the prime pair conjecture?)

要約すると「WilesによるFLTの証明もPAで形式化することができると言われている，見たところはできるらしい」というところでしょうか．

FLT（のn=3や4の場合）からIΣ_1を出すのは，notIΣ_1の任意のモデルについてx^n+y^n=z^nを満たすx, y ,zが存在することを言えばいいってことだよな．出来るのか．やってる人いるのか．

Bruno Poizat, A course in model theory, 2000
http://books.google.co.jp/books?id=XUsXw0ubmgwC&pg=PA158&lpg=PA158&dq=peano+arithmetic+fermat+last+theorem&source=bl&ots=zkrLY_rfDz&sig=FhsFoWuCkqXJBsNrxgAa574BWOE&hl=ja&ei=J0ZFStb8JMmIkQXw-7W2Dw&sa=X&oi=book_result&ct=result&resnum=6

英語でおk．
まあ，だいたい，FLTを証明する代わりに，FLTが無矛盾であることを証明しようとしても難しさは変わらないよ，ってことぽ．

ていうか指数関数定義するのにIΣ_1要るんだっけ？

体系が弱いと，指数関数の定義はできるがトータリティの保証ができないんだった．
ていうかnが具体的な自然数のときは，FLTを書き下すのに指数関数必要ない．