A bunch of people have been asking me to take a look at yet another piece of Cantor crankery recently posted to Arxiv. In general, I'm sick and tired of Cantor crankery - it's been occupying much too much space on this blog lately. But this one is a real prize. It's an approach that I've never seen before: instead of the usual weaseling around, this one goes straight for Cantor's proof.
But it does much, much more than that. In terms of ambition, this thing really takes the cake. According to the author, one J. A. Perez, he doesn't just refute Cantor. No, that would be trivial! Every run-of-the-mill crackpot claims to refute cantor! Perez claims to refute Cantor, Gödel, Church, and Turing. Among others. He claims to reform the axiom of infinity in set theory to remove the problems that it supposedly causes. He claims to be able to use his reformed axiom of infinity together with his refutation of Cantor to get rid of the continuum hypothesis, and to eliminate any strange results proved by the axiom of choice.
Yes, Mr. (Dr? Professor? J. Random Schmuck?) Perez is nothing if not a true mastermind, a mathematical genius of utterly epic proportions! The man who single-handedly refutes pretty much all of 20th century mathematics! The man who has determined that now we must throw away Cantor and Gödel, and reinstate Hilbert's program. The perfect mathematics is at hand, if we will only listen to his utter brilliance!
To give you a bit of background: towards the beginning of the 20th century, mathematics was in a confused state. They'd just started to encounter problems with paradoxical statements in foundational things like set theory. David Hilbert, one of the great mathematicians of the time, set out a grand goal: to create the perfect mathematical foundation. The goal was to carefully start from first principles, and:
- create a precise formal system in which everything followed a set of strict, well-defined rules;
- define the rules to prevent inconsistency by strictly preventing anything from reasoning about itself. This was done by by separating everything strictly into orders. A first order statement could talk about mathematical objects, but not about predicates. A second order statement could talk about objects and first-order predicates, but not about second-order predicates. A third order statement could talk about primitive objects, first order predicates, and second order predicates - but not about third. But within the system, you could never even formulate a statement in which a second-order predicate talked about a second-order predicate.
- the system was supposed to be complete: in it, all true statements could be proved to be true; all false statements could be proved to be false; and all statements were either true or false.
- the system was supposed to be consistent: no contradictions could ever be derived from valid applications of the system. Every statement was either true or false - there would be no statements that could be proved to be both true and false; and there would be no statements that could not be proved to be either true or false.
- the system was supposed to be decidable: there would be a mechanical process which, given any statement, would be able to tell you after a finite period of time whether the statement was true or false. ere would be an algorithm which would, after a finite amount of time,
Hilbert's program was a huge deal. It consumed a huge amount of time and resources from the best mathematicians of the time. It's well known for producing a major work by Russell and Whitehead called the Principia, which took hundreds of pages to work its way up to being able to prove that 1 + 1 = 2. It was a truly epic project; but if it were successful, it would have put all of mathematics on a sound basis. It would, in some deep and important sense, have completed mathematics.
Alas, Gödel's work blew Hilbert's program right out of the water. You can't built a complete, consistent system of mathematics. You can't define a complete system of math with a decision procedure. But our intrepid genius claims that all of this is wrong: Cantor's set theory is bogus, the set of reals is the same size as the set of natural numbers, Gödel's incompleteness theorems are wrong, Turing was wrong about computability, and we can re-instate Hilbert's program, finish the Principia, and happily have the perfect mathematical system, with J. A. Perez as the most brilliant mathematician of all time.
Except for the minor problem that he's completely wrong.
What he does is interesting, in a brain-dead sort of way. He basically tries to find a problem with the basic proof technique used by both Cantor and Gödel. Of course, proof by contradiction is an old, well-respected proof system. You can't just say that all proofs by contradiction are wrong. There are lots of really good proofs that are done by contradiction. But Cantor and Gödel are obviously wrong, and yet both proofs look bulletproof - so there's got to be something wrong with how they used proofs by contradiction.
What he homed in on is what he calls internal contradiction versus external contradiction.
He claim that the classical uses of proof by contradiction are what he calls external contradiction. In proof by external contradiction, you start with a statement P, which you want to prove is true. So you assume that it's false, and then you use that to derive a contradiction. So you assume not-P, and then use that to derive a proof of some other statement, R, which is known to be false. So by the process of proof from not-P, you've derived the contradiction R∧¬R. By simple logic, that means that not-P allowed you to prove a false statement, which in turn means that not-P is false, and that means that P is true. Presto, you've got your proof.
In contrast, Cantor and Gödel are what he calls proof by internal contradiction. He claims that in these proofs, you start with the statement you want to prove - P. Then you negate P; and by using not-P, you can derive a proof that P is true. So not-P is used to derive P. Instead of ¬P deriving R∧¬R, ¬P is used to derive ¬P∧P.
It's an interesting distinction in its way - it's fundamentally a difference between a proof built on self-reference, and one that isn't. Self-reference is the source of many problems - the fundamental paradoxical statements that have plagued modern math are all built on self reference: Cantor's naive set theory was shown inconsistent by the use of a self-referential object: the set of all sets that do not contain themselves; Gödel's proof is build around the self referential statement "There is no proof that this statement is true".
But there's no logical flaw with a proof that has a self-referential aspect. Or is there? Perez claims that there is.
Let's start with his version of a proof by external contradiction. He says that every proof is, essentially, a sequence of statements, Q1, Q2, ..., Qn, where each statement Qi+1 is an implication of Qn. So you can state a proof as Q1 ⇒ Q2 ⇒ ... ⇒ Qn, where Qn is the conclusion. In this formulation, Q1 is the statement ¬P - that is, the negation of the statement you want to prove; and Qn is the statement R∧¬R, where R is some statement that is neither P nor ¬P. (That last line is, according to Perez, very important. He repeats it several times in different ways.) So the entire proof can be reduced to ¬P⇒(R∧¬R).
In a proof by internal contradiction, you've got the same basic setup, except that you start with ¬P, and you end up with ¬P⇒(¬P∧P). That is, the final contradiction that breaks the proof contains the initial false assumption.
According to Perez, that's potentially a problem. It isn't necessarily a problem, but it might be. See, if you can reason backwards from the contradiction to cast doubt on any of the earlier statements, then according to him, the proof will fail.
This is where things start to get a bit goofy. Suppose that in your basic proof schema, all of the implications were not just implications, but logical equivalences. That is, your proof schema for the proof by internal contradiction was: (¬P)⇔Q2⇔...⇔Qn-1⇔(¬P∧P). Then you've got a known-falsehood at the end - and you can also use that backwards. So (¬P∧P) ⇔ Qn-1. And, in fact, (¬P∧P) imply each any every one of the Qi. So the invalid conclusion implies each of the statements in the proof - which means, according to Perez, that the truth of every statement is thrown into question; in fact, the proof by internal contradiction contains an implicit disproof of every true statement used in the proof. Since the entire proof technique is doing something that we know to be incorrect, that demonstrates that the proof by internal contradiction, when the logical connectives are equivalences, is invalid.
If that proof technique is invalid, then every proof that was built using it is also invalid. So Cantor's diagonalization goes out the window. And so does Gödel. And so does most of Chaitin. And, well, lots of other stuff.
The problem for Perez is that this argument is bogus in so many ways.
Let's take one nice one, which he's absolutely explicit about. His proof schema is based on a proof as a sequence of atomic statements, each of which implies the following statement. That's not the structure of a proof. A proof does have a series of implications leading to a conclusion, but it's not linear. Proofs are graphs of implications, not lines.
A perfect demonstration of how bogus this is comes from Perez's discussion of Cantor's diagonalization. According to Perez, you start with the statement P that you want to prove. In Cantor's diagonalization, P is the statement: "The unit interval I = [0, 1)" is an uncountable set.". The proof is sketched as:
- Take ¬P to use as the foundational step of the proof by contradiction: ¬P="The unit interval I := [0, 1) is a countable set".
- Q1 = "The set I can be written out as an array of decimal expansions, ..."
- Q2 = "It is possible to define a real number ... such that it belongs to the interval, but ..."
- Q3 = "The array is not a complete listing of the elements of I."
According to Perez, ¬P⇔Q1. That is not true: assuming that the interval is a countable set does not give you the fact that the set can be written out as an array of decimal expansions. The decimal expansions comes from an entirely different starting point. So the proof actually has two branches from the beginning. The proof isn't a straight line of implication; it's a branched structure. So the proof schema isn't "¬P⇔Q1⇔Q2⇔Q3." It's actually "¬P. Q1. ¬P∧Q1∧...↔Q3." (I left the dots, because there are still missing steps; ¬P∧Q1 isn't enough to get get to Q2.)
The branching is a fundamental problem for Perez. Because what he wants to say is that every statement used in the proof is invalidated by the contradiction. But with logical connectives like "∧", that's not true. Perez wants to say that since Q3 provides a contradiction, that it invalidates Q2; which invalidates Q1. And, in fact, according to Perez's reasoning, it does worse than that: it invalidates every axiom used in the proof - because the axioms are used as steps.
But axioms aren't used as discrete atomic steps of the proof implied by prior steps. They're used as parts of complex statements. Axioms are used in the form "Qi ∧ Axiom ⇔ Qi+1." The negation of that doesn't imply the negation of the axiom; it implies (¬Qi) ∨ ¬Axiom).
And boom, there goes Perez's proof; the structure of a proof by internal contradiction doesn't imply the falsehood of every statement used in the proof. It doesn't imply the falsehood of any axioms.
But there's more stupidity. One of the most basic rules of logic is that you can't reason from contradiction. That is, given a statement like (A ∧ ¬A), the statement is always false. Given any false statement, you can arbitrarily construct implications: for any possible statement S, no matter whether S is true or false, (A∧¬A)⇔S. The fact that a contradiction implies something is utterly worthless. You can never reason from that implication, because the statement (A∧¬A) is always false, so you can't infer anything about the conclusion. The entire process that Perez uses, trying to trace backwards from a contradiction is fundamentally meaningless.
From this point, things go downhill. Perez then verges into classic anti-Cantor-crackpot material, providing his version of several different constructions that allegedly demonstrate a correspondence between the natural numbers and the reals. And then he really goes off the deep end.
Seriously, this is one of the most ridiculously grandiose works of crankery that I've ever seen. This guy seriously believes that he's pretty much the most brilliant mathematician in the history of mathematics, and that this paper is the ultimate mathematical tour-de-force. He's probably sitting in his office waiting for his Fields medal.
Physical Science
Comments
"for any possible statement S, no matter whether S is true or false, (A∧¬A)⇔S"
You're arrow has too many heads. It should be (A∧¬A)=>S. The other direction only holds if S is false.
Posted by: Anonymous | March 9, 2010 9:12 PM
He's also wrong about Cantor's argument in a different way: You can phrase the diagonalization proof as being what he calls a proof by external contradiction. This takes minimal effort. You start with your hypothetical 1-1 mapping function and you get a specific number that is not equal to itself (since it is both in the range and not in the range of your function).
Posted by: Joshua Zelinsky | March 9, 2010 9:14 PM
Checking the Combined Membership List of the AMS, I did find a Juan Perez, who is a graduate student in mathematics at the University of Michigan. I don't know whether he is the author of the paper, but he is the only match in the CML.
Posted by: ARS | March 9, 2010 9:56 PM
ARS: Nope, that's the wrong one. Different middle name (google "Juan Perez michigan" and look at the google profile at the bottom of the page)
Posted by: Max | March 9, 2010 10:03 PM
If his "reasoning backward" argument made sense for proofs by "internal contradiction", would it not make equal sense for proofs by "external contradiction"?
(You introduced the distinction, but then promptly failed to use it for anything. Curious whether Perez does the same thing. Well, not that curious. You seem to spend a lot of time reading crackpots.)
Posted by: Nemo | March 9, 2010 10:06 PM
Oh, Perez got up on the arXiv at last? I'm going to enjoy reading your analysis of his writings - he spent some time about a year back trying to convince me to sponsor his posting to the archive.
Posted by: Mikael Vejdemo Johansson | March 9, 2010 10:19 PM
He may be a crank, but at least he managed to derive a date with your mom!
Posted by: Spencer Bliven
| March 9, 2010 10:26 PM
If you assume ~P and derive P, we can proceed two ways:
(1) Obtain P immediately by the principle of non-contradiction.
(2) Directly, as in a conditional proof, where we have shown that ~P => P, which is equivalent to ~~P v P, and so P.
Posted by: ijc | March 10, 2010 1:49 AM
There's a dangling sentence fragment under the bullet points listing the goals of the Hilbert Program. Not critical, but somewhat distracting.
Posted by: Ingvar | March 10, 2010 4:54 AM
To P or not to P, that is the question.
Posted by: xavier johnson
| March 10, 2010 6:31 AM
Whoa, that's one verbose explanation. Even I can get it, and I'm not mathematician :)
Posted by: Kuroki Kaze | March 10, 2010 7:30 AM
"(¬P∧P) imply each any every one of the Qi"
should probably be:
"(¬P∧P) imply each and every one of the Qi"
Posted by: Tristram Brelstaff | March 10, 2010 7:42 AM
Mark,
I generally enjoy your posts but as an old physicist could use a little help on the notation. Does the little square mean "and"?
Posted by: bobh | March 10, 2010 8:04 AM
@bobh 13
The square means that your browser is not rendering properly. It inserts a square there as a filler instead of the actual symbol.
Posted by: mike | March 10, 2010 8:35 AM
For those not getting the joke Bliven@7 made
http://xkcd.com/704/
Posted by: Robert S. | March 10, 2010 9:46 AM
The first part makes it sound like Perez was halfway to reinventing some sort of finitist/constructivist approach to mathematics, before going off the rails.
I suppose the difference between a crank and a mathematician is that, given a proof with a distasteful conclusion, the crank futilely attacks the proof, while the mathematician finds an axiom the proof relies on, declares it "obviously false"[0], and gets back to work.
Maybe someone should sit these cranks down and tell them that, while Cantor's proof really is sound, it honestly is, why don't they just regard it as a proof-by-absurdity that real numbers don't exist, or something? Really, for geniuses of their obvious caliber, attacking a mere proof seems trivial when they could be striking at the flawed axioms that everything else builds from.
[0]: When Alfred Tarski sought to publish a proof of equivalence between the Axiom of Choice and the statement "every infinite set A has the same cardinality as the Cartesian product of A with itself", it was rejected by two different reviewers; one wrote that an equivalence between propositions known to be true was not novel, while the other wrote that an equivalence between propositions known to be false was not interesting.
Posted by: a soulless automaton | March 10, 2010 9:55 AM
For those having trouble with the character rendering...the little square means that the "and" symbol (looks like an upside-down "v") doesn't exist in the font that your browser is using. You'll want to change the "sans-serif" font to something that includes it. In my case, the default for sans-serif was Arial, which doesn't include the "and" symbol (∧). I changed to Trebuchet MS, and now it renders correctly.
Depending on the browser that you're using, you need to open the Preferences or Options pane, find where you can set the default font, and then (probably) click on the "Advanced" button.
Posted by: Tom | March 10, 2010 11:08 AM
@mike 14
Thanks. Using latest Firefox on Windows. Tried latest IE and it displayed properly - makes sense now.
Posted by: bobh | March 10, 2010 11:13 AM
Thanks for this.
I'm not a mathematician - but I still enjoy reading this blog. Thanks for keeping the level of math high but explaining it even for us dummies ;)
Posted by: ex | March 10, 2010 11:22 AM
@16: That story really cracked me up! :)
It reminds me of another (quite unrelated) story, about a professor in my university: In one of his reviews, he said that the author gave "unnecessary and insufficient conditions for [statement]"... Pure genius :)
Posted by: Quercus | March 10, 2010 1:34 PM
Mark C. Chu-Carroll: He claims to be able to use his reformed axiom of infinity together with his refutation of Cantor to get rid of the continuum hypothesis, and to eliminate any strange results proved by the axiom of choice.
You don't have to reform the axiom of infinity to do that; that may just require taking Refutation of the Axiom of the Power Set. Without being able to assert that the Infinity Axiom set's Power Set is itself a set, you can't construct sets of higher cardinality than the initial Aleph-0, which throws out the question of the continuum hypothesis by throwing out both the Real Numbers and all the other cardinalities. =)
Mark C. Chu-Carroll: Axioms are used in the form "Qi ∧ Axiom ⇔ Qi+1."
I think it would be more precise to say that they are used in the form "Qi ∧ Axiom ⇔ Qi ∧ Axiom ∧ Qi+1".
Mark C. Chu-Carroll: That is, given a statement like (A ∧ ¬A), the statement is always false.
Well, in a logic based on any Boolean lattice, anyway. In a logic based on a Heyting lattice, it may be a value that is neither TRUE nor FALSE, akin to UNDEFINED. However, Heyting logic isn't used much except by perverse philosophers who don't like one or another Boolean axiom.
Posted by: abb3w | March 10, 2010 2:53 PM
Pages 31-35 or so are particularly amusing. Proof of this statement is left as an exercise for the reader. :)
Posted by: delosgatos | March 10, 2010 3:50 PM
This distinction between internal and external contradictions seems particularly inane. Since, as mentioned, a false premise can imply anything, it doesn't take much to get from P => R ^ ~R, and R^~R => P ^ ~P, to P => P^~P. So voila... an 'external' contradiction IS an 'internal' contradiction.
Semi-random, amusing aside that this reminds me of....
In a fundamentals of advanced math course several semesters ago, there was a problem on a test to prove that there were no solutions to some simple inequality, via contradiction. After about 3-4 lines, I arrived at x^2 + 1
Posted by: Mike | March 10, 2010 4:08 PM
@23:
Two mistakes:
- I think you're wrong on your first point. the fact that you CAN derive P^~P from R^~R doesn't mean that it's an "internal" contradiction - the definition does not mention continuations of the proof.
- x^2+1 is not a statement, so you can't really say it's a "contradiction" :P
Posted by: Quercus | March 10, 2010 4:47 PM
I don’t think Perez is a crank, though his analysis goes against the current orthodoxy. No one has mentioned that his starting point was the construction of a proof of Goodstein’s Theorem in first-order arithmetic (arxiv.org/abs/0904.1957). I can’t see anything wrong with this proof, which doesn’t fall into the Cantor crankery camp. Mark and others have not commented on this proof, so presumably also found it correct. If this proof is correct, as you all probably know, it contradicts Godel and implies completeness. As far as I can see, Perez looked at Cantor and Godel to try and explain this discrepancy. His analysis of proofs by contradiction is spot on, as any basic text book confirms – though clearly this is uncomfortable when applied to Cantor!
Mark is right about branching being an essential part of the construction of any proof, but only to establish the truth of intermediate statements of the main line, so doesn’t hold water as a criticism of Perez’s analysis. Mark’s other arguments against Perez are irrelevant, weak or misrepresent what is actually said in the paper. And Perez doesn’t reformulate the Axiom of Infinity, as Mark wrongly states. I think people should read the paper themselves, objectively, and not rely on Mark’s subjective comments, which address only a small part of the paper.
However, I do agree with Mark on something – Hilbert was a great mathematician, so it’s a shame his views were discounted in favour of Godel. It might be unthinkable at the moment that Perez is right, but it might be easier to swallow if we focus on the benefits of completeness as Hilbert envisaged, and see Godel as misled by Cantor.
Posted by: Colin T | March 10, 2010 6:08 PM
I completely agree with Colin T in #25. I found Mark's review questionably subjective and condescending at times especially with clauses such as "[...] with J. A. Perez as the most brilliant mathematician of all time."
On the other hand, I understand Mark is rather tired of papers claiming to refute Cantor by people who clearly do not understand Cantor.
I hope to see both of Perez's papers get some more attention, especially regarding the [in]completness aspect.
Posted by: Anthony de Almeida Lopes | March 10, 2010 6:38 PM
My personal guess is that both the last two posters are either cranks, or Perez himsel writing under an alias.
Posted by: Rilke's granddaughter | March 10, 2010 7:28 PM
My personal guess is that both the last two posters are either cranks, or Perez himsel writing under an alias.
Posted by: Rilke's granddaughter | March 10, 2010 7:34 PM
Or maybe Perez's proof isn't written in first-order arithmetic. (He also apparently failed to consider the possibility that Paris and Kirby were wrong.)
Perez doesn't understand the contradiction Cantor's establishing. Cantor's immediate result wasn't "the antidiagonal element shows P(N) is not denumerable"; it was "the antidiagonal element shows that the proposed bijection is not a bijection". (Look at example 3.3. The sets S_k are denumerable, but not bijections.)
Posted by: Freak | March 10, 2010 8:07 PM
@25:
Don't presume anything based on what I didn't say.
Perez analysis of proof by contradiction is absolute, utter, total rubbish. He created a meaningless distinction between "internal" and "external" contradiction; and then formulated an invalid proof schema, which he used in his proof. My post is pretty specific about what he did wrong. He specifically claims that the initial statement, "The reals are enumerable", implies and is implied by "The reals are representable". That's crucial to his critque - and yet, it's not true.
As for my mocking him - let's be serious for a moment. If, indeed, Perez was able to formulate a proof that showed that Cantor, Gödel, Church, and Turing were all wrong about some of their most foundation works, it would be a truly astonishing feat of brilliance. If he really did that, he would absolutely deserve to be recognized as one of the greatest mathematicians of all time. No sarcasm there - anyone who could really do what Perez claims to have done would be a historic figure in math.
The problem is, Perez's "analysis" is a pile of rubbish. It's riddled with errors. It's based on meaningless distinctions and invalid logical reasoning. It's purest garbage. And instead of just writing that silly piece of garbage, he uses it as a springboard to set out on a truly ridiculous and arrogant course of redefining most of modern mathematics in silly ways.
And if he doesn't redefine the axiom of infinity, then what the heck is his theorem of real infinity about? It's an attempt to take the implications of the axiom of infinity that he doesn't like, and define them out of existence. He specifically introduces it by talking about the "problems" with the axiom of infinity.
Posted by: Mark C. Chu-Carroll | March 10, 2010 8:08 PM
@28:
Yeah, it sure looks like sockpuppetry. "Colin"'s IP address shows up before his comment. Then there's his comment. Then 30 minutes later, there's another visit from Colin's IP address, immediately followed by a comment posted through an IP anonymizer. It's not proof, but it's certainly suspicious.
Posted by: Mark C. Chu-Carroll | March 10, 2010 8:11 PM
Mark, you don't understand the basics of proof by contradiction. If the infinite prime proof ended up showing that the elements in the list were both prime and composite, you'd say the proof was still valid. So when you talk about Cantor, I just sit back and laugh my head off. You're a riot. You think that if the result is nonsensical, that this is enough for a proof by contradiction.
Posted by: Vorlath | March 10, 2010 9:02 PM
Perhaps Heyting logic isn't popular in mathematics at large, but it's quite relevant in (some branches of) computer science (and related mathematics). Constructive mathematics is in a sense the mathematics of the computable. Through that view, excluded middle says "we can compute proofs or disproofs for every proposition," which is quite simply incorrect. So, it crops up quite naturally in programming languages where one wants to incorporate proofs into their programs.
Also, I may be a bit confused, but I don't think A ∧ ¬A is some undefined, non-false value. It's quite simple to prove ¬(A ∧ ¬A) in intuitionistic logic. What one can't prove in general is A ∨ ¬A. One can prove ¬¬(A ∨ ¬A) for arbitrary A, but the double-negation cannot be eliminated, making A ∨ ¬A in a sense non-false, but not true (or, non-disprovable, but not provable).
Posted by: Dan Doel | March 10, 2010 9:14 PM
His proof of Goodstein's theorem isn't remotely in PA.
The axioms of PA are very low level:
Ax:Sx != 0
AxAy: Sx = Sy -> x = y
...
Just coming up with a way to state Goodstein's theorem in PA is pretty difficult.
[quote=Perez]Proof. Since i) a 1 = a , ∀a N , and ii) 1b = 1 , ∀b N , assume that a , b ≥ 2 . Consider N , the set of the natural numbers. Now consider, within the enumeration of the elements of N, all the powers of a , which can be selected to construct the corresponding subset Na N: Na = {a0, a1, a2, a3, a4, } = {a k, k ∈N}.
(3.1)
The critical requirement is to establish that the subset Na is an infinite set. If Na were a finite set, the implication would be that one of the elements of Na would ...
[/quote]
PA doesn't even have the direct concept of a set, let alone finite vs. infinite. Perez might have done his proof in some first order system equivalent to PA, but if so, he should claim that explicitly.
Posted by: Freak | March 10, 2010 10:22 PM
Freak in #34, good point.
Dan Doel in #33, in intuitionist logic, A ∧ ¬A would be by definition A ∧ (A → ⊥). Applying modus ponens to this renders absurdity. ¬(A ∧ ¬A) would be (A ∧ (A → ⊥)) → ⊥ which, as shown above, by definitional reduction, should reduce to ⊥ → ⊥ which is a tautology. So, I think you're right: ¬(A ∧ ¬A) should be completely valid (and true), as my understanding goes anyway. On the other hand, A ∨ ¬A is not given as an axiom; however, you could justify it or introduce it as an assumption, depending on the specific choice of A. I'm not sure that's relevant for this discussion though.
MarkCC in #31, you thought I was coming from an IP anonymizer? Hmm, weird.. Anyway..
I'm curious, "where are you coming from?" I mean, in general, what logical framework do you work in? Do you disagree with BHK and/or intuitionism in general?
"If that proof technique is invalid, then every proof that was built using it is also invalid."
Indeed, I think this is what he is actually saying. The opinion is not unique to him though as this is a stance taken by many other constructivists and intuitionists. The vast majority of modern type theory operates on this premise.
Posted by: Anthony de Almeida Lopes | March 11, 2010 6:19 AM
I want to clarify that I am neither a Cantor crank nor do I necessarily agree with Perez in general. I do happen to understand Cantor's proofs and I understand that if I were to ever disagree with Cantor it would have to be from a constructive-finitist point of view or it would involve rejecting the actual logic (the formal system itself) as Perez is doing.
My only concern here is that we are not being as open minded from a metamathematical point of view as we could be. If we agree with classical logic, clearly Perez is wrong. That is not to say that Perez is right in any named logic (even intuionistic), but I think it is worth at least entertaining the idea of a mathematics without the specific type of redictio argument that he highlights. Does disallowing them get us anywhere? That is what I really am curious about.
By the way, in contrast to my previous post, Gödel's theorems and proofs for them have been formalized in a proof-assistant that is based on intuitionistic logic (namely, Coq) by Russell O'Connor in 2003. I suspect it has been done by hand many times before that although I do not have a specific reference.
Posted by: Anthony de Almeida Lopes | March 11, 2010 6:49 AM
Actually, it seems there is at least one logic that allows formally reasoning from a contradiction: "para-consistent logic" and it's based on the principle of "dialetheism." (Admittedly, I'm reading about this for the first time.)
Anyway, Perez doesn't mention any of this. So either he's working in classical logic and is wrong, is working in a para-consistent logic and hasn't explicitly stated that he is or doesn't know what he's doing at all (or by dialetheism, all of the above!)
Stanford's Encyclopaedia of Philosophy has a pretty good introduction to dialetheism:
http://plato.stanford.edu/entries/dialetheism/
Posted by: Anthony de Almeida Lopes | March 11, 2010 7:57 AM
@Anthonny de Almeida Lopes (Colin T?)
Mark and most his readers are 15 steps ahead of you. Nobody cares what logic Perez is working with and we aren't irked by the scope of what his claims, if true, would entail. The point is that Perez makes crazy errors all over the place while talking about the most famous proofs from the last century. It's what Mark labels as "Grandiose" that makes this crankery noteworthy.
Posted by: mike | March 11, 2010 8:23 AM
@mike:
Thanks for your response. That's exactly what I was wondering: whether or not his mistakes were independent of the underlying logic (or in general, philosophy) used. It just bothered me that that aspect wasn't addressed explicitly, but I suppose that would be tedious for Mark to do in every post (and probably for his readers to read), especially since such things are probably more obvious to the more experienced here.
Posted by: Anthony de Alemida Lopes | March 11, 2010 8:48 AM
@Dan Doel (#33): Logics with more than two truth values are indeed useful in computer science, though it bears noting that programmers have a different standard term for a third logical value. Multi-valued logics are also useful in digital circuit design, with additional logical values for things like "disconnected". For the truly dedicated, there's even IEEE 1164 9-valued logic.
@Anthony de Alemida Lopes (#39): Did you actually look at the arXiv link? Even if everything he says is correct in some nonstandard logic, he writes as if it applies to standard logic, which doesn't inspire confidence. He also moves very quickly past the crux of his argument (which may or may not constitute a reasonable definition of a nonstandard logic) without giving it a satisfyingly rigorous definition, instead jumping into an extended discussion about all the amazing things you can prove afterwards. Like I said in my previous comment: Cranks complain about proofs, real mathematicians complain about axioms.
Otherwise, everything you say is perfectly reasonable. In fact, speaking as a computer scientist, I'm strongly inclined to question the sensibility of non-constructivist logic, but I'm not about to claim that being unable to express a proof within a typed λ-calculus constitutes a refutation of it.
Posted by: a soulless automaton | March 11, 2010 10:37 AM
The non-standard logic thing is a non-starter.
You can define a logic to produce just about any structure you want. But one of the fundamental points of Gödel is that if you do, and you can express Peano arithmetic in that logical system, that the system is necessarily either inconsistent or incomplete.
If Perez's work is in a non-standard logic, it doesn't matter. Gödel's proof still applies: it shows you how to use Peano arithmetic to construct an unprovable statement, demonstrating that the system is incomplete.
Perez clearly includes Peano arithmetic in his system. So standard logic versus non-standard doesn't matter. Intuitionist or constructivist versus classical doesn't matter.
Worse, Perez clearly states that his result shows that the halting problem is solvable. And yet, the classic problem with the halting problem - the simple counterexample that Turing used in the original proof - still exists. In fact, I can literally write it as a simple, tiny program. A dozen lines of haskell, including various type declarations.
So whatever logic he's using, he's generating trivially demonstrably false results. He even makes a stab at admitting that - basically by creating the notion of "inconceivable", and defining it so that the exception to the halting problem - even though it's clearly trivially constructable - is inconceivable.
Posted by: Mark C. Chu-Carroll | March 11, 2010 10:58 AM
@a soulless automaton in #40: Yes, I did look at it actually, but that doesn't say much as I already admitted, I did not see many of the errors as obvious.
Anyway,
"he writes as if it applies to standard logic."
Yeah, I definitely see that as a huge problem which I think I even mentioned before? I was just curious if anything he said made sense even if his logic was non-standard, which I think Mark, right below your post, explains perfectly.
"but I'm not about to claim that being unable to express a proof within a typed λ-calculus constitutes a refutation of it."
Very good point. Syntactic inadmissability is not refutation at all. Hmmm, right.
By the way, regarding your original comment in #16, "why don't they just regard it as a proof-by-absurdity that real numbers don't exist"
After having read a few of the crank debunkings here (and the extensive comment threads they generate), I actually came to believe that. Glad to know that doesn't make me too crazy.
"Cranks complain about proofs, real mathematicians complain about axioms."
Huh?
@Mark in #41. Awesome explanation. Thanks, I appreciate that you took the time to explain that.
Posted by: Anthony de Almeida Lopes | March 11, 2010 11:26 AM
@Anthony de Almeida Lopes (#42):
My conclusion, upon cursory inspection, was that given his claims, Perez is either catastrophically wrong or is effectively constructing a very weak system (e.g., something like the propositional calculus or Presburger arithmetic) and misapplying it to ideas it cannot express (real numbers, general recursion, etc.). Either way it's deeply confused, but I didn't have time to figure out in which way; MarkCC's comment suggests the former.
"After having read a few of the crank debunkings here (and the extensive comment threads they generate), I actually came to believe that. Glad to know that doesn't make me too crazy."
Outside mainstream mathematics perhaps, but not crazy; real numbers are conceptually very problematic from a computational perspective. Most real number numbers can't be computed--or in fact described--at all, where "computed" means you can produce an approximation to arbitrary precision, like calculating digits of pi. The computable reals remain awkward as well, due to issues such as testing equality being, in general, undecidable (actually equivalent to the Halting Problem, I think).
"Huh?"
I just mean that, when mathematicians don't like a valid proof, they tend to reject a key axiom rather than produce bogus "refutations"--the Axiom of Choice is perhaps the best example, being both intuitively "obvious" and providing proofs of "absurd" propositions.
Posted by: a soulless automaton | March 11, 2010 12:52 PM
@41:
Real numbers are extremely strange. They start off seeming perfectly reasonable, but once you accept them, you're stuck with some very strange results - like the fact that the vast majority of numbers cannot ever even be described. In fact, if you were to really randomly select the a real number from a uniform distribution, the odds of it being a number that can be described algorithmically is zero.
Greg Chaitin, who I personally believe is the best mathematician working in the world today, has said that it's worth at least considering the notion that real numbers don't really exist, but are rather just an artifact of logic.
It's perfectly reasonable to discard Cantors proof for the simple reason that you think that the definition of real numbers is too strange. You can build up a perfectly reasonable mathematics using a system of computable numbers - which gives you the integers, the rationals, and all of the irrationals and transcendentals that you care about.
But it's not standard math. And even by doing it, you don't get rid of much of the strangeness that Perez aims to defeat. It would invalidate Cantor's proof - or rather, Cantor's proof doesn't say that the set of computable numbers is larger than the set of natural numbers; Cantor's proof about the real numbers applies to the real numbers - not to a subset of the reals like the computables. A variant of Cantor's proof *can* still be used to show that the powerset of the set of computables is larger than the set of computables. And it definitely doesn't come anywhere close to touching Gödel; Gödel doesn't use anything but natural numbers in his proof.
Posted by: Mark C. Chu-Carroll | March 11, 2010 1:13 PM
MarkCC raises an excellent point.
Interestingly, we can observe that the computable reals have countably infinite cardinality, as they are (by definition) expressible as finite algorithms, so we know that a bijection between the natural numbers and the computable reals must be possible. The computable reals also have infinitely long sequences of non-repeating digits. These points together at first seem to suggest that Cantor's diagonal proof does apply, letting us compute successive digits of a number not in the list! What is this madness?
In actuality the argument does indeed work in a fashion, but proves something different. The flaw in the above is the assumption that the bijection from naturals to computable reals is itself computable. In other words, the computable reals have in some sense "countably infinite" cardinality, yet it is impossible to actually enumerate, and thus count, them! Gödel will not be denied so easily, I fear.
Posted by: a soulless automaton | March 11, 2010 2:19 PM
@a soulless automaton (#40)
It's actually not that intuitionistic logic has more than two 'truth' values. It doesn't have true, false, and file-not-found. :) At least, it doesn't have three provably distinct values like that.
Rather, one can classify propositions into something like the following:
1) P is a theorem (these are 'true' propositions)
2) ¬P is a theorem (these are 'false' propositions)
3) ¬¬P is a theorem (these are non-false propositions, but not true)
After this it collapses, because ¬¬¬P → ¬P is a theorem for all P. It's also a theorem that P → ¬¬P, so 'true' propositions are also non-false. But we can't reason from P being non-false to P being true. In fact, ¬¬(P ∨ ¬P) is a theorem for all P, so excluded middle is non-false in intuitionistic logic (this works in general for the propositional calculus; if P is a theorem in the classical propositional calculus, ¬¬P is a theorem in the intuitionistic propositional calculus). So, strictly speaking, I suppose the best way to characterize the situation is that there aren't three truth values (there's no file-not-found that is provably distinct from true or false), but you can't prove that every truth value (or proposition) is either true or false.
Here is an article that probably explains it better than I have (I haven't fully internalized it myself).
Also, to give the subject of the article some credit, if you've found a flaw in Cantor's argument, you may well have found a flaw in Goedel's and Turing's (and Tarksi's) arguments as well, because they are, in an abstract sense, all the same argument.
Finally, I doubt a paraconsistent logic would save the guy, at least if his argument was described correctly. He apparently accepts:
P => ... => R ∧ ¬R
as a valid disproof of P (the so-called external contradiction). But a paraconsistent logic would reject this just as easily as it'd reject
P => ... => P ∧ ¬P
which he takes issue with. So I don't see how that could be the answer to "what is he thinking?"
Posted by: Dan Doel | March 11, 2010 3:07 PM
But I thought that Cantor's proof was NOT a proof by contradiction?
You know, take a function f: N |-> R and show that it isn't surjective.
Posted by: Anonymous | March 11, 2010 4:17 PM
Colin T wrote:
Perez is obviously a crank. If you can't tell, you're an idiot yourself.
Perez starts off with grandiose claims that he's done something original with Goodstein sequences (starting above 2) which is in fact entirely unoriginal. He then claims to have proven Goodstein's theorem in Peano Arithmetic (not in First-Order Arithmetic, as you state, an assertion which doesn't make any sense in this context whatsoever). His claim is mere handwaving.The assertion by a later poster that PA doesn't have finite sets etc is a pointless distraction. PA can code for these things rather routinely, so that's not the level Perez has failed to deliver on.
An intelligent poster would have concluded that they had not bothered to look at it. I guess that's not you.
If the proof is correct it also implies the twin prime conjecture. It also provides a very short proof of the four color theorem!
A more intelligent deduction from a correct PA proof that Goodstein sequences go to zero (something neither you nor Perez is capable of, apparently) is that Paris-Kirby made a mistake. I've been through their paper, and Kaye's textbook treatment. They did not.
Posted by: william e emba | March 12, 2010 12:07 PM