17
$\begingroup$

As far as I know, whether Fermat's Last Theorem is provable in Peano Arithmetic is an open problem. What is known about this problem?

In particular, what is known about the arithmetic systems $PA + \text{Fermat's Last Theorem}$ and $PA + \lnot \text{Fermat's Last Theorem}$?

Note in particular that if $PA \vdash \text{Fermat's Last Theorem}$, the first system will just be $PA$ and the second system with be inconsistent. If FLT is independent of PA, then both will be consistient systems distinct from $PA$. $PA \vdash \lnot \text{Fermat's Last Theorem}$ is not possible, since $PA$ and Fermat's last theorem are both true in $\mathbb N$.

Improve this question
$\endgroup$
2
  • 9
    $\begingroup$ Here's a lower bound, of sorts: arxiv.org/abs/1602.03580 gives a very weak theory of arithmetic with a model where FLT cannot be proven. $\endgroup$
    – David Roberts ♦
    Commented Feb 15, 2018 at 5:50
  • $\begingroup$ Alternatively, $PA \vdash \lnot FLT$ is not possible because whatever can be proven in PA can be proven in ZFC, so we would get $ZFC \vdash \lnot FLT,$ implying ZFC is inconsistent, in which case we have much bigger problems to worry about. $\endgroup$
    – Display name
    Commented Aug 7, 2020 at 11:38

1 Answer 1

Reset to default
29
$\begingroup$

The main reference for this topic is Angus Macintyre's appendix to Chapter 1 ("The Impact of Gödel's Incompleteness Theorems on Mathematics") of Kurt Gödel and the Foundations of Mathematics: Horizons of Truth (Cambridge University Press, 2011).

There are a a couple of reasons why one might wonder whether the proof of FLT can be formalized in PA.

  1. The modularity theorem, as well as various arguments in the proof of the modularity theorem, appears at first glance to quantify over higher-order structures (sets of integers, sets of sets of integers, etc.), and so one might wonder whether all the necessary concepts can even be stated in the first-order language of arithmetic.

  2. Even if the modularity theorem and all other crucial intermediate statements along the way to FLT can be formulated arithmetically, there is no a priori guarantee that we don't need to appeal to axioms with greater logical strength than PA.

The "mathematician in the street" is typically more worried about #2. After all, doesn't the proof of FLT use all kinds of fancy-shmancy high-powered mathematics, and isn't PA "elementary"? Maybe one needs powerful axioms to carry out all those "advanced" arguments. While this is a theoretical possibility, there isn't any hint in the proof of FLT that strong axioms are needed. Experts can "smell" the intrusion of a strong axiom from a long way off; for example, the primary reason that the Robertson–Seymour graph minor theorem requires more than PA is that it invokes a highly sophisticated argument by induction at a crucial point. The proof of FLT doesn't give off this sort of odor anywhere. Of course, a smell test is not a proof, but the smart money is that if we run into difficulties trying to prove FLT in PA, it won't be because we need some strong arithmetic axiom. For more on this topic, especially the oft-discussed axiom of universes, see Colin McLarty's 2010 paper in the Bulletin of Symbolic Logic as well as his more recent arXiv preprint.

Issue #1, of whether all the higher-order apparatus in which the proof of FLT is couched is intrinsically necessary, is what Macintyre mainly concerns himself with. His appendix is essentially a ten-page sketch of an argument that all the relevant concepts and intermediate results on the road towards proving FLT can be replaced by "finite approximations" using standard techniques. As Macintyre says,

There is no possibility of giving a detailed account in a few pages. I hope nevertheless that the present account will convince all except professional skeptics that [the modularity theorem] is really $\Pi_0^1$.

In short, to say that it is an "open problem" whether FLT is provable in PA, while technically correct, is somewhat misleading. Demonstrating in full detail that FLT is a theorem of PA is more akin to an engineering project, where we more or less know how to proceed and are pretty sure—though of course not mathematically certain—that the project can be carried out if we just work hard enough at it.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ So, its a strongly believed conjecture that PA proves FLT, but no one cares enough to try and prove it, right? $\endgroup$
    – Christopher King
    Commented Feb 16, 2018 at 2:49
  • 3
    $\begingroup$ I don't think it is a matter of caring enough. Formalizing current well understood parts of mathematics into a version that is verifiable by a mechanical proof checker is something many care about, yet it is apparent that many mathematician hours (my guess is at least a million, and Timothy can probably give a better estimate) are needed just to get to the point before one can start trying MacIntyre's development. Gerhard "It's A Long, Long Haul" Paseman, 2018.02.15. $\endgroup$
    – Gerhard Paseman
    Commented Feb 16, 2018 at 3:24
  • 5
    $\begingroup$ @PyRulez : You could put it that way, I guess, but again I would say that your way of phrasing it is a bit misleading. Suppose I said that it is a "strongly believed conjecture" that we can connect every community in the world to the Internet, so presumably the only reason it hasn't happened yet is that "nobody cares enough" to do it. That would be a strange thing to say, wouldn't it? People do care, and people even have a pretty good idea how to do it, but it's a large engineering project, and it takes a lot of time and effort. $\endgroup$
    – Timothy Chow
    Commented Feb 16, 2018 at 3:53
  • $\begingroup$ @TimothyChow, okay, maybe the idea that no one cares was an exaggeration, but there are many conjectures where we have a pretty good idea if they are true or not. For example, we are pretty sure that P != NP, but its still a conjecture. $\endgroup$
    – Christopher King
    Commented Feb 16, 2018 at 4:02
  • 12
    $\begingroup$ @PyRulez : Again, I think you're operating with the implicit assumption that the only reason someone wouldn't prove something is because they don't have any idea how to do it. If they knew how to prove it then they would. But this mindset tacitly assumes that the only hard thing about producing a proof is figuring out how to do it. In other words, the "engineering" obstacles to actually carrying out the proof are relatively trivial. That assumption may work fine with problems like P != NP or the Riemann hypothesis, but it doesn't apply here. The engineering aspects are non-trivial. $\endgroup$
    – Timothy Chow
    Commented Feb 16, 2018 at 4:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .