Chapter 1, §§1-3
Chapter 1, §4

I thought it would be useful to have a list of the concepts, methods, and heuristics suggested by the characters of Imre Lakatos’ Proofs and Refutations: The Logic of Mathematical Discovery (1976). It would make positions easier to compare, and it’s nice to have them all in one place. For my third time going through the text, I have decided to compile such a list.  This is not a replacement for actually reading through the dialogue, as I will not be explaining Cauchy’s proof or its counterexamples.

Section 4 focuses on methods for responding to global counterexamples of a proof (the Method of Surrender, the Method of Monster-Barring, the Method of Exception-Barring, the Method of Monster-Adjustment, and the Method of Lemma-Incorporation), as well as some discussion about the Method of Proof and Refutations and why it seems to work.  These are the concepts and methods I found notable from this section.  I don’t claim that my definitions and descriptions are the best—my goal here is to provide something I would have found useful the first time I read through P&R.  I hope writing this out will help my own and others’ understanding.

Name of the Concept / Method / Heuristic
Description or definition of the concept, method, or heuristic.
Context in the text. Also, quotes from the text, if I think something is particularly useful.
If applicable, I will note where this concept, method, heuristic notably reappears in the discussion of other concepts, methods, or heuristics.

§4. Criticism of the Conjecture by Global Counterexamples

Counterexample which is both Global and Local
(See local counterexample and global counterexample.) This is a counterexample which refutes both the main conjecture and at least one of the lemmas/subconjectures of its proof (defn ii).
In §4, several methods are invented to respond to global counterexamples. Some of these methods care that global counterexamples also often happen to be local counterexamples. In §3, we discuss Counterexamples which are Local but not Global. In §5.b-c, we discuss Counterexamples which are Global but not Local.
“ALPHA: I have a counterexample which will falsify your first lemma – but this will also be a counterexample to the main conjecture, i.e. this will be a global counterexample as well.” (13)

(§4.a) Rejection of the conjecture. The method of surrender

Method of Surrender
A counterexample which is both global and local shows the main conjecture and at least one of the lemmas/subconjectures of the proof to be false. In response to this, the Method of Surrender says that we have to give up on both the conjecture and the proof (defn ii), and start over with something totally new. For example, we could propose a new conjecture to solve the problem and try to prove that new conjecture—or we could come up with a new methodology.
This method is criticized on the grounds that it gives up too soon on the conjecture (by proponents of the Method of Monster-Barring, the Method of Exception-Barring, or the Method of Monster-Adjustment), or it is criticized on the grounds that it gives up too soon on the proof (by proponents of the Method of Lemma-Incorporation).
“GAMMA: ... A single counterexample refutes a conjecture as effectively as ten. The conjecture and its proof have completely misfired. Hands up! You have to surrender. Scrap the false conjecture, forget about it and try a radically new approach.” (13)

(§4.B) Rejection of the counterexample. The method of monster–barring

