Is Fermat's last theorem provable in Peano arithmetic?
Clash Royale CLAN TAG#URR8PPP
up vote
5
down vote
favorite
The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily only outside PA).
Compared to Fermat's last theorem $F$ which states that for $n>2, a, b, c in mathbbN$
$$a^n + b^n = c^n rightarrow a = 0 text or b = 0$$
it's hard to write $S$ down as a sentence of PA and understand its meaning. Nevertheless it's a (true) theorem of pure number theory, perfectly expressible in the language of PA. And for both $S$ and $F$ no proof inside PA is known. (For $S$ there cannot be one.)
My question is: Can it be shown (and/or how can be shown) that Fermat's last theorem has no proof in the language of Peano arithmetic?
This would imply that one must leave the realm of Peano arithmetic to prove it. As a side question: How would one - in general terms - name the realms in which Gödel and Wiles performed their proofs? "Model theory" and "algebraic geometry"?
number-theory diophantine-equations proof-theory incompleteness peano-axioms
asked Aug 20 at 8:39
Hans Stricker
4,34213574
 |Â
show 4 more comments
up vote
5
down vote
favorite
The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily only outside PA).
Compared to Fermat's last theorem $F$ which states that for $n>2, a, b, c in mathbbN$
$$a^n + b^n = c^n rightarrow a = 0 text or b = 0$$
it's hard to write $S$ down as a sentence of PA and understand its meaning. Nevertheless it's a (true) theorem of pure number theory, perfectly expressible in the language of PA. And for both $S$ and $F$ no proof inside PA is known. (For $S$ there cannot be one.)
My question is: Can it be shown (and/or how can be shown) that Fermat's last theorem has no proof in the language of Peano arithmetic?
This would imply that one must leave the realm of Peano arithmetic to prove it. As a side question: How would one - in general terms - name the realms in which Gödel and Wiles performed their proofs? "Model theory" and "algebraic geometry"?
number-theory diophantine-equations proof-theory incompleteness peano-axioms
asked Aug 20 at 8:39
Hans Stricker
4,34213574
3
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
1
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18
 |Â
show 4 more comments
up vote
5
down vote
favorite
up vote
5
down vote
favorite
The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily only outside PA).
Compared to Fermat's last theorem $F$ which states that for $n>2, a, b, c in mathbbN$
$$a^n + b^n = c^n rightarrow a = 0 text or b = 0$$
it's hard to write $S$ down as a sentence of PA and understand its meaning. Nevertheless it's a (true) theorem of pure number theory, perfectly expressible in the language of PA. And for both $S$ and $F$ no proof inside PA is known. (For $S$ there cannot be one.)
My question is: Can it be shown (and/or how can be shown) that Fermat's last theorem has no proof in the language of Peano arithmetic?
This would imply that one must leave the realm of Peano arithmetic to prove it. As a side question: How would one - in general terms - name the realms in which Gödel and Wiles performed their proofs? "Model theory" and "algebraic geometry"?
number-theory diophantine-equations proof-theory incompleteness peano-axioms
asked Aug 20 at 8:39
Hans Stricker
4,34213574
The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily only outside PA).
Compared to Fermat's last theorem $F$ which states that for $n>2, a, b, c in mathbbN$
$$a^n + b^n = c^n rightarrow a = 0 text or b = 0$$
it's hard to write $S$ down as a sentence of PA and understand its meaning. Nevertheless it's a (true) theorem of pure number theory, perfectly expressible in the language of PA. And for both $S$ and $F$ no proof inside PA is known. (For $S$ there cannot be one.)
My question is: Can it be shown (and/or how can be shown) that Fermat's last theorem has no proof in the language of Peano arithmetic?
This would imply that one must leave the realm of Peano arithmetic to prove it. As a side question: How would one - in general terms - name the realms in which Gödel and Wiles performed their proofs? "Model theory" and "algebraic geometry"?
number-theory diophantine-equations proof-theory incompleteness peano-axioms
asked Aug 20 at 8:39
Hans Stricker
4,34213574
edited Aug 20 at 8:55
asked Aug 20 at 8:39
Hans Stricker
4,34213574
asked Aug 20 at 8:39
Hans Stricker
4,34213574
asked Aug 20 at 8:39
Hans Stricker
4,34213574
4,34213574
3
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
1
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18
 |Â
show 4 more comments
3
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
1
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18
3
3
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
1
1
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18
 |Â
