> Therefore, all basic claims are more or less false. We just do not know why they are false. The entire body of science and mathematics therefore does not rest on a set of true statements but on a set of difficult-to-prove-false statements. Disproving a claim may even require showing where we can find a bug in the successor function. This is seriously hard, but still possible, because we know that these bugs must exist.
We do NOT know that these bugs exist. Gödel has shown us that any useful formalization of mathematics (such as the commonly utilized Zermelo–Fraenkel "ZF" set theory) cannot prove its own consistency. However, that does not imply that it must be inconsistant.
The fact that thousands of mathematicians have used ZF for about a hundred years without finding a contradiction makes me confident that even if it's inconsistant, we should be able to patch it up easily enough. But honestly I don't expect that to happen.
In my opinion, Kurt Gödel's claim points to something that seems to go wrong in Alonzo Church's successor function. For the sake of the argument, let's call that a bug. It would take a serious amount of work to point out how that would affect Zermelo–Fraenkel.
> The fact that thousands of mathematicians have used ZF for about a hundred years without finding a contradiction makes me confident that even if it's inconsistant, we should be able to patch it up easily enough. But honestly I don't expect that to happen.
As an example of this, the Greeks assumed that every number was rational (actually, that any two numbers could be expressed as an integer multiple of some common unit). When they did prove that this was false, they re-worked math without it and found that (almost?) all of their other theorems still worked even without the assumption that all numbers were rational.
Instead try to write a program which proves that the limit sin(1/x) x->0 does not exist. (Remember proving that a single function doesn't work isn't enough. You have to prove no such function exists.)
I suspect that such program could revolve around showing that for any arbitrarily small number -- almostZero -- you can always find two smaller numbers x1,x2 as such that sin(1/x1) is smaller and sin(1/x2) is larger than sin(1/almostZero). The Popper-compliant claim could be: find me an almostZero for which the defeating function will be incapable of producing such x1 and x2. I am not sure about all of this, though. Unless you have investigated something very similar before, it takes time to investigate things like that.
I think it may be possible to phrase a claim for this.
for any almostZero, it is possible to find an integer m1, so that the m1.2.pi + pi/2 is greater than 1/almostZero and therefore for which sin(m1.2.pi+pi/2) =1; 1/(m1.2.pi + pi/2) will be smaller than 1/almostZero. It is also possible to find an integer m2, so that m2.pi+pi is greater than 1/almostZero and therefore for which sin(m2.pi+pi) =0; 1/(m2.pi+pi) will be smaller than 1/almostZero.
The claim: find me an almostZero for it is not possible to find such m1,m2.
This could be a possibility, but I haven't written the program yet ;-)
The original CH mapping, that is, "a proof is a program, the formula it proves is a type for the program" is quite hard to achieve because it tries to demonstrate that a particular statement is true. It is much easier to honestly fail in demonstrating that it is false.
I think the fact that I cant drop that article onto a computer and have it tell me if its correct highlights the problem the author is trying to make.
I was also under the impression that programs like Mathimatica enabled you to do this with mathematic equations. But I guess for many they would take a long time to prove.
I suppose a easy way to sum up the article is we have a mathematic symbol for infinity, yet we could never compute that on a compter as you could always add a value greater than zero.
The reason we can't drop the article into a computer and have it magically return "true" or "false" is because making computers that even have human intelligence is damn hard as it is, so until we can perfect language parsing and the like and then input millennia of collective mathematical knowledge (correctly, no less), we're not going to have any particular progress on that front.
What does this have to do with "flaws" in contemporary mathematics though? If you're trying to use this as an example of a flaw in anything, it would be the computer industry for not figuring out artificial intelligence, not the mathematics community. So, if this was the author's intention, then I think it's flawed right from the outset, but I don't think this was truly the author's intent. (For one thing, Curry-Howard correspondence is talking about lambda calculus, not what you think when you hear "computer" today.)
Really, the article's entire premise is predicated on extreme misunderstandings of Godel. For instance:
> In fact, Gödel's 1931 Second Incompleteness Theorem insists that it is strictly forbidden to ever claim the truth of any scientific or mathematical statement:
What? Where does it say that? It says (quoting the article here):
> For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.
If a theory includes a statement of its own consistency, then that theory is inconsistent. How does that imply that it is "strictly forbidden to ever claim the truth of any scientific or mathematical statement"? The honest answer is that it doesn't, not in the slightest. When it comes to mathematics, we're not saying the axioms are consistent, we're saying statements within this set of axioms are true. Are the axiomizations true? I don't know, but a lot of work has gone into these theories and so far they look pretty good. But at any rate, the author uses this theorem in a completely incorrect manner. He is right that we don't know if any of the various mathematical foundations are consistent, true, but as I said, so far everything looks pretty good.
Then he throws this bombshell:
> Given Gödel's First Incompleteness we already know that for any claim making use of basic arithmetic, counterexamples must exist.
What? How? Here's Godel's First Incompleteness Theorem, per Wikipedia:
> Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250)
How in the world does that say that "for any claim making use of basic arithmetic, counterexamples must exist." (Counterexamples of what, anyway? Basic arithmetic?) Actually, what the theorem says that you can't have a theory capable of expressing elementary arithmetic that is both consistent and complete. The both is the huge part. So far, for example, we think ZFC is consistent. We know it is not complete; see this: http://en.wikipedia.org/wiki/List_of_statements_undecidable_... . So, the idea that there "must exist counterexamples" (of what, I don't know) as per Godel's First Incompleteness Theorem is simply ridiculous. As a result, we don't know that there are "simply bugs" in the "successor function." As a result, the idea that "all basic claims are more or less false" is completely shot down. Needs better proof.
> The claim above is not Popper-compliant.
Why not? It's falsifiable, so it is. (If it were false, you would need simply to provide an extremely small epsilon and ask for the correspondingly large delta.) It gives the "appearance" of truth because it is indeed true -- relative to th...
> That sentence is essentially a rewording of an old-fashioned delta-epsilon proof. So, how does that indicate a flaw in contemporary mathematics at all?
The first flaw is that it is not a proof but only a reduction. The second flaw is that contemporary math does not make the slightest attempt at making its claims easier to verify. What is wrong with an invitation/challenge in the form of a program asking to show the claim wrong?
Contemporary math does not attempt to make its claims verifiable in the sense you describe, because it proves them. There might be a flaw in the proof itself (and there is active research in creating programs to check proofs).
Sometime proofs in math our of the form you describe. For example, the (most well known) proof that sqrt(2) is irrational is a challenge to find the simplist fraction of to intergers that equals sqrt(2). The proof then goes on to show that any possible response you can provide to the challege is false. Simmilarly, for any mathametical claim, if you can provide a single counter example then you have dissproven the claim. Not being able to provide a counter example does not prove the claim.
> Well, I have to insist that math does not prove a statement true.
Be careful to define your terms. Most people, including mathematicians, will insist that Euclid's prime theorem proves that there are an infinity of primes -- that the assertion is "true".
But it will always be possible to redefine "true" arbitrarily to reject any such claims, which partly explains philosophy's low standing among intellectual disciplines.
> It is never possible to prove a claim anyway.
You've shifted ground in your wording, and contradicted the idea of a mathematical proof. There really are mathematical proofs.
In general science, your claim is correct -- a theory cannot be proven true, only false. But in mathematics, proofs exist.
Math and science use exactly the same method of reducing their claims to their basic claims and backing those with a failed search for counterexamples. Consequently, all untruth is invariably always the result of the untruth hidden in the basic claims. The untruth in the basic claims obviously exists but it is sheer impossible to pinpoint precisely where exactly it is.
> Math and science use exactly the same method of reducing their claims to their basic claims and backing those with a failed search for counterexamples.
This is false. You're overlooking a very important difference between math and science. Science is empirical, which means any scientific theory can be overthrown by new evidence arising in nature. This is not true for mathematics -- once a conjecture becomes a theorem, it's irrevocable.
Your viewpoint is a philosophical one that fails to account for the key difference between math and science.
Probably worse than that. I simply refuse to make any such key difference between math and science. In my opinion, both math and science are empirical.
In what way is math empirical? If one wants to prove that 1+1=2, one does not take one apple, add another apple, and observe that one now has two apples. One defines:
x + 0 = x
x + successor(y) = successor(x) + y
1=successor(0)
2=successor(1)
One then takes the true true statement
1+1=1+1 | Identity
And finds:
1+successor(0)=1+1 | Definition of 1
successor(1) + 0 = 1+1 | Definition of +
2 + 0 = 1+1 | Definition of 2
2=1+1 | Definition of +
I made no observation to prove 1+1=2. What I do observe is that if we map the counting numbers to the count of how many apples I have, and we map the addition operation to combing to groups of apples, then the mathematical result is consistent with reality.
However, if we empirically discover that the mathematical result is not constitent with reality, than that does not mean that the math is wrong, it simply means that the reality does not behave in a way that corresponds to the math.
He goes from the statement
"For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent."
To "all basic claims are more or less false."
If we could actually prove that all claims were false, we would be in violation of the Incompletness theorum.
Not to mention the absurtidy of his conclusion. Proving a statement for a set of values you thought of is far more likely to be wrong than proving it with formal mathamatics.
I like your attempt. At least, it is meaningful. Only the domain of statements about facts can be verified with facts. The domain of statements about statements cannot. You have indeed correctly underlined that the rules governing scientific statements -- statements about statements -- cannot be scientific themselves.
>Not to mention the absurtidy of his conclusion. Proving a statement for a set of values you thought of is far more likely to be wrong than proving it with formal mathamatics.
This, if the program did fail all that's been proven is that that particular delta-epsilon function, the defeatEpsilon here, doesn't work. In order to prove that the function doesn't converge you have to prove there is no function which can satisfy the conditions.
(Luckily there are some theorems which make it so one only have to prove that two different sequences of the function converge to different values. But that's getting into Real Analysis which is a whole semester worth of explanations.)
It only disproves that the particular delta-epsilon function works though. That just proves that the proof writer wasn't clever enough to find a working d-e, not that there isn't a d-e.
Well, if there is such d-e, the person challenging the reduction should be able to supply it. Since it just a number, he should be able to supply that number to the program and trigger a failure.
If the program fails, it only proves that the chosen defeatEpsilon proof does not work. In order to prove that that their is no defeatEpsilon, you would need to run you program against every function of the Real->Real.
If your delta epsilon did work, you would need to test in for every delta>0.
You state:
"Gödel's 1931 Second Incompleteness Theorem insists that it is strictly forbidden to ever claim the truth of any scientific or mathematical statement"
That claim is false, therefore, the truth of that claim is equivilent to the truth of 'false'. Becuase your article is true iff all of the statements within it are true, and your article contains a statement which is false, then your entire article is false. Using this, we can 'reduce' the 'proof' of your into assert(false). I suspect that the parent is using 0 as an alias for false.
More generally, for any contemporary mathamatical proof, what you call a reduction, you can reduce the proof of the form you describe to either assert(true) xor assert(false), depending on what the mathametical proof/reduction shows.
The claim follows trivially from Gödel's Incompleteness. Claiming the truth of a theory amounts to extending it with a statement about its consistency, automatically making the whole inconsistent.
The whole point was that we were going to write a program and invite each other to find counterexamples for the statement proposed, so that we can finally stop the bullshit of ad-hominem arguments. I know it must be hard for you to switch but in the long term it will benefit you.
46 comments
[ 4.1 ms ] story [ 161 ms ] threadNo, a Popper-compliant claim must be falsifiable. It does not need to be phrased in any particular way.
> Therefore, all basic claims are more or less false. We just do not know why they are false. The entire body of science and mathematics therefore does not rest on a set of true statements but on a set of difficult-to-prove-false statements. Disproving a claim may even require showing where we can find a bug in the successor function. This is seriously hard, but still possible, because we know that these bugs must exist.
We do NOT know that these bugs exist. Gödel has shown us that any useful formalization of mathematics (such as the commonly utilized Zermelo–Fraenkel "ZF" set theory) cannot prove its own consistency. However, that does not imply that it must be inconsistant.
The fact that thousands of mathematicians have used ZF for about a hundred years without finding a contradiction makes me confident that even if it's inconsistant, we should be able to patch it up easily enough. But honestly I don't expect that to happen.
As an example of this, the Greeks assumed that every number was rational (actually, that any two numbers could be expressed as an integer multiple of some common unit). When they did prove that this was false, they re-worked math without it and found that (almost?) all of their other theorems still worked even without the assumption that all numbers were rational.
for any almostZero, it is possible to find an integer m1, so that the m1.2.pi + pi/2 is greater than 1/almostZero and therefore for which sin(m1.2.pi+pi/2) =1; 1/(m1.2.pi + pi/2) will be smaller than 1/almostZero. It is also possible to find an integer m2, so that m2.pi+pi is greater than 1/almostZero and therefore for which sin(m2.pi+pi) =0; 1/(m2.pi+pi) will be smaller than 1/almostZero. The claim: find me an almostZero for it is not possible to find such m1,m2.
This could be a possibility, but I haven't written the program yet ;-)
I don't see how the code provided has any relation to the Curry-Howard correspondence, which is a statement relating types and proofs.
I was also under the impression that programs like Mathimatica enabled you to do this with mathematic equations. But I guess for many they would take a long time to prove.
I suppose a easy way to sum up the article is we have a mathematic symbol for infinity, yet we could never compute that on a compter as you could always add a value greater than zero.
What does this have to do with "flaws" in contemporary mathematics though? If you're trying to use this as an example of a flaw in anything, it would be the computer industry for not figuring out artificial intelligence, not the mathematics community. So, if this was the author's intention, then I think it's flawed right from the outset, but I don't think this was truly the author's intent. (For one thing, Curry-Howard correspondence is talking about lambda calculus, not what you think when you hear "computer" today.)
Really, the article's entire premise is predicated on extreme misunderstandings of Godel. For instance:
> In fact, Gödel's 1931 Second Incompleteness Theorem insists that it is strictly forbidden to ever claim the truth of any scientific or mathematical statement:
What? Where does it say that? It says (quoting the article here):
> For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.
If a theory includes a statement of its own consistency, then that theory is inconsistent. How does that imply that it is "strictly forbidden to ever claim the truth of any scientific or mathematical statement"? The honest answer is that it doesn't, not in the slightest. When it comes to mathematics, we're not saying the axioms are consistent, we're saying statements within this set of axioms are true. Are the axiomizations true? I don't know, but a lot of work has gone into these theories and so far they look pretty good. But at any rate, the author uses this theorem in a completely incorrect manner. He is right that we don't know if any of the various mathematical foundations are consistent, true, but as I said, so far everything looks pretty good.
Then he throws this bombshell:
> Given Gödel's First Incompleteness we already know that for any claim making use of basic arithmetic, counterexamples must exist.
What? How? Here's Godel's First Incompleteness Theorem, per Wikipedia:
> Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory (Kleene 1967, p. 250)
How in the world does that say that "for any claim making use of basic arithmetic, counterexamples must exist." (Counterexamples of what, anyway? Basic arithmetic?) Actually, what the theorem says that you can't have a theory capable of expressing elementary arithmetic that is both consistent and complete. The both is the huge part. So far, for example, we think ZFC is consistent. We know it is not complete; see this: http://en.wikipedia.org/wiki/List_of_statements_undecidable_... . So, the idea that there "must exist counterexamples" (of what, I don't know) as per Godel's First Incompleteness Theorem is simply ridiculous. As a result, we don't know that there are "simply bugs" in the "successor function." As a result, the idea that "all basic claims are more or less false" is completely shot down. Needs better proof.
> The claim above is not Popper-compliant.
Why not? It's falsifiable, so it is. (If it were false, you would need simply to provide an extremely small epsilon and ask for the correspondingly large delta.) It gives the "appearance" of truth because it is indeed true -- relative to th...
The first flaw is that it is not a proof but only a reduction. The second flaw is that contemporary math does not make the slightest attempt at making its claims easier to verify. What is wrong with an invitation/challenge in the form of a program asking to show the claim wrong?
> Not being able to provide a counter example does not prove the claim.
It is never possible to prove a claim anyway. It is only possible to prove that it does not contain original untruth.
Be careful to define your terms. Most people, including mathematicians, will insist that Euclid's prime theorem proves that there are an infinity of primes -- that the assertion is "true".
http://en.wikipedia.org/wiki/Euclids_theorem
But it will always be possible to redefine "true" arbitrarily to reject any such claims, which partly explains philosophy's low standing among intellectual disciplines.
> It is never possible to prove a claim anyway.
You've shifted ground in your wording, and contradicted the idea of a mathematical proof. There really are mathematical proofs.
In general science, your claim is correct -- a theory cannot be proven true, only false. But in mathematics, proofs exist.
This is false. You're overlooking a very important difference between math and science. Science is empirical, which means any scientific theory can be overthrown by new evidence arising in nature. This is not true for mathematics -- once a conjecture becomes a theorem, it's irrevocable.
Your viewpoint is a philosophical one that fails to account for the key difference between math and science.
One then takes the true true statement 1+1=1+1 | Identity And finds: 1+successor(0)=1+1 | Definition of 1 successor(1) + 0 = 1+1 | Definition of + 2 + 0 = 1+1 | Definition of 2 2=1+1 | Definition of +
I made no observation to prove 1+1=2. What I do observe is that if we map the counting numbers to the count of how many apples I have, and we map the addition operation to combing to groups of apples, then the mathematical result is consistent with reality. However, if we empirically discover that the mathematical result is not constitent with reality, than that does not mean that the math is wrong, it simply means that the reality does not behave in a way that corresponds to the math.
In that case, we should watch out to use that kind of math in engineering or for example calculate expected airplane behaviour with it.
He goes from the statement "For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent." To "all basic claims are more or less false." If we could actually prove that all claims were false, we would be in violation of the Incompletness theorum.
Not to mention the absurtidy of his conclusion. Proving a statement for a set of values you thought of is far more likely to be wrong than proving it with formal mathamatics.
That is grossly wrong interpretation of the theorem. I stopped reading the article right there.
This, if the program did fail all that's been proven is that that particular delta-epsilon function, the defeatEpsilon here, doesn't work. In order to prove that the function doesn't converge you have to prove there is no function which can satisfy the conditions.
(Luckily there are some theorems which make it so one only have to prove that two different sequences of the function converge to different values. But that's getting into Real Analysis which is a whole semester worth of explanations.)
It would prove that such epsilon exists. That counterexample should be enough to reject the claim itself.
That claim is false, therefore, the truth of that claim is equivilent to the truth of 'false'. Becuase your article is true iff all of the statements within it are true, and your article contains a statement which is false, then your entire article is false. Using this, we can 'reduce' the 'proof' of your into assert(false). I suspect that the parent is using 0 as an alias for false.
More generally, for any contemporary mathamatical proof, what you call a reduction, you can reduce the proof of the form you describe to either assert(true) xor assert(false), depending on what the mathametical proof/reduction shows.
Oops, my python roots are showing.
(P.S. I used to be a mathematician in my previous life)