Method of Monster-Barring
Monster-barring is an attempt to explain how a counterexample which is both global and local is not a legitimate counterexample to the proof (defn ii) of the main conjecture. In response to such counterexamples, monster-barring mathematicians seem to strategically redefine the mathematical concepts of the lemmas or main conjecture to claim that the proposed counterexample doesn’t actually apply to the lemma/conjecture. The counterexample is labelled a “monster” because it is said to be unnatural to the true intention and nature of the proof.
Monster-barring adds precision to the definitions of one or more mathematical concepts, with the goal of more precisely specifying which cases contain genuine examples of the mathematical concept(s) and which do not. The precise definition is constructed in such a way that the monstrous-counterexamples turn out to be improper examples of the mathematical concept(s). Because they don’t fit the definitions, the monster cannot be an example of the mathematical concept(s) failing to meet the mathematical relation set out by the lemma/conjecture. The monstrous-counterexample’s claim to refute a lemma/conjecture thus seems improperly aimed at incorrect definitions of the concepts.
The main motivation for this response stems from how the proof has held good for many other cases. People who employ this method believe that the thought-experiment style of proof (defn ii) has proven with certainty (defn i) the main conjecture. They refuse to accept anything as a legitimate counterexample because if something has been proven (defn ii), then it cannot be incorrect—they believe that the problem must therefore be in the counterexample.
People may also be motivated to take up Monster-Barring as an alternative to the Exception-Accepting Method, which may seem so unreasonable that the best option is to bar the exceptions as monsters. (25-26) However, if the only goal is to get away from the Exception-Accepting Method, then there are other methods than Monster-Barring that one can land on. (26)
There are at least two big criticisms to the Method of Monster-Barring.
First, people might say that the monster-barrers are giving new, ad hoc definitions, they are not simply clearing up ambiguities in the original definition. Monster-barrers claim that the concept was always defined by the more precise definition, and that the people proposing the counterexamples are the ones proposing new definitions which stretch the concepts beyond their originally intended qualities (See concept-stretching for a reappraisal of this idea.) But if the monster-barrers “always meant” the more precise definition, why didn’t they simply give their precise definition from the start? Further, because the redefinitions are made ad hoc as a response to monsters, how can the monster-barring mathematician be sure that their newest ad hoc definition has barred all of the monsters that might appear in the future? (They thought their previous definition was good enough, but it wasn’t—why is this any different?) Similar criticism of this ad hoc style applies to the Methods of Exception-Barring.
Second, the method dogmatically refuses to try to improve the proof or the conjecture—monster-barrers are so assured that the proof (def ii) and conjecture are correct that they don’t see how accepting the counterexamples as interesting cases might encourage slight modifications that result in an improved proof/conjecture. (This criticism is used to support the Method of Lemma Incorporation, which tries to take the counterexamples seriously.)
“DELTA: But why accept the counterexample? We proved our conjecture – now it is a theorem. I admit that it clashes with this so–called ‘counterexample’. One of them has to give way. But why should the theorem give way, when it has been proved? It is the ‘criticism’ that should retreat. It is fake criticism.” (14)
“ALPHA: A series of counterexamples, a matching series of definitions, definitions that are alleged to contain nothing new, but to be merely new revelations of the richness of that one old concept, which seems to have as many ‘hidden’ clauses as there are counterexamples.” (21)
“TEACHER: I think we should refuse to accept Delta’s strategy for dealing with global counterexamples.... Using this method one can eliminate any counterexample to the original conjecture by a sometimes deft but always ad hoc redefinition of the polyhedron, of its defining terms, or of the defining terms of its defining terms. We should somehow treat counterexamples with more respect, and not stubbornly exorcise them by dubbing them monsters. Delta’s main mistake is perhaps his dogmatist bias in the interpretation of mathematical proof: he thinks that a proof necessarily proves what it has set out to prove.” (23) To see the Teacher’s non-dogmatic interpretation of ‘proof’, see proof as thought-experiment (defn ii).
Ideas closely related to monster-barring are taken up in §5 with hidden lemmas and §8 with concept stretching’s reappraisal of monster-barring and the concept of error/refutation.

(§4.c) Improving the conjecture by exception-barring methods. Piecemeal exclusions. Strategic withdrawal or playing for safety

