*sighs*
The limitation of the proofs that they are citing lie in the associated computer programs used to cover a large number of special cases. We currently have neither the ability to prove the correctness of computer programs nor the theoretical basis for doing so. Part of the difficulty lies in a proof by Turing that is a variant of the Godel theorems.

Can't even prove there is a computer....

IIRC, Marilyn Vos Savant (she of the stratospheric IQ) once wrote a monograph detailing the reasons why Andrew Wiles' proof of Fermat's Last Theorem was unacceptable. Basically, it boiled down to surveyability, the ability to keep the entire proof in your head. Wiles' proof was so intricate and long that (according to MVS) it could not be followed.

It is tangentially related to the lack of surveyability of proofs by computer.

G�del proved that any sufficiently complex logical system will by necessity contain truths that cannot be deduced from within that system. His proof is based on a rigorous application of set theory, 1st order predicate logic, and lamba calculus.

Whether the human mind is similarly constrained and thus cannot prove certain true statements, is an argument for the meta-theorists. Basically it boils down to whether you think the Church-Turing thesis is applicable.

damn him and the horror he has caused to be visited upon undergraduates.

Can't even prove there is a computer...

Don't have to, the computer is axiomatic, or rather its existence is implied by the definition of a computable real number, which in turn relies on the axioms of lambda calculus. Bearded, God-killing axioms.

joe:

Yes, that it's all axiomatic is self-defeating.

Ptah:

I'm not sure about the latest research, but I suspect that problem is insoluable; I would think a proof of program correctnesss is equivalent to the correct program, and thus you have the problem of proving your proof which is no easier...

In the words of the great Donald Knuth:
Beware of bugs in the above code; I have only proved it correct, not tried it.

Mike/Ptah: how long have proofs featured embedded code? I can vaguely remember this issue surfacing & recall it was controversial at the time, but do not remember how long ago that was. Thanks.

The first significant use of this was the proof of the 4 color map theorem, which was back in 1977.

The first case was the Four Color Theorem. Haken and Appel used convential induction to get to the point where they could say that if there was a 5 colorable map, it had to include one of about 20,000 cases. They then used a computer program to test every one of those cases to show that none of them required 5 colors, and so therefore no map needs 5 colors. QED. Nothing inherently wrong with that, as if there'd been only five or seven cases, the classic form would have solved them, even though it would be considered an "inelegant" proof. The objections were that you were assuming that the computer program correctly colored each map. Since it's been almost 30 years and no one has objected, I guess we can conclude that they got it all right. (Then again, I've never heard of, or seen, any attempt at repeating their work. I find it hard to believe that someone hasn't tried, but it's possible.)

AOG is correct: I recall being troubled at the time at the departure from formal logic.

So, OJ, is there such a thing as TRUE Faith and FALSE faith? How do you know the difference?

P:

Aesthetics.

I feel like [Goliath] going up against [David] each time OJ misreferences Godel.

Here it comes...

Mike:

You are. Belief that math is more than a faith is philistine.

OJ:

Don't misunderstand me, I think math is axiomatic, and so it is faith based too, but that's not what Godel showed. Hence I'm David.

P:

Aesthetics.

Yeah, and my mom said she was gorgeous because Rubens painted fat ladies.
-------------------------------------------
Something else to throw into the mix ;)

Let us take any given set of axioms as the basis for a logical mathematics that contains arithmetic. If it is consistent, then Godel's theorem states that it is incomplete because he has an algorithm that can generate a mathematical statement that is guaranteed to be both true and unprovable given the original set of axioms as the input. If A0 is the original set of axioms, then Godel's algorithm generates a new member. The supposed fix by adding that new axiom to A0 to yield A1 won't work because the Godel algorithem also works on A1. I.e. A0+G(A0) yields A1. A1+G(A1) yields A2. A2+G(A2) yields A3. Nobody was really worried about a set of axioms by which one generated an infinite number of truths, but an infinite number of sets of axioms was too much to handle.

