Mixing
How can know if a proof technique can actually prove something? Specifically, induction
$begingroup$
Induction is an incredible tool to prove some propositions. Although it seems that these propositions require some level of simplicity for us to be able prove them using only induction. If we wanted, for example, to prove Fermat's last theorem using induction on the exponential, I think we would have a hard time.
Regardless of that, if $phi$ (n) is the statement:$n > 2$ $land$ $x^n + y^n = z^n$ has no natural solutions. Since Fermat's last theorem is now proved the statement: $phi (0)$ $ land $ $forall x(phi(x) implies phi(x+1))$ is trivially true. (trivially in the sense that it follows directly from Wile's proof of Fermat's last theorem). Then, using in the Induction Scheme, we can conclude that $forall x phi (x)$
So, the induction scheme over our statement is provable. But i doubt that anyone would ever be capable of proving Fermat's last theorem using only induction.
Is there a formalization of the concept of "proof technique"? Are there current theories which could, theoretically, prove that if a computer is programmed to only search for proofs using induction, it would never be capable of proving Fermat's last theorem?
I apologize if this question is too vague. If a moderator believes this question is not meant for this website, please delete this.
Edit: In my research I found some paper called "natural proofs", in which it shows that any proof using certain technique, directly related to a combinatorial property, would not be enough to prove that P != NP. But it seems to me, at least in my ignorance, that the proof is too connected with Complexity Theory, and I wouldn't know if we can generalize this for other methods of mathematics. Has this been done before?
logic induction computability proof-theory
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
$endgroup$
add a comment |
$begingroup$
Induction is an incredible tool to prove some propositions. Although it seems that these propositions require some level of simplicity for us to be able prove them using only induction. If we wanted, for example, to prove Fermat's last theorem using induction on the exponential, I think we would have a hard time.
Regardless of that, if $phi$ (n) is the statement:$n > 2$ $land$ $x^n + y^n = z^n$ has no natural solutions. Since Fermat's last theorem is now proved the statement: $phi (0)$ $ land $ $forall x(phi(x) implies phi(x+1))$ is trivially true. (trivially in the sense that it follows directly from Wile's proof of Fermat's last theorem). Then, using in the Induction Scheme, we can conclude that $forall x phi (x)$
So, the induction scheme over our statement is provable. But i doubt that anyone would ever be capable of proving Fermat's last theorem using only induction.
Is there a formalization of the concept of "proof technique"? Are there current theories which could, theoretically, prove that if a computer is programmed to only search for proofs using induction, it would never be capable of proving Fermat's last theorem?
I apologize if this question is too vague. If a moderator believes this question is not meant for this website, please delete this.
Edit: In my research I found some paper called "natural proofs", in which it shows that any proof using certain technique, directly related to a combinatorial property, would not be enough to prove that P != NP. But it seems to me, at least in my ignorance, that the proof is too connected with Complexity Theory, and I wouldn't know if we can generalize this for other methods of mathematics. Has this been done before?
logic induction computability proof-theory
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
$endgroup$
1
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32
add a comment |
$begingroup$
Induction is an incredible tool to prove some propositions. Although it seems that these propositions require some level of simplicity for us to be able prove them using only induction. If we wanted, for example, to prove Fermat's last theorem using induction on the exponential, I think we would have a hard time.
Regardless of that, if $phi$ (n) is the statement:$n > 2$ $land$ $x^n + y^n = z^n$ has no natural solutions. Since Fermat's last theorem is now proved the statement: $phi (0)$ $ land $ $forall x(phi(x) implies phi(x+1))$ is trivially true. (trivially in the sense that it follows directly from Wile's proof of Fermat's last theorem). Then, using in the Induction Scheme, we can conclude that $forall x phi (x)$
So, the induction scheme over our statement is provable. But i doubt that anyone would ever be capable of proving Fermat's last theorem using only induction.
Is there a formalization of the concept of "proof technique"? Are there current theories which could, theoretically, prove that if a computer is programmed to only search for proofs using induction, it would never be capable of proving Fermat's last theorem?
I apologize if this question is too vague. If a moderator believes this question is not meant for this website, please delete this.
Edit: In my research I found some paper called "natural proofs", in which it shows that any proof using certain technique, directly related to a combinatorial property, would not be enough to prove that P != NP. But it seems to me, at least in my ignorance, that the proof is too connected with Complexity Theory, and I wouldn't know if we can generalize this for other methods of mathematics. Has this been done before?
logic induction computability proof-theory
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
$endgroup$
Induction is an incredible tool to prove some propositions. Although it seems that these propositions require some level of simplicity for us to be able prove them using only induction. If we wanted, for example, to prove Fermat's last theorem using induction on the exponential, I think we would have a hard time.
Regardless of that, if $phi$ (n) is the statement:$n > 2$ $land$ $x^n + y^n = z^n$ has no natural solutions. Since Fermat's last theorem is now proved the statement: $phi (0)$ $ land $ $forall x(phi(x) implies phi(x+1))$ is trivially true. (trivially in the sense that it follows directly from Wile's proof of Fermat's last theorem). Then, using in the Induction Scheme, we can conclude that $forall x phi (x)$
So, the induction scheme over our statement is provable. But i doubt that anyone would ever be capable of proving Fermat's last theorem using only induction.
Is there a formalization of the concept of "proof technique"? Are there current theories which could, theoretically, prove that if a computer is programmed to only search for proofs using induction, it would never be capable of proving Fermat's last theorem?
I apologize if this question is too vague. If a moderator believes this question is not meant for this website, please delete this.
Edit: In my research I found some paper called "natural proofs", in which it shows that any proof using certain technique, directly related to a combinatorial property, would not be enough to prove that P != NP. But it seems to me, at least in my ignorance, that the proof is too connected with Complexity Theory, and I wouldn't know if we can generalize this for other methods of mathematics. Has this been done before?
logic induction computability proof-theory
logic induction computability proof-theory
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
edited Sep 18 '16 at 16:33
Martin Sleziak
44.7k8117272
44.7k8117272
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
asked Aug 1 '16 at 11:55
Victor ChavautyVictor Chavauty
1779
1779
1
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32
add a comment |
1
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32
1
1
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.)
$defnn{mathbb{N}}$
$deft#1{text{#1}}$
$defplace#1{,boxed{#1},}$
$defcode#1{underline{#1}}$
Meta-Reasoning
We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $nn$, and arithmetic constants $0,1 in nn$, and arithmetic operations $+,times$, such that $(nn,0,1,+,times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $nn$ is of the form "$1+1+cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.
Induction in general
Induction in the most general sense is the following inference rule:
Given any $1$-parameter sentence $P$ with one natural number parameter:
If you can deduce both of the following:
$P(0)$.
$forall n in nn ( P(n) to P(n+1) )$.
Then you can deduce:
$forall n in nn ( P(n) )$.
Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).
For example "$exists m in nn left( place{1} = 2m lor place{1} = 2m+1 right)$" is a $1$-parameter sentence where all the occurrences of "$place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:
If you can deduce both of the following:
$exists m in nn ( 0 = 2m lor 0 = 2m+1 )$.
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) to exists m in nn ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Then you can deduce:
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) )$.
Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.
Now Fermat's last theorem corresponds to the statement:
$forall n in nn ( t{FLT}(n) )$
where "$t{FLT}(n)$" denotes "$n > 2 to neg exists x,y,z in nn ( x > 0 land y > 0 land x^n+y^n=z^n )$".
Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):
$t{FLT}(0)$.
$forall n in nn ( t{FLT}(n) to t{FLT}(n+1) )$.
So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.
One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.
Induction in first-order PA
Since the language of PA only has $0,1,+,times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:
$P(0) land forall n ( P(n) to P(n+1) ) to forall n ( P(n) )$.
Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $nn$.
However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:
$exists m ( 0 = 2m lor 0 = 2m+1 )$.
$forall n ( exists m ( n = 2m lor n = 2m+1 ) to exists m ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Therefore PA can, by using one of the axioms in the induction schema, deduce:
$forall n ( exists m ( n = 2m lor n = 2m+1 ) )$.
It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.
This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$neg forall n ( exists m ( n = 2m lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.
Fermat's last theorem in weak arithmetic theories
The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):
PA$^-$ plus quantifier-free induction cannot prove "$t{FLT}(3)$".
where "$t^3$" is read as "$t times t times t$" [the language of PA cannot express exponentiation!].
$t{Th}(nn) + t{Exp}$ cannot prove "$forall n ( t{FLT}_e(n) )$"
where $t{Th}(nn)$ (the theory of $nn$) is the collection of all sentences satisfied by $nn$
and $e$ is a binary function symbol and $t{Exp}$ consists of the familiar laws of exponentiation
and $t{FLT}_e(n)$ is the same as $t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".
The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $t{exp}$ over PA such that for every $a,b,c in nn$ we have that $nn$ satisfies "$t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $t{exp}$.
The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:
? PA proves "$forall n ( n > 2 to neg exists x,y,z,p,q,r in nn ( x > 0 land y > 0$
$ land t{exp}(x,n,p) land t{exp}(y,n,q) land t{exp}(z,n,r) land p+q=r ) )$".
The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $nn$ and sequences from $nn$, then one might consider $t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $nn$, the above claim loses its meaning.
This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
$endgroup$
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
|
show 7 more comments
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f1877780%2fhow-can-know-if-a-proof-technique-can-actually-prove-something-specifically-in%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.)
$defnn{mathbb{N}}$
$deft#1{text{#1}}$
$defplace#1{,boxed{#1},}$
$defcode#1{underline{#1}}$
Meta-Reasoning
We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $nn$, and arithmetic constants $0,1 in nn$, and arithmetic operations $+,times$, such that $(nn,0,1,+,times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $nn$ is of the form "$1+1+cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.
Induction in general
Induction in the most general sense is the following inference rule:
Given any $1$-parameter sentence $P$ with one natural number parameter:
If you can deduce both of the following:
$P(0)$.
$forall n in nn ( P(n) to P(n+1) )$.
Then you can deduce:
$forall n in nn ( P(n) )$.
Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).
For example "$exists m in nn left( place{1} = 2m lor place{1} = 2m+1 right)$" is a $1$-parameter sentence where all the occurrences of "$place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:
If you can deduce both of the following:
$exists m in nn ( 0 = 2m lor 0 = 2m+1 )$.
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) to exists m in nn ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Then you can deduce:
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) )$.
Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.
Now Fermat's last theorem corresponds to the statement:
$forall n in nn ( t{FLT}(n) )$
where "$t{FLT}(n)$" denotes "$n > 2 to neg exists x,y,z in nn ( x > 0 land y > 0 land x^n+y^n=z^n )$".
Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):
$t{FLT}(0)$.
$forall n in nn ( t{FLT}(n) to t{FLT}(n+1) )$.
So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.
One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.
Induction in first-order PA
Since the language of PA only has $0,1,+,times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:
$P(0) land forall n ( P(n) to P(n+1) ) to forall n ( P(n) )$.
Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $nn$.
However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:
$exists m ( 0 = 2m lor 0 = 2m+1 )$.
$forall n ( exists m ( n = 2m lor n = 2m+1 ) to exists m ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Therefore PA can, by using one of the axioms in the induction schema, deduce:
$forall n ( exists m ( n = 2m lor n = 2m+1 ) )$.
It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.
This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$neg forall n ( exists m ( n = 2m lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.
Fermat's last theorem in weak arithmetic theories
The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):
PA$^-$ plus quantifier-free induction cannot prove "$t{FLT}(3)$".
where "$t^3$" is read as "$t times t times t$" [the language of PA cannot express exponentiation!].
$t{Th}(nn) + t{Exp}$ cannot prove "$forall n ( t{FLT}_e(n) )$"
where $t{Th}(nn)$ (the theory of $nn$) is the collection of all sentences satisfied by $nn$
and $e$ is a binary function symbol and $t{Exp}$ consists of the familiar laws of exponentiation
and $t{FLT}_e(n)$ is the same as $t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".
The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $t{exp}$ over PA such that for every $a,b,c in nn$ we have that $nn$ satisfies "$t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $t{exp}$.
The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:
? PA proves "$forall n ( n > 2 to neg exists x,y,z,p,q,r in nn ( x > 0 land y > 0$
$ land t{exp}(x,n,p) land t{exp}(y,n,q) land t{exp}(z,n,r) land p+q=r ) )$".
The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $nn$ and sequences from $nn$, then one might consider $t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $nn$, the above claim loses its meaning.
This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
$endgroup$
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
|
show 7 more comments
$begingroup$
Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.)
$defnn{mathbb{N}}$
$deft#1{text{#1}}$
$defplace#1{,boxed{#1},}$
$defcode#1{underline{#1}}$
Meta-Reasoning
We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $nn$, and arithmetic constants $0,1 in nn$, and arithmetic operations $+,times$, such that $(nn,0,1,+,times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $nn$ is of the form "$1+1+cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.
Induction in general
Induction in the most general sense is the following inference rule:
Given any $1$-parameter sentence $P$ with one natural number parameter:
If you can deduce both of the following:
$P(0)$.
$forall n in nn ( P(n) to P(n+1) )$.
Then you can deduce:
$forall n in nn ( P(n) )$.
Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).
For example "$exists m in nn left( place{1} = 2m lor place{1} = 2m+1 right)$" is a $1$-parameter sentence where all the occurrences of "$place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:
If you can deduce both of the following:
$exists m in nn ( 0 = 2m lor 0 = 2m+1 )$.
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) to exists m in nn ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Then you can deduce:
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) )$.
Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.
Now Fermat's last theorem corresponds to the statement:
$forall n in nn ( t{FLT}(n) )$
where "$t{FLT}(n)$" denotes "$n > 2 to neg exists x,y,z in nn ( x > 0 land y > 0 land x^n+y^n=z^n )$".
Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):
$t{FLT}(0)$.
$forall n in nn ( t{FLT}(n) to t{FLT}(n+1) )$.
So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.
One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.
Induction in first-order PA
Since the language of PA only has $0,1,+,times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:
$P(0) land forall n ( P(n) to P(n+1) ) to forall n ( P(n) )$.
Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $nn$.
However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:
$exists m ( 0 = 2m lor 0 = 2m+1 )$.
$forall n ( exists m ( n = 2m lor n = 2m+1 ) to exists m ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Therefore PA can, by using one of the axioms in the induction schema, deduce:
$forall n ( exists m ( n = 2m lor n = 2m+1 ) )$.
It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.
This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$neg forall n ( exists m ( n = 2m lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.
Fermat's last theorem in weak arithmetic theories
The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):
PA$^-$ plus quantifier-free induction cannot prove "$t{FLT}(3)$".
where "$t^3$" is read as "$t times t times t$" [the language of PA cannot express exponentiation!].
$t{Th}(nn) + t{Exp}$ cannot prove "$forall n ( t{FLT}_e(n) )$"
where $t{Th}(nn)$ (the theory of $nn$) is the collection of all sentences satisfied by $nn$
and $e$ is a binary function symbol and $t{Exp}$ consists of the familiar laws of exponentiation
and $t{FLT}_e(n)$ is the same as $t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".
The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $t{exp}$ over PA such that for every $a,b,c in nn$ we have that $nn$ satisfies "$t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $t{exp}$.
The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:
? PA proves "$forall n ( n > 2 to neg exists x,y,z,p,q,r in nn ( x > 0 land y > 0$
$ land t{exp}(x,n,p) land t{exp}(y,n,q) land t{exp}(z,n,r) land p+q=r ) )$".
The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $nn$ and sequences from $nn$, then one might consider $t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $nn$, the above claim loses its meaning.
This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
$endgroup$
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
|
show 7 more comments
$begingroup$
Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.)
$defnn{mathbb{N}}$
$deft#1{text{#1}}$
$defplace#1{,boxed{#1},}$
$defcode#1{underline{#1}}$
Meta-Reasoning
We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $nn$, and arithmetic constants $0,1 in nn$, and arithmetic operations $+,times$, such that $(nn,0,1,+,times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $nn$ is of the form "$1+1+cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.
Induction in general
Induction in the most general sense is the following inference rule:
Given any $1$-parameter sentence $P$ with one natural number parameter:
If you can deduce both of the following:
$P(0)$.
$forall n in nn ( P(n) to P(n+1) )$.
Then you can deduce:
$forall n in nn ( P(n) )$.
Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).
For example "$exists m in nn left( place{1} = 2m lor place{1} = 2m+1 right)$" is a $1$-parameter sentence where all the occurrences of "$place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:
If you can deduce both of the following:
$exists m in nn ( 0 = 2m lor 0 = 2m+1 )$.
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) to exists m in nn ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Then you can deduce:
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) )$.
Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.
Now Fermat's last theorem corresponds to the statement:
$forall n in nn ( t{FLT}(n) )$
where "$t{FLT}(n)$" denotes "$n > 2 to neg exists x,y,z in nn ( x > 0 land y > 0 land x^n+y^n=z^n )$".
Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):
$t{FLT}(0)$.
$forall n in nn ( t{FLT}(n) to t{FLT}(n+1) )$.
So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.
One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.
Induction in first-order PA
Since the language of PA only has $0,1,+,times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:
$P(0) land forall n ( P(n) to P(n+1) ) to forall n ( P(n) )$.
Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $nn$.
However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:
$exists m ( 0 = 2m lor 0 = 2m+1 )$.
$forall n ( exists m ( n = 2m lor n = 2m+1 ) to exists m ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Therefore PA can, by using one of the axioms in the induction schema, deduce:
$forall n ( exists m ( n = 2m lor n = 2m+1 ) )$.
It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.
This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$neg forall n ( exists m ( n = 2m lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.
Fermat's last theorem in weak arithmetic theories
The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):
PA$^-$ plus quantifier-free induction cannot prove "$t{FLT}(3)$".
where "$t^3$" is read as "$t times t times t$" [the language of PA cannot express exponentiation!].
$t{Th}(nn) + t{Exp}$ cannot prove "$forall n ( t{FLT}_e(n) )$"
where $t{Th}(nn)$ (the theory of $nn$) is the collection of all sentences satisfied by $nn$
and $e$ is a binary function symbol and $t{Exp}$ consists of the familiar laws of exponentiation
and $t{FLT}_e(n)$ is the same as $t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".
The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $t{exp}$ over PA such that for every $a,b,c in nn$ we have that $nn$ satisfies "$t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $t{exp}$.
The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:
? PA proves "$forall n ( n > 2 to neg exists x,y,z,p,q,r in nn ( x > 0 land y > 0$
$ land t{exp}(x,n,p) land t{exp}(y,n,q) land t{exp}(z,n,r) land p+q=r ) )$".
The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $nn$ and sequences from $nn$, then one might consider $t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $nn$, the above claim loses its meaning.
This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
$endgroup$
Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.)
$defnn{mathbb{N}}$
$deft#1{text{#1}}$
$defplace#1{,boxed{#1},}$
$defcode#1{underline{#1}}$
Meta-Reasoning
We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $nn$, and arithmetic constants $0,1 in nn$, and arithmetic operations $+,times$, such that $(nn,0,1,+,times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $nn$ is of the form "$1+1+cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.
Induction in general
Induction in the most general sense is the following inference rule:
Given any $1$-parameter sentence $P$ with one natural number parameter:
If you can deduce both of the following:
$P(0)$.
$forall n in nn ( P(n) to P(n+1) )$.
Then you can deduce:
$forall n in nn ( P(n) )$.
Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).
For example "$exists m in nn left( place{1} = 2m lor place{1} = 2m+1 right)$" is a $1$-parameter sentence where all the occurrences of "$place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:
If you can deduce both of the following:
$exists m in nn ( 0 = 2m lor 0 = 2m+1 )$.
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) to exists m in nn ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Then you can deduce:
$forall n in nn ( exists m in nn ( n = 2m lor n = 2m+1 ) )$.
Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.
Now Fermat's last theorem corresponds to the statement:
$forall n in nn ( t{FLT}(n) )$
where "$t{FLT}(n)$" denotes "$n > 2 to neg exists x,y,z in nn ( x > 0 land y > 0 land x^n+y^n=z^n )$".
Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):
$t{FLT}(0)$.
$forall n in nn ( t{FLT}(n) to t{FLT}(n+1) )$.
So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.
One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.
Induction in first-order PA
Since the language of PA only has $0,1,+,times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:
$P(0) land forall n ( P(n) to P(n+1) ) to forall n ( P(n) )$.
Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $nn$.
However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:
$exists m ( 0 = 2m lor 0 = 2m+1 )$.
$forall n ( exists m ( n = 2m lor n = 2m+1 ) to exists m ( n+1 = 2m lor n+1 = 2m+1 ) )$.
Therefore PA can, by using one of the axioms in the induction schema, deduce:
$forall n ( exists m ( n = 2m lor n = 2m+1 ) )$.
It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.
This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$neg forall n ( exists m ( n = 2m lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.
Fermat's last theorem in weak arithmetic theories
The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):
PA$^-$ plus quantifier-free induction cannot prove "$t{FLT}(3)$".
where "$t^3$" is read as "$t times t times t$" [the language of PA cannot express exponentiation!].
$t{Th}(nn) + t{Exp}$ cannot prove "$forall n ( t{FLT}_e(n) )$"
where $t{Th}(nn)$ (the theory of $nn$) is the collection of all sentences satisfied by $nn$
and $e$ is a binary function symbol and $t{Exp}$ consists of the familiar laws of exponentiation
and $t{FLT}_e(n)$ is the same as $t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".
The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $t{exp}$ over PA such that for every $a,b,c in nn$ we have that $nn$ satisfies "$t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $t{exp}$.
The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:
? PA proves "$forall n ( n > 2 to neg exists x,y,z,p,q,r in nn ( x > 0 land y > 0$
$ land t{exp}(x,n,p) land t{exp}(y,n,q) land t{exp}(z,n,r) land p+q=r ) )$".
The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $nn$ and sequences from $nn$, then one might consider $t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $nn$, the above claim loses its meaning.
This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
edited Jan 2 at 12:05
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
answered Aug 3 '16 at 18:02
user21820user21820
38.8k543153
38.8k543153
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
|
show 7 more comments
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
I'm not at all qualified to comment on the actual mathematics in the proof of Fermat's last theorem, so any more specific questions about them will need to be directed to the experts around here. =)
$endgroup$
– user21820
Aug 3 '16 at 18:03
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Amazing answer!
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:08
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
Regarding the power of PA: The paper asserts that it is widely believed that PA can prove FLT. But let us assume that is not the case, that PA is too weak to do so, So one question comes to mind: How well can first order logic, and PA describe current modern mathematics? It would be a shame if most of our current theorems cannot be proved in these weak systems. Wouldn't every undecidability proof be useless then? Suppose one could show that PA cannot prove FLT. And suppose someone proved that before Wile's result. That would be discouraging, and problematic after someone actually proved it.
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:15
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
So, why should i care when a conjecture is shown to be undecidable? It is easy to prove that the sin function is undefinable in the field of real numbers (R, 0, 1, +, *, <). Nevertheless, we use it all the time. So, suppose i said to you i proved that some famous conjecture is undecidable in R. That shouldn't mean that it is impossible to prove it, right? Even if i proved it to be independent of ZFC, is modern mathematics a direct result of ZFC? If not, then even "unprovable" conjectures could indeed be provable. Does FOL with ZFC or PA actually describe modern mathematics?
$endgroup$
– Victor Chavauty
Aug 4 '16 at 11:19
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
$begingroup$
@VictorChavauty: It is not a big deal if PA or even EFA is unable to prove some theorem of mathematics about the natural numbers, such as FLT. By Godel's incompletenes theorems, if you already accept the existence of the collection $nn$ of natural numbers and that every sentence over PA is either true or false about $nn$, and you accept basic properties of strings, then you must accept that every consistent extension S of PA (PA plus extra axioms) that has decidable proof validity cannot prove the sentence "Con(S)". [cont]
$endgroup$
– user21820
Aug 4 '16 at 11:33
|
show 7 more comments
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
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
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f1877780%2fhow-can-know-if-a-proof-technique-can-actually-prove-something-specifically-in%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
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
Required, but never shown
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
Required, but never shown
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
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
$begingroup$
Take a look at en.wikipedia.org/wiki/RE_(complexity). Any theorem can be converted to a set of all x where the theorem is true. For a given set, we examine which values can be proved to be members (true) in finite time, and which ones require infinitely long to test. Sets are classified by the complexity of their computability. We can also build latices of complexity by taking prior sets as assumptions. e.g. given that Fermat's theorem is true, what other truth sets become easier to calculate?
$endgroup$
– Gary Kibble
Aug 1 '16 at 12:10
$begingroup$
See also: Avoiding proof by induction
$endgroup$
– Martin Sleziak
Sep 18 '16 at 16:32