Method of Exception-Barring (via Piecemeal Exclusions)
In this method’s response to a counterexample which is both global and local, the mathematician describes a quality of the counterexample and makes a general statement that this quality is the cause of the conflict with the theorem and one or more lemmas (conflict which is both ‘global and local’). The mathematician believes that we have discovered that the theorem/lemmas should not be taken to apply to the set of cases which are defined by that generalized quality of the counterexample. They modify the theorem and lemmas by restricting the theorem and lemmas’ domains to exclude those sets of cases which have the described qualities of the counterexamples. The theorem applies to fewer cases, but now avoids the counterexamples.
The counterexamples (as well the sets of cases which share the counterexamples’ seemingly problematic qualities) are not considered to be ‘monsters’ (as in the Method of Monster-Barring), but neither are they considered to widely refute the conjecture or lemmas in the proof. Instead, they are dubbed ‘exceptions’ which show that the theorem and the challenged lemma(s) are true only within a restricted domain of cases. This wording is used to claim that the original theorem and proof remain safe and intact. The exception-barring mathematician writes off the changes in their domains merely as a recognition that all theorems have their respective domains—not as a change in the theorem or proof.
This method is criticized in two ways.
First, it claims to be able to reach certainty when it is an ad hoc method—the exception-barring mathematician is restricting the domain in response to exceptions (global counterexamples), and is never certain that another exception will not be pointed out. They can never be sure that they have reached a domain which accounts for all exceptions. This method therefore seems like it doesn’t increase our certainty of the conjecture.
Second, this method ignores the proof—it restricts the domain of the conjecture and challenged subconjectures based on qualities of the counterexample, without taking inspiration from the proof (defn ii). What is the purpose of the proof-thought-experiment when it has failed to explain the conjecture with certainty, and only plays a passive role in improving the explanation of the modified conjecture?
Because this method tends to overlook the explanation given by the proof, the mathematician is at risk of overgeneralizing the quality of the counterexample which is in conflict with the conjecture / thought-experiment. Overgeneralizing means the mathematician might over-restrict the domain of the conjecture, leaving out cases which the conjecture accurately describes. This is especially a problem for the Method of Exception-Barring via Strategic Withdrawal.
BETA: I find some aspects of Delta’s arguments silly, but I have come to believe that there is a reasonable kernel to them. It now seems to me that no conjecture is generally valid, but only valid in a certain restricted domain that excludes the exceptions. I am against dubbing these exceptions ‘monsters’ or ‘pathological cases’. That would amount to the methodological decision not to consider these as interesting examples in their own right, worthy of a separate investigation. But I am also against the term ‘counterexample’; it rightly admits them as examples on a par with the supporting examples, but somehow paints them in war-colours, so that ... one panics when facing them, and is tempted to abandon beautiful and ingenious proofs altogether. No: they are just exceptions. (24)
“BETA: ... There are certainly three types of propositions: true ones, hopelessly false ones and hopefully false ones. This last type can be improved into true propositions by adding a restrictive clause which states the exceptions. I never ‘attribute to formulae an undetermined domain of validity. In reality most of the formulae are true only if certain conditions are fulfilled. By determining these conditions and, of course, pinning down precisely the meaning of the terms I use, I make all uncertainty disappear.’ So, as you see, I do not advocate any sort of peaceful coexistence between unimproved formulae and exceptions.” (26)
“TEACHER: You must admit that each new version of your conjecture is only an ad hoc elimination of a counterexample which has just cropped up.... [T]o take notice of these exceptions is all very well, but I think it would be worth while to inject some method into your blind groping for ‘exceptions’.... How can you be sure that you have enumerated all exceptions?” (27)
“TEACHER: ... [Y]our argument forgets about the proof; in guessing the domain of validity of the conjecture, you do not seem to need the proof at all. Surely you do not believe that proofs are redundant?” (29)
“Cauchy’s revolution of rigour rested on the heuristic innovation that the mathematician should not stop at the proof: he should go on and find out what he has proved by enumerating the exceptions, or rather by stating a safe domain where the proof is valid. But neither Cauchy – nor Abel – saw any connection between the two problems. It never occurred to them that if they discover an exception, they should have another look at the proof.” (55)

Method of Exception-Barring (via Strategic Withdrawal)
Like the Method of Exception-Barring (via Piecemeal Exclusions), the proof and theorem are protected by a method of restricting the domain of the proof’s lemmas and the theorem, in an attempt to avoid exceptions. ‘Strategic withdrawal’ is different from ‘piecemeal exclusion’ because ‘piecemeal exclusion’ restricts the domain bit by bit in response to each counterexample / exception, while ‘strategic withdrawal’ takes a big initial leap and makes a large restriction to the domain from the beginning. This large initial restriction is an attempt to restrict the domain of the theorem to something small and (supposedly) safe from further counterexamples / exceptions.
This runs into very similar criticisms as the Method of Exception-Barring via Piecemeal Exclusions.
While it might seem to avoid the ad hoc domain restrictions of the Piecemeal Exclusion Method of Exception-Barring, it still does not guarantee certainty, as someone might still be able to find an exception within the small and purportedly safe domain.
This method’s big (and largely uninformed) domain restriction may leave out cases which are accounted for by the mathematical relationship described by the conjecture—the goal is to find the full domain of the conjecture, not just a safe domain. See the problem of ‘overgeneralizing’ described in the Method of Exception-Barring via Piecemeal Exclusions.
It also ignores the proof in the same way as the Method of Exception-Barring via Piecemeal Exclusions.
“TEACHER: ... [P]iecemeal withdrawal has been replaced by a strategic retreat into a domain hoped to be a stronghold of the conjecture. You are playing for safety. But are you as safe as you claim to be? You still have no guarantee that there will not be any exceptions inside your stronghold. Besides, there is the opposite danger. Could you have withdrawn too radically, leaving lots of Eulerian polyhedra outside the walls? Our original conjecture might have been an overstatement, but your ‘perfected’ thesis looks to me very much like an understatement; yet you still cannot be sure that it is not an overstatement as well.” (28-29)
“TEACHER: ... There is nothing heuristically unsound about this procedure which combines provisional exception-barring with successive proof-analysis and lemma-incorporation.
“BETA: Of course this procedure does not abolish criticism, it only pushes it into the background: instead of directly criticising an over-statement, they criticise an under-statement.” (38)

