On the largest mathematical proof -- aka the Enormous Theorem
I came across an interesting short note about the largest existing mathematical proof, composed of 15.000 pages; it involved more than 100 mathematicians in its formulation. I wonder if there's an entry for it in the Guinness Book of Records? There should be!
The Enormous Theorem concerns groups, which in mathematics can refer to a collection of symmetries, such as the rotations of a square that produce the original shape. Some groups can be built from others but, rather like prime numbers or the chemical elements, "finite simple" groups are elemental.There are an infinite number of finite simple groups but a finite number of families to which they belong. Mathematicians have been studying groups since the 19th century, but the Enormous Theorem wasn't proposed until around 1971, when mathematician Daniel Gorenstein of Rutgers University in New Jersey devised a plan to identify all the finite simple groups, divide them into families and prove that no others could exist.
Pshaw. In my "There are non-circular paradoxes, but Yablo's isn't one of them", I give a proof that is omega-cubed-plus-two lines long. The so-called 'Enormous Theorem' is puny in comparison.
ReplyDeleteKidding, of course. But this does raise the issue of what does, and doesn't, count as a proof in the relevant sense. If the sum of all the papers that went into the 'Enormous Theorem' counts as a single proof, then why doesn't the sum of all mathematical papers whatsoever count as a proof of the conjunction of the individual theorems proved? That would be one big-@$$ proof!
Of course, there is something interesting and important about the "Enormous Theorem" that is (presumably) lacking in the monster conjunctive 'proof' I just described. But it seems non-trivial to say exactly what that something is.
A connected issue, of course, has to do with the difference between giving a proof explicitly (which has been done - at least we think - in the case of the "Enormous Theorem" versus merely proving that a proof exists. If all we need is the latter, then we can of course identify proofs that are much longer than the "Enormous Proof" - for example, the proof discussed in Boolos' "A Curious Inference", which contains more steps than there are particles in the universe.
Yes, this is the kind of thing I had in mind, that the Enormous Theorem could raise interesting questions on the metaphysics of proofs:
ReplyDelete- what are the criteria of individuation for proofs? Like you said, put any two proofs together and you have a conjunctive proofs :) And yet, mathematicians do seem to regard the Enormous as ONE proof, something that makes a coherent whole.
- are we talking actual or possible proofs? And what do these concepts mean anyway with respect to proofs? These are points that are often raised in connection with constructivism, but they show up here too. Is the sketch of a proof is sufficient, like in the Boolos case, then it's not obvious that the Enormous is the largest one around. So probably they mean fully explicit, worked-out proofs; but then, lots of other arguments that seem to be regarded as 'proofs' by mathematicians would not count as proofs.
Roy, Catarina, totally agree with you regarding the non-settled issue about what is needed to be a proof (enourmous or not). For example, must there be a target that makes the whole demonstration coherent or intelligible?
ReplyDeleteMy own thoughts about this matter aren't so clear. I'm somehow inspired by Mercier & Sperber's sketch of ways of reasoning's as 'intuitive' or 'proper' one. From this point of view it follows that obviously we have many 'intuitive' thoughts about proofs and mathematical and logical inferences. But, for us as professional community to be sure that we are constructing sound knowledge, our standards require proofs ('proper' reasoning). [Though it isn't clear that when professionals talk about proofs they mean 'finitist proofs'] However, as M&S claim in their paper, when we accept a given argument (a (in)finite proof) we ultimately rely on 'intuitive' judgments "that certain conclusions follow from certain premises".
So, when for example you're discussing a proof including omega-rule (and therefore infinite steps that cannot be followed by any man -but by Zeus) it doesn't seem to me to be misleading to say "But, really, don't you 'see' the proof?" The key issue would be whether it is legitimate to ask others to share our intuition about metarepresentational matters, i.e. that the omega-rule obviously, and correctly, leads to statements that need an infinity of steps to be secure.
You can read about Alexandre Borovik's worrying prediction that in about 20 years time only one person will have a proper overview of the whole proof here.
ReplyDeleteIf this is right, what happens when she passes on and yet people are still relying on the result? As Alexandre told me, repair jobs still continue on the proof. The thought is that it's not finished in the sense that a fully rigorous proof has been written out. Rather it's finished in the sense that whenever anyone points to a gap, there's someone who knows how to reassure them.
Hello Damian,
ReplyDelete"The key issue would be whether it is legitimate to ask others to share our intuition about metarepresentational matters, i.e. that the omega-rule obviously, and correctly, leads to statements that need an infinity of steps to be secure."
There's an M-Phi post from a few months back proving that Peano arithmetic with the omega-rule is complete.
http://m-phi.blogspot.com/2011/03/completeness-of-pa-with-omega-rule.html
Can you say what you mean though in relation to this?
Jeff
Two simply stated, but hard-to-answer questions that I think focus two of the central issues here:
ReplyDelete(i) Is the omega-cubed plus two line long 'proof' I give in my Yablo paradox paper mentioned above a proof, in some substantial sense of the word (for most of you who haven't read it, it involves constructing the Yablo paradox in terms of infinite conjunctions and then deriving a contradiction directly utilizing infinitary versions of and-introduction and and-elimination. In the paper, I 'give' the proof, but at a number of points I indicate that one repeats the general construction just carried out for all remaining numbers using the mathematically useful "..."
(ii) Is the Enormous Theorem a proof? Is it merely warrant for believing that we could (given enough time, effort, and interest) construct a proof? Does it somehow 'point to' a complete, abstract proof? (Is it Azzouni that says something like this about informal proofs? I forget).
Roy,
ReplyDelete"(i) Is the omega-cubed plus two line long 'proof' I give in my Yablo paradox paper mentioned above a proof, in some substantial sense of the word."
Yes! We already know that humans, being very finite, can only survey the tiniest proofs. But the shortest tableau proof for the following logically true statement,
"If there are 1001 dalmatians and 1000 food bowls and each dalmatian uses exactly one food bowl, then at least two dalmatians share the same food bowl"
has length at least $10^9$ symbols (because on my calculation, the number of symbols is at least $n^3$, if the parameter is $n$; unfortunately, I've forgotten how I did the calculation). A billion symbols is about 20,000 pages.
This is an example of the kind Boolos 1987 discusses, but nowhere near as big. The advantage is that everyone I ask agrees that the statement is correct! (It's an instance of the Pigeonhole Principle transcribed as a first-order logical truth.)
Incidentally, I think an upper bound for the proof of any arithmetic truth in PA using the omega rule is $\omega^2$. (I.e., use the $\omega$ rule itself $\omega$-many times.)
"A billion symbols is about 20,000 pages."
ReplyDeleteOops. I meant to write: about 200,000 pages.
Jeffrey
ReplyDeletewhen I wrote my comment I intended to say the following. (Maybe I'm making some conceptual mistakes here -but please let me know)
I think a rough finitist won't accept the kind of 'proofs' you allow in PA-omega (would he?) nor the proof given by Roy in his Yablo paper. But why? Not because his life would be too short to check all the steps of the demostration, but because there isn't any (arbitrarely big and) finite amount of time that would suffice to check the complete derivation -for him or for any computer.
That's why I said that there is some disagreement between that imaginary opponent and someone who believes (as I do, as far as I know) that omega-proofs like Roy's are substantially well-conceived and real proofs. Where does the disagreement rely? Well, puted in Mercier & Sperber's terms, I have the intuition that some conclusions (the ones that are the output of omega-proofs) follow from certain premises (in fact, from omega many premises alltogether) which the imaginary rough finitist does not have. This kind of intuitions -about metarepresentations- seem to be the ultimate argumentative ground in which any evaluation of an argument must rely.
Two more things.
1) In conversation some colleagues are always reluctant to accept the omega-rule as a logical rule, and therefore to accept it in context of logical demonstrations (regarding Yablo's paradox, for instance). So one could support it's application for mathematical needs, but not for logical problems. For that very reason I've heard some of them reject logical derivations involving the second-order Induction Axiom. So, I don't know yet what to answer, but it looks controversial.
2) I don't understand (but it is surely my fault): could you make some clarifications about PA-omega and it's own Gödel sentence? What relation do PA-omega and non-standard models have?
Damian
Hello Damián,
ReplyDeleteJust quickly on the second question,
"2)..could you make some clarifications about PA-omega and it's own Gödel sentence? What relation do PA-omega and non-standard models have?"
Yes, $PA^{\omega}$ is not a recursively axiomatizable formal system. In particular, the property "$(\theta_0, \dots, \theta_a)$ is a derivation in $PA^{\omega}$" is not arithmetically definable. Hence, there is no Gödel sentence (this is essentially the same reason as why there is no Gödel sentence for $Th(\mathbb{N})$).
As a theory, $PA^{\omega}$ is the same as true arithmetic - $Th(\mathbb{N})$. So, they have the same non-standard models.
"I think a rough finitist won't accept the kind of 'proofs' you allow in PA-omega (would he?) nor the proof given by Roy in his Yablo paper. But why? Not because his life would be too short to check all the steps of the demostration, but because there isn't any (arbitrarely big and) finite amount of time that would suffice to check the complete derivation -for him or for any computer."
ReplyDeleteRight. The proofs are not finitary mathematical objects. As I mentioned above, the property of being a derivation in $PA^{\omega}$ is not even definable in arithmetic. Its definition requires second-order arithmetic.
But the mere existence of an infinitely long proof (a mathematical object) need not imply that some human being or computer can recognize it as a proof (this is an epistemological or even psychological issue). Still, one can have recognizable finite metaproofs about these infinite mathematical objects.
Jeff
"1) In conversation some colleagues are always reluctant to accept the omega-rule as a logical rule"
ReplyDeleteI agree. It is not a logical rule; its character is that of a genuine mathematical principle rather than finitary logical rule (though this may be a partly terminological point).
Instead of the $\omega$-rule, one can instead use a much weaker single scheme, known as the uniform reflection scheme over a theory $T$ in the language of arithmetic (called $RFN(T)$),
$\forall n(Prov_T(\ulcorner \phi(\dot{n}) \urcorner) \rightarrow \phi(n))$
If $T$ is a recursively axiomatized extension of $PA$, then $T + RFN(T)$ is a non-conservative extension of $T$.
Jeff
Oops. I should have said "recursively axiomatized consistent extension of $PA$ ...".
ReplyDeleteDoes it matter whether the proof is set-sized or proper class sized? Along the same lines as the proof in my Yablo paper, one can 'construct' a Yablo-like paradox where you have a sequence of statements:
ReplyDeleteYi
for each ordinal i, and where each statement Yi is equivalent to the predication of falsity to all Yj for j > i. The proof then has proper class many steps.
My intuition is that this is a proof, and further that I can see that it is a proof (based on my description of it abstractly) even if I could never construct it (nor presumably could anyone, regardless of how liberal one wants to be about supertasks!)
By the way, I should have mentioned in connection to the last comment - the proof I give in my Yablo paradox paper is a supertask (since all countable ordinals are embeddable in the real line). The proper class sized version, of course, is not. Does this matter?
ReplyDeleteRoy, I'd say that short or feasible derivations have epistemic significance: they can be grasped/recognized by a human mind (on average and other things being equal, as some minds may have better memory resources, pattern recognition, etc., than others).
ReplyDeleteStill, the assumption that non-graspability of Fs implies the non-existence of Fs is form of idealism ("every F can be grasped", cf., Berkeley's esse est percipi), which is dodgy.
On the more specific point, I don't see an ontological problem with infinitely long derivations, or even class-sized ones. There is a graspability problem when we get beyond 10,000 pages, say; but non-graspability doesn't imply non-existence. As with the examples given in Boolos 1987 (and myself in Analysis 2005), there are logical truths whose derivations in FOL are ungraspable, but which can be proved valid using ordinary mathematics, in a page or less, or a bit more, depending on one's favourite setup. More generally, speed-up phenomena provide examples of (classes of) theorems feasibly provable in $T_1$ but having no short proof in $T_2$, and even if $T_1$ conservatively extends $T_2$.
Jeff