## Saturday, 27 July 2013

### Re-proving theorems, and the trouble with incorrect proofs of true statements

(Cross-posted at NewAPPS)

“That's the problem with false proofs of true theorems: it's not easy to produce a counterexample.”

This is a comment by Jeffrey Shallit in a post on a purported proof of Fermat’s Last Theorem. (Incidentally, the author of the purported proof comments here at M-Phi occasionally.) In all its apparent simplicity, this remark raises a number of interesting philosophical questions. (Being the pedantic philosopher that I am, I'll change a bit the terminology and use the phrase 'incorrect proof' instead of 'false proof', which I take to be a category mistake.)

First of all, the remark refers to a pervasive but prima facie slightly puzzling feature of mathematical practice: mathematicians often formulate alternative proofs of theorems that have already been proved. This may appear somewhat surprising on the assumption that mathematicians are (solely) in the business of establishing (mathematical) truths; now, if a given truth, a theorem, has already been established, what is the point of going down the same road again? (Or more precisely, going to the same place by taking a different road.) This of course shows that the assumption in question is false: mathematicians are not only interested in theorems, in fact they are mostly interested in proofs. (This is one of the points of Rav’s thought-provoking paper ‘Why do we prove theorems?’)

There are several reasons why mathematicians look for new proofs of previously established theorems, and John Dawson Jr.’s excellent ‘Why do mathematicians re-prove theorems?’ discusses a number of these reasons. The original proof may be seen as too convoluted or not sufficient explanatory – ideally, a proof shows not only that P is the case, but also why P is the case (more on this below). Alternatively, the proof may rely on notions and concepts alien to the formulation and understanding of the theorem itself, giving rise to concerns of purity. Indeed, recall that Colin McLarty motivates his search for a new proof of Fermat’s Last Theorem in these terms: “Fermat’s Last Theorem is just about numbers, so it seems like we ought to be able to prove it by just talking about numbers”. This is not the case of the currently available proof by Wiles, which relies on much heavier machinery.

From the point of view of the dialogical conception of proofs that I’ve been developing, as involving a proponent who wants to establish the conclusion and an opponent who seeks to block the derivation of the conclusion (see here and here), an important reason to re-prove theorems would be related to the persuasive function of proofs. Dawson does mention persuasion in his paper, but he does not adopt an explicit dialogical, multi-agent perspective:
[W]e shall take a proof to be an informal argument whose purpose is to convince those who endeavor to follow it that a certain mathematical statement is true (and, ideally, to explain why it is true). (p. 270)
(In my opinion, this is a fabulous definition of mathematical proofs, except for the fact that it is not explicitly multi-agent.) That is, a given proof, while correct, may still fail to be sufficiently convincing in this sense. I am here reminded of Smale’s original proof of the possibility of eversion of the sphere, which however did not exhibit the process through which the eversion would take place. It was only when Morin built clay models of the stages of the process that it became clear not only that a sphere can be eversed, but also how it can be eversed. (In mathematics, whys often become hows, i.e. how to construct a given entity, how to realize a given process etc.) In fact, it is now known that there are different ways of eversing the sphere.

Still within the dialogical framework, another reason to formulate alternative proofs of theorems are the different commitments and tastes of various audiences. A mathematical proof is a discourse, and even though there is an absolute sense in which a proof is or is not correct, different proofs will be more or less persuasive to different audiences. For example, this observation would explain the search for constructive as well as classical proofs of the same theorems, thus catering for different groups of potential addressees. More generally, different preferences in argumentative styles (not only in theoretical commitments as the ones separating classical and constructivist mathematicians) may also create the space for several proofs of the same theorems.

And here is a final, less ‘noble’ reason for re-proving previously established theorems: such proofs are harder to refute. The mathematician’s preferred approach to refuting a proof is to provide a counterexample, i.e. a situation or construction where the premises hold but the conclusion (the theorem) does not. Now, if providing such a counterexample were the only move available to opponent to block the inference of the conclusion by proponent (a thought that I confess to have entertained for a while), then every proof of a true theorem would be a valid proof, no matter how absurd and defective (such as the one motivating Shallit’s comment above).

This is exactly why a proof cannot be a one-step argument going directly from premises to conclusion (which is, in effect, a necessarily truth-preserving move in the case of true theorems): a proof spells out the intermediate steps, which must be individually perspicuous and explanatory – and yes, also necessarily truth-preserving. So incorrect proofs of true theorems require the additional work of delving into the details of the proof in its different steps in order to reveal where the mistake(s) lie(s) – more work, and often tedious work.

Nobody said it was easy being a mathematical opponent.

1. For some reason I decided a couple of years ago to allow myself to be drawn into a long email exchange with somebody who wrongly thought that he had proved a major theorem. I ran into exactly the difficulty that you refer to, and that presumably Shallit was talking about: that if you point out that B doesn't follow from A, despite the fact that B is probably true, then you may be challenged to provide a counterexample. To someone who isn't fully steeped in the conventions of mathematical proofs, it is very hard to explain why such a challenge is illegitimate. The technique I attempted to use was to identify the underlying wrong argument and try to prove a statement that was definitely false using the same argument. My hope was to persuade the person I was corresponding with of the truth of the false statement and then reveal that it was false. The trouble was, he had enough knowledge to spot many of the false statements and come back at me with, "That argument doesn't work because the conclusion is false." And if I tried to argue that it was the same argument, he could always point to some superficial difference. Also, even if I did temporarily convince him of a false statement, if I then revealed that it was false he could switch to the same tactic.

The remarkable thing about the whole experience was that eventually, after many failed attempts, I did manage to persuade him that he could use his own logic to prove a statement that was manifestly false. His initial reaction to that was that ZFC must be inconsistent, but I eventually got him to agree that if you start from some correct assumptions, make a not fully justified step, and end up with a false conclusion, it is more likely that the fully justified step can't be justified than that ZFC is inconsistent.

I found the exchange interesting (or I wouldn't have persisted with it for so long). A model I like of what a proof is, and described in a book I wrote about ten years ago, is that it is a text written at a high level on the understanding that any part of it can be expanded if necessary -- a process that can be iterated. Most of the time, you don't need to bother expanding, since you know your audience when you write, but in principle if there is anything that your reader doesn't accept, you can write it more fully and in a lower-level language. So there is a kind of "implicit" dialogue that only occasionally becomes actual. The exchange I had was by far the most elaborate actualization of this that I had ever experienced, though my opponent didn't always play by the rules I had in mind (since he wasn't used to expressing himself with the precision that I insisted on).

1. As I hope is obvious, I meant to write "it is more likely that the not fully justified step can't be justified".

2. These are very useful observations, thanks for that. What you describe is squarely in the spirit of my dialogical conceptualization of proofs: the interplay between a proponent and an opponent, and in this case you were the opponent (as I said at the end of the post, it's not easy being an opponent...).

On this picture, there are two basic moves for opponent: to provide a counterexample, and to ask for a given inferential step to be unpacked -- precisely as you describe in your last paragraph. The interesting thing is that there are cases where the counterexample move is not available to opponent, at least not in a straightforward way, so he/she has to resort to other means to refute the purported proof proposed by proponent.

2. Hi Catarina,

"a proof spells out the intermediate steps, which must be individually perspicuous and explanatory – and yes, also necessarily truth-preserving."

Isn't the notion of "intermediate step" equivalent to an inference rule (which can involve CUT: i.e., using a previously proved lemma)? Otherwise, why would an informal proof convince anyone?

This isn't about discovery of proofs, but about whether they serve an epistemic justificatory role.

If I understand right, you disagree that an informal proof given in a maths paper should be, in principle, formalizable: in principle, one should be able to translate the sentences into some $L$ and fill in the intuitive "gaps" by principles like "from $A, A \to B$, infer $B$" and "given $\exists x \phi(x)$, one may name a witness $a$, such that $\phi(a)$", etc.

Is that principle of formalizablity of informal proofs what you don't agree with?

With you on the importance of conceptual explanatoriness, though. We want to know why something is so, and not just that something is so. But it's a very hard topic! "Proofs from the Book", as Erdos called them.

http://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

Cheers,

Jeff

1. Hi Jeff,

I don't disagree with the claim that a mathematical proof should, in principle, be formalizable; but the formalized version is not the proof itself, it is a 'translation' of it in a suitable language. Moreover, there is always the issue of whether a given informal proof is indeed accurately formalized into a given derivation. So ultimately, I'm with Rav and Dawson when they claim that the notion of proof that philosophers of mathematics should talk about does not correspond to a derivation in a given formal system (a debate we've had before!).

This being said, I think there is much to be gained in terms of understanding proofs by means of formalization, so rest assured that I am not a formalization skeptic! :)

2. "Isn't the notion of "intermediate step" equivalent to an inference rule (which can involve CUT: i.e., using a previously proved lemma)? Otherwise, why would an informal proof convince anyone?"

Jeffrey, I believe for Catarina an intermediate step is more like a compressed sequence of successive applications of inference rules, like a high-density pack of thingies. This finds confirmation in what Tim Gowers says: "Most of the time, you don't need to bother expanding, since you know your audience when you write, but in principle if there is anything that your reader doesn't accept, you can write it more fully and in a lower-level language. ". You can then take the application of a single inference rule to be the lowest level in this sense.

3. Hi Antonio,

Yes, that's what I mean by an intermediate step.

Cheers,

Jeff

3. Catarina,

Suppose we have an informal proof - in English, Punjabi or Hebrew, etc., - a finite sequence of interpreted sentences, say,

$S_1, \dots, S_n$.

(I ignore diagram proofs ... which I think are important and interesting).

We formalize this by a mapping

$^{\circ} : Informal-Mathlish \to L$

giving:

$(S_1)^{\circ}, \dots, (S_n)^{\circ}$.

This can be expanded into a fully formalized proof, in "machine code".

Is that the picture you do agree with?

Cheers.

Jeff

1. This is an important and difficult question, but I don't think it is directly related to the core of the post above. Well, maybe it is, because in the case of formalized derivations, it is much easier to refute a derivation, namely by pointing out that there is an incorrect application of a rule of inference of the formal system along the way. But here I'm taking as my starting point (which is argued for in more detail especially by Rav, but also to some extent by Dawson) the idea that a mathematical proof is first and foremost a so-called informal proof, and it is only in a derivative sense that a derivation in a formal system can be said to be a 'proof'.

Maybe when I'm back from my vacation I will try to write a blog post more precisely on this issue :) I don't think I've ever spelled out in detail my reasons to side with Rav and Dawson, but for the most part it has to do with the trivial observation that mathematical proofs as presented in math journals are not as such derivations in formal systems (even if they can be *turned* into such derivations).

2. I've just found this recent post by Dick Lipton, dealing with: formal vs. informal proofs, Homotopy Type Theory's take on proofs, Mochizuki, proof checking within mathematical practice, etc…

http://rjlipton.wordpress.com/2013/07/14/surely-you-are-joking/

Catarina, you may find this particularly interesting:
http://www.informatik.uni-trier.de/~ley/pers/hd/g/Ganesalingam:Mohan

4. Hi Catarina,

Yes, I agree entirely with Dawson and Rav.

Cheers,

Jeff

5. Hi Catarina,

To be more exact on our difference: I think you identify a normative, multi-agent, epistemic role for informal proofs, P. Call this role R. Then your view is that a proof is something filling this role.

Whereas I say that a proof is whatever it is, even if it doesn't fill this role R. There may exist proofs that don't satisfy your role criterion. For example, they might be trillions of pages long. A proof might be infinitely long. A proof might involve concepts which humans cannot grasp because of their cognitive limitations.

(Actually, I think of proofs *semantically*: what matters is their meaning.)

For example, Mochizuki's text does not fill this defined normative, multi-agent, epistemic role, as all agree.

On your view, it is therefore "wrong".

http://m-phi.blogspot.co.uk/2013/05/whats-wrong-with-mochizukis-proof-of.html

But, on my view, no one has given a reason for thinking Mochizuki's proof is wrong. It may be right. No one knows; possibly not even Mochizuki.

Cheers,

Jeff

1. Yes, one can say I hold a 'functionalist' conception of mathematical proofs, and if a purported proof does not perform its function, then it fails as a proof. Another way to say the same thing is that I am interested in proofs insofar as they perform a certain cognitive function for us humans, i.e. proofs as cognitive tools of knowledge transfer.

Sorry to be brief, but I'm in the middle of packing here. And everybody else: I won't be able to reply to comments for the next 10 days or so, but by all means, do keep the debate going if you feel like it.

2. Hi Catarina, have a good trip!

So, let this cognitive role R be defined as follows:

Definition: an informal text $p$ occupies the role R if and only if $p$ convinces those who endeavor to follow it that a certain mathematical statement A is true (and, ideally, to explain why it is true)

Suppose $p$ occupies this role R. Does it follow that the statement A is true?

That is, is the following argument valid?

(Premise) p convinces those who endeavor to follow it that a certain mathematical statement A is true
--------------
(Conclusion) Therefore, A is true.

Cheers,

Jeff

3. Re Catarina's remarks on Rav, I think that for him the important point is not that informal proofs are very different from formal proofs ('derivations'). Rather he claims that the process Tim Gowers talks of, of successively formalising more sections of a (correct) proof, to greater and greater 'depths', is not guaranteed after a finite time to result in a derivation. He takes the latter to be finite, characterised in the usual recursive fashion.

I agree with you Jeff that derivations can be infinitely long (though not that they are semantical, here I am with Rav). That we will never confront such entities is no objection: even in finitary formal languages, all but an insignificant number of expressions and derivations will have more steps or sub-formulae than the estimated number of neutrinos in the universe. Derivations are abstract mathematical entities (whatever, if anything, they are). This provides a route for blocking Rav's argument.

One then naturally wants to ask what useful role derivations play in mathematics, especially if they can be infinitary objects. A good question indeed. Aren't they just boring old well-understood objects: numbers, or sequences of set-theoretic objects, or things which can be coded by them.

One useful role could be philosophical: to block objections to formalism, for example, from limitative results such as Godel's. Those results might also be used to bolster Rav's argument that, relative to an informal axiomatisation taken as fixing a mathematical domain, not all informal proofs will be formalisable; again appeal to infinitary languages and logics provides a way of countering the argument.

Formalisation also has increasingly important practical roles in mathematics, via theorem-proving programs such as Isabelle and Coq. To be sure no machine running these will ever output a token of a proof with more steps than all the neutrinos there are and ever were or will be. But for any formal language or system, we can introduce a new language or system which abbreviates the former. Though no such abbreviatory system can bring all expressions down to feasible length, there is no bound (finite or infinite) to the size of a formal expression which can be feasibly abbreviated by some system, or other. Informal proofs concerning the powers of formal systems can help us construct formal systems and decide on their soundness, completeness and so forth guiding us on which to use, including in automated theorem-provers.

6. "I'll change a bit the terminology and use the phrase 'incorrect proof' instead of 'false proof', which I take to be a category mistake.)"

"Maverick Philosopher" Bill Vallicella calls those alienans adjectives. For example red leather is leather and Corinthian leather is leather, but imitation leather is not leather.

I don't see much different between a false proof and an incorrect proof. Both are alienans adjectives, negating rather than modifying their associated noun.

7. Hi Alan, many thanks!

But Rav's view is the same as mine:

"Let us fix our terminology to understand by proof a conceptual proof of customary mathematical discourse, having an irreducible semantic content, and distinguish it from derivation, which is a syntactic object of some formal system. "

That is, proofs have semantic content, and analysing this turns out to be a major problem.

Cheers,

Jeff

1. Jeff: (been away for a few days hence the delay).
Yes that's certainly true, the quotation you give encapsulates something crucial for Rav's argument. I think he has a tendency to slide from a) what makes a structure a proof is something purely formal/syntatic to b) the strings in the structure must lack meaning. I think b) doesn't follow from a). Terminological matters re 'proof' and 'derivation' aren't all that important but I think that in lots of low-grade mathematical proofs (the sort of thing you would get in high-school books, the workings of engineers etc.) what we have are formal derivations (true we usually omit obvious steps but they could be filled in mechanically) in the sense that purely formal considerations determine whether they are correct derivations. So in that sense, it looks like I disagree with you. I'm saying meaning doesn't matter, in determining what's a correct derivation. But that doesn't mean the sentences in the derivations lack meaning.

Of course in high-grade maths, proofs in maths journals etc, it's not obvious, to say the very least, that there are purely formal rules determining which purported proofs really are proofs or that there are determinate transformation procedures which will turn correct informal proofs into derivations whose correctness is determined formally. That's the, or at least, a, key issue it seems to me, and a difficult one.

2. Thanks, Alan - seems pretty much right. Algorithmic checkability is very important; we might weaken the demand if we consider $\omega$-proofs, say, but the finite fragments should be checkable. So, it seems to me that any attempt to reject the usual structural analyses (derivations, trees, tableaux, etc.) of the notion of a proof is a non-starter. Even if $A$ does imply $B$ (in the standard sense: $B$ is true in every interpretation that makes $A$ true), the statement "$A$, therefore $B$" cannot count as a proof - except perhaps for God! A proof must be a structure that links $A$ to $B$, via smaller and smaller links, eventually coming to minimal (sound) ones. If there is such a structure, then anyone who does follow it will thereby recognise that $B$ follows from $A$ (Dawson's demand).

Still, the interesting questions here seem to be about semantic and cognitive issues though. If we examine, say, six proofs of $B$ from $A$, some may be more significant or explanatory than others.

I've just reminded myself of something I read probably 12 years ago or so: Robin Chapman has a note giving 14 proofs of

$\sum^{\infty}_{n=1} \frac{1}{n^2} = \frac{\pi^2}{6}$

http://empslocal.ex.ac.uk/people/staff/rjchapma/etc/zeta2.pdf

Cheers,

Jeff

8. Having said that, and agreed with the importance of semantic content, I do have several points of disagreement with Rav, because he makes some mistakes. For example, Rav does not understand Tarski's analysis of concept of truth: the notion "truth in a model" does not appear in his Tarski's 1936 paper, "On the Concept of Truth in Formalized Languages".

A definition of truth for an interpreted language $L$ is adequate when it implies the T-sentences, which involve a name of the object language sentence $S$ and a translation of it into the metalanguage. This translation must preserve semantic content.

The language $L$ for which truth is defined is, and must be (as Tarski emphasised) interpreted. This confusion about interpreted languages is very common, and is a mistake in Rav's paper.

Cheers,

Jeff

9. If proof is simply an informal argument intended to convince an audience, then we shouldn't care much who that intended audience is. As you say, different proofs may be intended to be convincing arguments to different audiences.

But I'm wondering about small children. (I am a classroom teacher.) First, there are many informal arguments that would be convincing to a young student that would be seen as mathematically problematic for a more mature mathematician. Would these arguments be accepted as proofs on your thinking?

More generally: what about bad arguments that are convincing? (e.g. Arguments that contain false premises or incorrect inferences that nonetheless fool an entire audience.) On what grounds can you argue that these arguments aren't proofs, given your definition? (Perhaps by arguing that these proofs fail to be convincing in the broad sense, since eventually someone will find the error and unconvince everyone? Or perhaps you take a pragmatic stand, and call the argument a proof until an error is revealed?)