‘Method’ of Exception-Acceptance
Similar to the ‘Method’ of Satisfactory Demonstration, I have taken liberty in baptizing this as a method and giving it a name—in the dialogue, this merely a position held by one of the characters (Sigma) and is closely related to the Methods of Exception-Barring. Unlike the Exception-Barring Method, the Exception-Accepting Method allows for some propositions to be in a sort of state of being both true and false, with their validity dependent on which cases are being looked at. In many cases, the proposition will be true, but if the cases are ‘exceptions’, as described in the Method of Exception-Barring via Piecemeal Exclusions, then the proposition is false.
This position seems to allow for propositions to be simultaneously true and sometimes false. This is criticized for causing more problems than it solves.
“SIGMA: ... ‘Exception’ is the right expression. ‘There are three sorts of mathematical propositions:
‘1. Those which are always true and to which there are neither restrictions nor exceptions, e.g. the angle sum of all plane triangles is always equal to two right angles.
‘2. Those which rest on some false principle and so cannot be admitted in any way.
‘3. Those which, although they hinge on true principles, nevertheless admit restrictions or exceptions in certain cases....
‘One should not confuse false theorems with theorems subject to some restriction.’” (24)
“DELTA: ... Sigma wants us to admit a third category of propositions that are ‘in principle’ true but ‘admit exceptions in certain cases’. To agree to a peaceful coexistence of theorems and exceptions means to yield to confusion and chaos in mathematics.” (25)

(§4.d) The method of monster-adjustment

Method of Monster-Adjustment
This method claims that there is a way of interpreting the counterexamples which are both global and local such that they are cases of the mathematical concepts fitting the mathematical relation set out by the conjecture. That the case seems to refutes the conjecture, according to this method, is a result of people are taking advantage of an ambiguity in how the case is interpreted. Those people come up with an unnatural, monstrous interpretation of a case, and make it seem like a counterexample when it is not. The method tries to adjust our interpretations of the case away from such monstrous interpretations, and towards interpretations which are ‘rational’ and ‘healthy’—that is, towards interpretations of the cases for which allow the conjecture to hold true.
This position is criticized for not being able to justify why one interpretation is better than another interpretation—the monster-adjusting mathematician may claim it is intuitive, but that doesn’t seem to be good enough reason to ignore the counterexample interpretations. It also fails for similar reasons as the Method of Exception-Barring; it claims to reach certainty (but there is no guarantee that someone in the future will not come up with an un-adjustable counterexample), and it forgets about the proof (there seems to be no need for a proof if achieving certainty merely requires a theorem and monster-adjustment).
“RHO: ... Monsters don’t exist, only monstrous interpretations. One has to purge one’s mind from perverted illusions, one has to learn how to see and how to define correctly what one sees. My method is therapeutic: where you – erroneously – ‘see’ a counterexample, I teach you how to recognise – correctly – an example. I adjust your monstrous vision...” (31)
“KAPPA: But how can you distinguish healthy minds from sick ones, rational from monstrous interpretations?” (32)
“ALPHA: I am willing to admit both interpretations on a par, but one of them will certainly be a global counterexample to Euler’s conjecture. Why admit only the interpretation that is ‘well-adjusted’ to Rho’s preconceptions?” (33)
“BETA: ... The Teacher criticised my conceited view that [the Exception-Barring Method] leads to certainty, and also for forgetting about the proof. These criticisms apply just as much to your ‘monster-adjustment’ as to my ‘exception-barring’.” (39)