Enter Cantor, transfinite mathematics, and Aleph (google them). Transfinite mathematics is designed to reason about infinities, and thus can reason, not only about A0 and the infinite number of truths it can generate, but the infinite set of infinite sets of truths generated by the infinite set of {A0, A1, A2, A3....}. The idea is to realize that there is a 1 to 1 correspondence between the natural numbers (1, 2, 3...} and the infinite set of {A0, A1, A2,...}, and the number Aleph represents the "size" of both those sets. Surprisingly enough, the size of the set of rational numbers (natural number divided by natural number) IS EXACTLY THE SAME as the set of natural numbers. Both proofs are done by a demonstration known as diagonalization: you come up with an algorithm to map the rational number "textually" to a unique natural number that maintains the ordering of the rational numbers by looking at the mapped natural numbers, while you just add 1 to the subscript of the axiom set and use that one to map the axiom set to the natural numbers. If R1 and R2 are rational numbers, and D(R1) and D(R2) are the natural numbers assigned to them, then if R1

The set of REAL numbers are NOT mappable to the natural numbers because one cannot enumerate the irrationals. I don't recall the proof, but I think it involves the fact that no one-one on-to mapping between real numbers and the natural numbers can avoid the fact that if R1

Because transfinite math can swallow infinities whole, it can not only handle the godel axiom set {A0, A1, A2...} for any starting Axiom set A0, but can even deal with an infinite number of starting sets A0, B0, C0, D0, etc.. It is possible to diagonalize not only {A0, A1, A2...}, but also ALL THE TRUTHS THAT THEY CAN DERIVE, with the natural numbers. The result, if I recall correctly, is that there are as many logical systems, plus derived truths, plus Godel-originated truths that are not provable, as there are natural numbers.

This is important because of a rational assumption that all mathematicians make about undecidable logic systems that include mathematics: If you know that there is ONE truth of the system that is not provable, then it can be shownt that there are possibly an infinite number of them. I don't remember who made the argument (Cantor, I believe), but they noted that, if that was true, then the number of systems, combined with their truths, would have MORE members than the natural numbers, and probably the SAME number as the set of real numbers. I.e. transfinite mathematics proves that, for any set of initial axioms A0, that there is one and only one truth that is NOT PROVABLE in logic system A0: G(A0).

The problem: Transfinite mathematics used in this way is an explicitly METAmathematical system: I.e. the ONLY THING IT CAN TALK ABOUT IS MATHEMATICS, AND NOT ANYTHING ELSE, while the claim for MATHEMATICS is that it CAN EXPLAIN EVERYTHING. The belief that something explicitly narrower in scope can completely explain something that is believed to be of wider scope is why nobody believes that Transfinite mathematics has disproved Godel's theorem.

Another problem: I believe, after Godel gave his proof, that someone proved that transfinite mathematics itself is incomplete by using the same trick Godel did with arithmetic. Thus, you'd need a trans-trans-finite mathematics to show that transfinite mathematics is complete, using the same proof that transfinite mathematics used to prove that a specific consistent set of axioms A0 is complete. However, the proof that trans-trans-finite mathematics itself is complete involves the use of trans-trans-trans-finite mathematics.

Ad infinitum.

The general rule is that, regardless of order, any system of mathematics can only be proven complete by a system of mathematics of a higher order (one more "trans-" appended to the front of it.).

Aww darn, I forgot that < needs to be written as &lt;: The formatting is all messed up. sorry people. Preview would have been my friend.

Diagonalization requires the assignment of natural numbers to the set being evaluated by being able to assign a natural number to each member in the target set such that if the target set is ordered, that the natural numbers assigned to each member is in the same order as the order of the target set. The reason why there are more real numbers than natural numbers is that there is no way to rationally assign ADJACENT natural numbers to two real numbers R1 and R2, and be able to assign a VALID natural number to all the real numbers BETWEEN R1 and R2. The truths derivable from an axiom set A0 would have been ordered in the order in which they would have been generated by the "mathematics machine" that was the goal of the vienna circle, with A0+G(A1) having a number bigger than any element in the set derived from A0 alone.

logic, [Godel] was convinced, is not the only route to knowledge of this reality; we also have something like an extrasensory perception of it, which he called �mathematical intuition.�

Zaftig (sp?) is beautiful. Skinny ain't.

OJ:

Perhaps a better reference - which doesn't change the conclusion, it's just pertinent - would be Turing and his noncomputable functions.

Turing, as I recall, wasn't capable of accepting the implications of Godel's thinking. As few physicists could accept Heisenberg and Schrodinger or biologists accept Mayr. No one wants to hear their profession is a ghost chase.

Bravo, or brava, ptah.

"No one wants to hear their profession is a ghost chase."

More like that they held the wrong beliefs, and unlike in religion, it can be shown that the gods they'd worshiped all their lives were false. Best example of this phenomena is Einstein's last 40 years.