show 4 more comments
1 Answer
1
active
oldest
votes
up vote
6
down vote
This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.
Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA.
Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.
However, McLarty in this paper claims that in the proof of FLT:
[...] certainly much less than ZFC is used in principle, probably
nothing beyond PA, and perhaps much less than that.
[p. 359]
Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic.
He 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, which plays a key role in Wiles' proof] is really $Pi^0_1$ [p. 15].
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
6
down vote
This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.
Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA.
Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.
However, McLarty in this paper claims that in the proof of FLT:
[...] certainly much less than ZFC is used in principle, probably
nothing beyond PA, and perhaps much less than that.
[p. 359]
Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic.
He 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, which plays a key role in Wiles' proof] is really $Pi^0_1$ [p. 15].
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
add a comment |Â
up vote
6
down vote
This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.
Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA.
Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.
However, McLarty in this paper claims that in the proof of FLT:
[...] certainly much less than ZFC is used in principle, probably
nothing beyond PA, and perhaps much less than that.
[p. 359]
Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic.
He 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, which plays a key role in Wiles' proof] is really $Pi^0_1$ [p. 15].
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
add a comment |Â
up vote
6
down vote
up vote
6
down vote
This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.
Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA.
Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.
However, McLarty in this paper claims that in the proof of FLT:
[...] certainly much less than ZFC is used in principle, probably
nothing beyond PA, and perhaps much less than that.
[p. 359]
Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic.
He 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, which plays a key role in Wiles' proof] is really $Pi^0_1$ [p. 15].
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
This paper shows that Fermat's Last Theorem (FLT) is not provable in weak arithmetics, including theories where exponentiation is not definable from addition and multiplication; in particular, FLT is not provable in Presburger artithmetic extended with a natural set of axioms for exponentials.
Concerning Peano arithmetic (PA), as far as I know, there is no negative result and the problem is still open. Actually, one of the main issues whether the proof of FLT can be formalized in PA is that it relies on higher-order structures and a priori there is no evidence that they can be reformulated in first-order language of PA.
Moreover, even if all the necessary concepts can be stated in the first-order language of PA, Wiles' original proof of FLT uses set-theoretical assumptions unprovable in Zermelo-Fraenkel set theory with axiom of choice (ZFC, which is stronger than PA) and there is no a priori guarantee that we do not need axioms with greater strength than PA.
However, McLarty in this paper claims that in the proof of FLT:
[...] certainly much less than ZFC is used in principle, probably
nothing beyond PA, and perhaps much less than that.
[p. 359]
Macintyre in the appendix of his chapter of the book Kurt Gödel and the Foundations of Mathematics: Horizons of Truth proposed and sketched a project of formalizing Wiles's proof of FLT in Peano arithmetic.
He 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, which plays a key role in Wiles' proof] is really $Pi^0_1$ [p. 15].
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
edited Aug 20 at 10:25
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
answered Aug 20 at 10:09
Taroccoesbrocco
3,72651433
3,72651433
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
add a comment |Â
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
3
3
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
How would you even state FLT in the language of Presburger arithmetic?
– Henning Makholm
Aug 20 at 10:13
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
@HenningMakholm - Formally you're right, I preferred a slightly ambiguous phrase instead of a more precise but heavier one (I don't even know the level of knowledge of the author of the OP). All technical details are well explained in the introduction of the first paper I cited. I summarize them in my comment below.
– Taroccoesbrocco
Aug 20 at 10:40
1
1
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
@HenningMakholm - Roughly speaking, they deal with expansions $(mathcalB, e)$ of models of arithmetical theories in the language $L = (0, 1, +, ·, leq)$ by a binary function $e$ intended as an exponential ($e$ satisfies a certain natural set of axioms $Exp$). They construct a model $(mathcalB, e) models Th(mathbbN) + Exp$ and a substructure $(mathcalA, e)$ with $mathcalA models Pr$ (Presburger arithmetic) such that in both $(mathcalB, e)$ and $(mathcalA, e)$ FLT for $e$ is violated by cofinally many exponents.
– Taroccoesbrocco
Aug 20 at 10:41
add a comment |Â
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2888541%2fis-fermats-last-theorem-provable-in-peano-arithmetic%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
3
Surprisingly I cannot quickly find a duplicate, but a remark in this answer claims that "experts now believe that Wiles' proof can be converted mechanically into a proof over an incredibly weak system, even weaker than PA!"
– Henning Makholm
Aug 20 at 8:55
Gödel's sentence is undecidable in PA (but is true). Suppose you could similarly prove that $F$ is undecidable in PA. Then you would have shown it was true, as otherwise a counter-example would exist which contradicts undecidability.
– user1729
Aug 20 at 9:05
1
I don't understand the argument. How does it follow that $F$ is true from being undecidable? (This holds and is the meaning only of $S$.)
– Hans Stricker
Aug 20 at 9:13
(Forget that we know that $F$ is true.) Suppose $F$ was both undecidable in PA and false. As it is false there exists integers $a$, $b$ and $c$, and an $n>2$ such that $a^n+b^n=c^n$. We can find these integers. Hence we can prove that $F$ is false within PA, contradicting undecidability. Hence, if you that $F$ is undecidable within PA it follows that $F$ is true.
– user1729
Aug 20 at 9:16
But how can we find them? They may be arbitrarily large. Doesn't miss this the essence of provability? Or did I miss something?
– Hans Stricker
Aug 20 at 9:18