(§4.e) Improving the conjecture by the method of lemma-incorporation. Proof-generated theorem versus naive conjecture

Method of Lemma-Incorporation
In response to a counterexample which is both global and local, this method has the mathematician perform a careful proof-analysis of the proof (defn ii), to try to pin down the specific lemma that has been refuted by the counterexample. Once the mathematician has found and described this lemma, they define the set of cases which satisfy the proposition described by the refuted lemma. They then replace the main conjecture with a slightly modified version of the main conjecture, now with its domain restricted to the intersection of the old conjecture’s domain and the set of cases which satisfy the lemma’s proposition.

Here is an example of the method in action:
1. The main conjecture states, “For all cases, there is a mathematical relation R among the mathematical concepts x, y and z.”
2. A counterexample refutes the conjecture by describing a case for which R(x, y, z) is false. Thus, it is a global counterexample.
3. The mathematician carefully examines the proof-analysis. Because they are confident that the logical connections of the proof-analysis are valid, they are looking for the lemma which makes the proof-analysis unsound.
4. Let’s say they find a lemma that states, “For all cases, the proposition V(a, b) is true.” This sticks out to the mathematician because in the case of the counterexample, V(a, b) is false. Thus, the counterexample is also a local counterexample. This falsehood in the assumptions of the proof-analysis seems to be what has led the main conjecture to be false as well.
5. The mathematician checks that this is the most specific subconjecture/lemma that is falsified by the counterexample. (35-36) That is, the lemma from step 4 cannot be decomposed further into sub-lemmas, for which only one of those sub-lemmas is refuted by the counterexample. The mathematician wants to generalize why this specific case of the counterexample has refuted the main conjecture—to figure out what quality of the counterexample is the source of the conjecture’s error. To define that quality, they are searching within the proof-analysis.
6. The mathematician now defines the set s* for which the proposition of the lemma holds true, e.g. “s* is the set of cases for which V(a, b) is true”. The problematic quality of the counterexample is defined as its ‘not being an element of s*’.
7. The mathematician updates the proof-as-thought-experiment and proof-analysis to remove the problematic lemma, and integrates their discovery it into the main conjecture. They integrate it by restricting the domain to cases without the problematic quality. That is, they describe a new conjecture to replace the main conjecture. The new conjecture is simply the main conjecture, but with its domain restricted to the intersection of the main conjecture’s domain (‘all cases’) and the set s* for which the lemma’s proposition is true. The new conjecture is: “For any case in set s*, the proposition R(x, y, z) is true.”
8. If more counterexamples arise, they may repeat the steps 3-7. That means that they will define more sets (s**, s***, ... ) in response to counterexamples which refute other lemmas. Every time they define one of these sets, they remove the falsified lemma and integrate its proposition’s corresponding domain into the replacement of the main conjecture; e.g. “For any case which falls into the intersection of sets s, s*, s**, ... , the conjecture R(x, y, z) is true.”
9. Or, if the conjecture is already a very mature conjecture, it might be that zero counterexamples arise. That means we would never reach step 2. This is also acceptable as part of the method of lemma-incorporation.