And note that that doesn't mean that the new gods are proven to be true, just that they haven't had their chance to be overthrown, too.

Ah, you're all missing the real boat.
You have to watch the CBS show "Numbers", for a really great introduction to the wonderful world of math.
Mike
http://www.tv.com/numb3rs/show/25043/summary.html

OJ:

I take back Turing - consider this, even if all mathematical statements were provable, as David Hilbert had originally hoped, they would still be axiomatic. Godel showed that there are a few unprovable statements, but the provable statements depended on assumptions anyway.

As to quantum mechanics, no one really accepts/likes it, it just gives the right answers. Doesn't mean studying it isn't useful, though.

Mike:

Yes, the dream was dead even before he pronounced it officially so, but still they held to it 'til then and most do even now.

Of course as long as we can jigger numbers until a theory produces decent technological results we oughtn't much care that it doesn't describe reality.

Ptah's dissertation reflects the confused state of modern Mathematics following Russell and Whitehead's attempt to axiomize all of Mathematics. G�del's original paper was titled "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" (available here in translation). He showed it was possible to construct a closed, 1st order predicate calculus statement containing bound arithmetic variables which was formally undecidable (i.e., neither it nor its negation could be demonstrated in the axiomatic system). Since by Tertium Non Datur (a statement must be either true or false, there is no third choice) either the statement or its negation is necessarily true, then there exist true statements which can not be demonstrated, i.e., the axiomatic system is incomplete. [Some claim G�del's statement must be true for semantic reasons, but this is both unnecessary and involves a covert assumption of Tertium in the semantic interpretation of the statement]

G�del's arithmetization of logic was a clever way around Tarski's ad hoc resolution of the Liar Paradox. To avoid the paradox, Tarski decreed that any statement about the truth (or falsity) of a logical statement was a "meta-statement" on a different level than the statement, and added his material criterion to prevent the infinte regress of truth value. This is commonly accepted today, though it is not without problems. (This is the viewpoint embodied in Ptah's trans-statements.) G�del simply revived the Lair Paradox by replacing discussion of truth value with the logical demonstrability of a statement. Since truth is not being considered, Tarski's solution is unavailable. Since truth and demonstrability are related to each other by the concepts of consistency and completeness of the axiom system, the extended paradox calls into question the completeness (or the consistency) of the system. Since mathematicians wish to limit the damage, they prefer to regard the system as incomplete rather than inconsistent, though consistency can not be proven. (G�del's Second Theorem "proves" that the Principia axioms can not be proven consistent)

At least, this is the way G�del's Theorems are normally interpreted. In an alternate universe (mine), I prefer to view G�del's result as the continued, extended criticism of Tertium begun with the Liar Paradox. If another logical value is admitted which can be consistently interpreted as "undecidable", then I can agree with G�del that his statement is formally undecidable, but this no longer means the system is incomplete, because it can no longer be argued that the statement must be either true or false -- both the statement and its demonstrability may be undecidable. The semantic argument likewise fails because the negation of an undecidable statement is itself necessarily undecidable. This viewpoint changes the supposed paradoxes into merely deficient definitions.

I believe that mathematicians thus have a choice. They can accept the traditional axioms and thereby be forced to accept Tarski and G�del's unsavory results, or they can accept another set of axioms without these pernicious consequences. And while I am not alone in favoring this approach, I must admit it is a minority opinion. It is a matter of where to place your faith.

Posted by: jd watson at February 22, 2006 11:29 PM

There are lots of alternative theories to quantum too, but the questions is what do they produce/predict that's better? Axiomatic mathematics has produced a lot of useful theorems; does the alternative add anything?

Regarding paradoxes, they don't seem to stop the theories from working. As he originally stated it, Zeno's paradox has never been resolved, but limits and calculus work just fine. QED introduces a zero point energy, which has the effect of introducing an infinite energy density into the universe - the approach was just to DC-offset it, which sounds like a kludge, but it works better than anything has ever worked before.

Mike:
Your analogy between formal axiomatic mathematical systems and empirical scientific theories seems tenuous to me. While usefulness is sometimes considered a criteria of empiric truth, such is not the case for mathematics. Few mathematicians would cite usefulness to justify their results.

I was not criticizing axiomatic systems, simply pointing out that a choice of different axioms is possible. G�del's Theorems seemed to remove any hope of proving the consistency and completeness of the Principia system -- it introduced a logical nihilism which still prevails.

Posted by: jd watson at February 23, 2006 3:50 PM