The method of lemma-incorporation takes counterexamples as valid refutations of both the conjecture and the lemma. The lemma is removed from the proof, and the main conjecture is falsified. In their place, however, we get a slightly modified proof-analysis and conjecture. The replacement conjecture incorporates the ‘cases in which the removed lemma is false’ by making them restrictions to its domain.
The motivation behind this method was foreshadowed in the criticisms of the other methods. One criticism of other methods was that they claimed to be able to reach certainty while being ad hoc responses to criticisms that people came up with—how can these methods be sure that another criticism won’t arise and challenge what they previously thought was certain? The method of lemma incorporation does not claim to reach certainty, but it claims to improve the theorem and proof in response to global and local counterexamples—it is a good process for mathematical discovery that doesn’t claim to do anything that it can’t.
Another criticism of other methods is that they ignore the proof in their attempts to rescue the conjecture and proof. Lemma-incorporation, like the other methods, tries to save as much of the conjecture and proof as possible (because they have worked pretty well so far and seem like a decent-enough starting point). This method proposes a principled method to keep the good qualities while doing away with the bad, by looking at the proof-analysis to pinpoint what exactly is creating the conflict between the conjecture and the counterexample. This method considers the counterexamples as legitimate sources of contradictions, and uses the counterexample and proof-analysis to sharpen the conjecture/proof. Unlike exception-barrers, this principled manner doesn’t wildly guess at what quality of the counterexample is causing the problem, and tries to update the domain of the conjecture with minimal changes. This is why Beta states, “In fact your method is, in this respect, a limiting case of the exception-barring method...” (37)
There are a few criticisms of this method. First, what if we run into a counterexample which is global but not local? Or, what if the conjecture and its proof are not worth rescuing, because another entirely different conjecture/proof is a better/simpler solution to the problem? In the process of improving the conjecture/proof, we reduce its domain; eventually, another conjecture/proof might seem to be able to describe more content more parsimoniously. Finally, perhaps there are some cases where we shouldn’t consider the counterexample as a valid counterexample, because it stretches our concepts farther than we think we should accept. (See concept-stretching)
“TEACHER: ... I accept this picture-frame as a criticism of the conjecture. I therefore discard the conjecture in its original form as false, but I immediately put forward a modified, restricted version.... Thus we have rescued some of the original hypothesis.” (33-34)
“TEACHER: ... [W]hile the exception-barring method restricted both the domain of the main conjecture and of the guilty lemma to a common domain of safety, thereby accepting the counterexample as criticism both of the main conjecture and of the proof, my method of lemma-incorporation upholds the proof but reduces the domain of the main conjecture to the very domain of the guilty lemma. Or, while a counterexample which is both global and local made the exception-barrer revise both the lemmas and the original conjecture, it makes me revise the original conjecture, but not the lemmas.” (34)
We may see how this method avoids the ad hoc nature of other methods by taking refutations to be a natural part of the method. It uses them as opportunities to improve our knowledge, rather than challenges which endanger it. “TEACHER: You have falsified my improved conjecture, but you have not destroyed my method of improvement. I shall re-examine the proof, and see why it broke down over your polyhedron. There must be another false lemma in the proof.” (35)
“TEACHER: I hope that now all of you see that proofs, even though they may not prove, certainly do help to improve our conjecture. The exception-barrers improved it too, but improving was independent of proving. Our method improves by proving. This intrinsic unity between the ‘logic of discovery’ and the ‘logic of justification’ is the most important aspect of the method of lemma-incorporation.” (37) The zig-zag between discovery, then explanation, then discovery, and so on is an interesting and important observation.
“ALPHA: The lemma-incorporating method relied on the argument – i.e. on the proof – and on nothing else. It virtually summed up the proof in the lemma-incorporating theorem” (41) The statement that this method relies on nothing but the proof only makes sense in comparison to the other methods, which reinterpret the terms or potentially bring in extraneous qualities—the lemma-incorporating method improves itself by taking inspiration from the proof, but also from the counterexamples and the terms used.
“LAMBDA: I would propose to rechristen our ‘method of lemma-incorporation’ the ‘method of proof and refutations’.” (49-50)

Naive Conjecture
The conjecture we begin with as an educated, inductive guess.
“ALPHA: ... [I]t is wrong to assert that ‘the aim of a “problem to prove” is to show conclusively that a certain clearly stated assertion is true, or else to show that it is false’. The real aim of a ‘problem to prove’ should be to improve – in fact, perfect – the original, ‘naive’ conjecture into a genuine ‘theorem’. (41) Alpha is assuming that the method of lemma-incorporation perfects the conjecture to turn it into a proof-generated theorem.

Proof-Generated Theorem
This is produced by applying proper heuristic methods to build up a naive conjecture. We set out to both prove (justify via thought experiment) and disprove (come up with refutations/counterexamples) the naive conjecture. This is said to sharpen and improve the conjecture until it reaches the amount of certainty we need to call it a theorem.
There are multiple heuristic methods that are suggested: the method of lemma-incorporation, the method of proof and refutations, and the method of proofs and refutations. There are also deductive methods at arriving at a theorem, but then the theorem might not seem to have been ‘proof-generated’.

Bibliography

Lakatos, Imre. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press. Kindle Edition.