What is the nature of proof in mathematics?

Question

Preamble: I think we have this sort of questions, where we are required to find a solution for them. For example, what is the area of a circle?. I think the way to solve these problems is to try to find similar problems. If the solution to the similar problems does not apply, then we try to figure out why, and this might help us to find the right solution.

However, we have another type of problems, where we need to establish the truth of something. For example, proving a theorem, which are in nature different from the first type of questions. I do not think the same approach as before can be applied for these problems. I do not think there exist recipes or structures to follow either once it comes to proving things, but I do think there should be certain strategies or plan as you wish to approach these in mathematics?

Questions: Based on the above introduction, I have the following questions:

1. Do you think we as humans in general use certain prove strategies to prove things?

   Regardless of the topic being mathematics or any other topics, do you think we have finite and limited ways of approaching proof-related problems? For example, see this.

2. If the above is true this means they are certain strategies that we need to follow, where do you think the creativity comes in?

   If they are certain strategies to follow, where do you think the creativity comes in? Does it come in come in when we try to apply a given strategy to a problem.

3. How does proving things in mathematics differ from real world?

For example, in real life if we want to prove someone is innocent we simply find a group of trusted witnesses to testify someone is innocent. In other words, to prove q in real life, we can easily find a p which results in q and it is not very challenging. What makes this challenging in mathematics though? Is it because we are not acquainted with mathematics world, the way we are with real world and once we become well familiar we can easily establish truth in mathematics world too?

Update: Based on the provided suggestions I would like to narrow down the question a bit further. If we think of a proof as a chain of logical arguments, which starts from the set of axioms (assumptions) and reaches some conclusions (theorems), then how would mathematician try to establish this logical link between axioms and theorems (questions 1 and 2 above relate to this argument).

Furthermore, it seems establishing this link between assumptions to the theorems is much easier in real life, regardless of the actual truth of the assumptions (question 3 above relates to this argument)

Please see @MarkOxford's answer and comments there for further clarification.

Answer 1

I'm not sure to fully understand your questions but I will try an answer biased by recent formal results in Proof Theory and my viewpoint of a computer scientist. So it won't be a very "philosophical" answer in the sense that I don't fully rely on philosophical references.

Note that the nature of proof is not clear at all and it's still something we seek. We actually have several answers for that.

Do you think we as humans in general use certain prove strategies to prove things ?

Toward a formalization of proof. Mathematician were already making proofs a long time before formal logic appeared. Around the 19th and 20th century a lot of system of proofs were established according our conception of proof.

• Frege with his Begriffsschrift started from the conception of Logic provided by Aristotle and the Stoics.

• Hilbert made a system were the modus ponens was the only rule and we try to derive proofs from already-established axioms

• More interesting : Gentzen first made a system based on the use of logic in mathematical methods called the Natural Deduction (because it reproduces the empirical use of logic by humans). When proving things we introduce connectives and eliminate them later :

  • from A and B we can reduce A /\ B (definition of "and")
  • from A /\ B we can either deduce A or B (use of "and")

With such a system we can restrict the space of proofs within the introduction and elimination of a finite set of connectives.

So yes, we use certain strategies to prove things. Another questions :

• Where do these rules come from ?
• Is logic more than that ?
• Why do we use these rules and not other ones ?

The first two questions can be answered, the last one may be a question of psychology or biology (there are actually some litterature about it).

If the above is true this means they are certain strategies that we need to follow, where do you think the creativity comes in ?

A fine analysis of logic. Coming back to Gentzen, he observed that deductions from the Natural Deduction system could be reduced/simplified : when we introduce a connective and eliminate it right after, we're making a "deviation" which is not necessary.

He was unable to prove that so he made another system called the Sequent Calculus. That system wasn't based on the study of the use of proof but on an analyze of natural deduction and logic. The Sequent Calculus analyze the deep structure of logic and its symmetries according to a duality hypothesis/conclusion rather than introduction/elimination or definition/use.

The last system was adequate enough to make the concept of "deviation" explicit : it's called the cut rule and that's were creativity comes in (but he didn't know that).

Creativity and the use of lemmas. The cut rule is expressed as follow : from Γ ⊢ Δ,A (left = conjunction of hypothesis, right = disjunction of conclusions, the Greek letters are multiset of formulas) and Σ,A ⊢ Π we can deduce Γ,Σ ⊢ Π,Δ. Reading the rule in the reverse direction, it means that if we want to prove Γ,Σ ⊢ Π,Δ (which is anything you want) you can introduce an arbitrary A providing that A can be proved with some hypothesis Γ you have and that giving A and some eventually some other hypothesis Σ you have you can prove what you wanted.

The cut rule is actually the use of lemma in mathematics. When you want to prove something, prove a lemma A and use it.

Following his goal, Gentzen proved the use of the cut rule (representing deviations now called "cuts") could be removed. It means that we can prove things without lemmas and only with pure application of logical rules. Only one problem : reducing a proof with cuts can lead to an explosion of complexity with proof of huge size (sometimes of an absurd size).

A concrete example of cuts. Say you want to prove that 5+3 is the same as 3+5. You can either use "pure application of rules" leading to the result of 8 in both sides OR use creativity/a lemma/the cut rule : we prove that addition is commutative (for all n and m, n+m = m+n) and that the commutativity of addition prove what we want.

We make a deviation that is not necessary but more creative, more useful, more interesting...

How does proving things in mathematics differ from real world? [...] In other words, to prove q in real life, we can easily find a p which results in q and it is not very challenging. What makes this challenging in mathematics though

Hum... I'm not sure to understand that one. In your example the reason may be that the space of search is finite when in mathematics it can be infinite. But it's not a general thing if in "real world" you include results about physics for instance.

Epilogue : Toward the deep structure of logic

The origin of rules. In the 20th century, logicians and computer scientists discovered something amazing called the Curry-Howard isomorphism. It states that :

• The proof of some logical systems actually correspond exactly to computer programs of some system (The Intuitionistic Natural Deduction corresponds to the Lambda Calculus).

• For the corresponding systems, the formula proved by a proof can be seen as the type of the corresponding program.

• The elimination of cuts can be seen as the execution of programs

There're not a lot of litterature about that but I think that correspondence gives a "natural" status the logical rules as coming from the natural concept of "computation".

This paradigm interpret logical rules as programs constructions : logical implication is seen as a function in a programming language, conjunction as a pair, disjunction as a sum type/algebraic type...

An even finer analysis of logic. Recently logicians like Jean-Yves Girard tried to look even deeper in the analysis of logic : in most proof systems we have a rule to "duplicate" and "erase formula". For instance, giving A ⊢ A, the following still holds : A,A ⊢ A. And giving A,A ⊢ A we have A ⊢ A which still holds. What if we remove these rules and see proofs like chemical reactions where we consume formulas ? It led to Linear Logic which eventually reintroduce infinity/staticity of truth with new operators !A and ?A.

Linear Logic finally led to a new dynamical and interactive status for proofs which is still being investigated nowadays. That new approach fully rely on the concept of cut elimination which is now seen as interaction, a central idea of current research in Proof Theory.

Toward a fully internal logic. As you said, the problem of axioms and theorem can be problematic. In logic we rely too much on an external world. Logicians tried to make an internal logic called Ludics which is also currently under investigations. Ludics have a concept of "partial" proofs where two partial proofs interact together with one trying to prove a formula A and the other the dual/negation and only one win.

The denial. Recent researches in Proof Theory interacts a lot with computer science and tends to give a preferential treatment to logic as explained by computation.

A quite controversial question is : what about the logical systems where the theorem of cut elimination (cuts can be eliminated) doesn't hold and which doesn't have any corresponding system in Computer Science ? Are they really "valid" ?

Some systems in "philosophical logics" doesn't enjoy the theorem of cut elimination but it's another debate.

Summary

• A proof can be seen as a program of some programming system in Computer Science

• Computer Science and the cut rule give really interesting directions

• The cut rule and the cut elimination procedure may the core of Logic

• Without considering the use of logic by human we can study the formal structure of logic even deeper and finer

• Formal results in Computer Science, Proof Theory and Mathematics should interact more with philosophers : philosophical ideas are unknown to most of the former and computation and technical details to the latter.

Answer 2

This is a very broad question; but perhaps by focussing on the contrast you suggest between legal and mathematical proofs, we can narrow it down a bit. In the very least, this may give you some ideas where you might start your search. So, you say:

“in real life if we want to prove someone is innocent we simply find a group of trusted witnesses to testify someone is innocent. In other words, to prove q in real life, we can easily find a p which results in q and it is not very challenging. What makes this challenging in mathematics though?”

Three brief caveats. (i) I’ll continue to use ‘proof’ for both the mathematical and the legal thing, though it would probably best to use two different words. (ii) Careful not to drift off into the psychological, when asking why we find legal proofs easier, and whether we have cognitive strategies for approaching proofs. (iii) I’m not sure why you say legal proofs are easier than mathematical ones one: there are simple proofs in maths, and hard proofs in law.

Now, if you are pointing to the fact that legal proofs, but not mathematical proofs, rely on empirical evidence, you could look into the A Priori vs A Posteriori distinction. Frege’s ‘Foundations of Arithmetic’ may be a good place to start. (Note that some argue that mathematical knowledge can be derived from empirical evidence: e.g., the Goldbach conjecture is arguably supported by the computers who are checking it. Alexander Paseau has written on this.)

If you are more particularly wondering about the epistemic status of witness testimonies, you could look into the literature on Knowledge by Testimony. (Note that a lot of people’s mathematical knowledge probably does come from testimony: I know that 2+2=4 because my mom/teachers told me, not because I proved it.)

Since you talk about p ‘resulting in’ q, you may also want to look at the literature on Deductive, Inductive, and Abductive Proofs/Reasoning. Mathematical proofs are deductive, of course; but it’s not obvious that legal proofs are. (If you haven’t done so yet, it may also help to look at some mathematical proofs ‘in action’. E.g. Enderton’s ‘A Mathematical Introduction to Logic’ is formally rigorous and highly readable. Or have a look at Robbins and Courant’s ‘What is Mathematics’. For a more philosophical perspective, see e.g. Giaquinto’s ‘The Search for Certainty’.)

Since you draw a distinction between the mathematical world and the real world, have a look at the Realism vs Nominalism debate. One challenge the Realist faces, is the question of how we can know about mathematics if numbers are abstract objects.

Finally, another way to approach the nature of the ‘mathematical world’ may be to ask about the Status of the Axioms – e.g.: How do we know ‘basic truths’? See e.g. Maddy’s ‘Defending the Axioms’ and Mary Leng’s review thereof.

These are just a few pointers, none of which answer your question directly. However, as I said above, if you can narrow the question down a bit, you’re much more likely to find a satisfying answer.

Answer 3

(I am hoping to give a reasonably short answer by choosing a specific perspective, instead of attempting an overview.)

Intuitionism was put forward as a way to address the problems people had with mathematical Platonism as they tried to formalize verbal logic. They found things like Russel's paradox were harder to evade than one might assume. And that dealt a deep blow to the ordinary, Platonic way of looking at the process of mathematics.

Intuitionists pointed out that Platonism might be a result rather than the real cause of what goes on in the mathematical process. That mathematics is not about absolutely stable ideas, but that it seeks out those ideas for the use of the other sciences.

One interpretation of Neo-Intuitionism is that mathematics is a real experimental science. It is the purest form of psychology. It experimentally determines what intuitive concepts humans cannot easily let go of once they have them, and how those concepts combine well or badly. So mathematics does not study some fixed realm of nature outside ourselves, it studies human thought and creative processes.

1. This assumes 'yes' to your question 1. But it does not say what they are. They are seem to exist because we find them. And we assume there are more of them because we keep finding them.

It does this the same way chemistry does, by taking products that it has already established its ability to reliably create and using them together in a contrived environment.

Proof, then, is not a specific thing that can be established and fixed. It is based upon what stable intuitions can be pulled in that are not readily undermined, and how they can be combined according to patterns that we find difficult to reject.

(The side effect of this view for which Intuitionism is most famous is that we should be tentative about the reach of 'proven-ness', and not assume that all the things we prove will be entirely consistent with one another. We find contradictions difficult psychologically, so we should avoid them. But we have no reason to believe that human intuition is internally consistent.)

2. This gives us a clear answer to your second question by direct observation: Creativity is obviously part of these processes, and they could not work without it. Even the construction of algorithms and formal systems itself is creative activity driven by the feeling of clarity and our shared human taste for elegance in logic.

From this point of view, mathematical results are relevant, but what is really being studied and evolved is the processes of combination and derivation.

Formal systems and previous results provide ways we can check whether we agree, but they do not solve problems for us. To the extent the problems are already solved mechanically, those are engineering tools, and no longer a subject matter for real mathematics.

3. This is the difference between mathematics and other forms of proof. It focusses upon assembling pure intuitions and models abstracted from situations into purely mechanical forms, unmixed with other data. It is not aimed at solving the problems at hand, but at providing methods for addressing problems in general that will automatically feel trustworthy to a wide range of human users.

Answer 4

I will only attempt to answer a small portion of your question. You ask, roughly: "are there certain strategies in mathematics that we use to prove things?" Well, to prove theorems, there are certainly some strategies that mathematicians use over and over. I have listed a couple below.

• Reductio ad Absurdum: To prove that a certain statment is true, we assume that the converse is true and try to reach a contradiction. If this occurs, then we can say that the original statement is true. This technique is often called proof by contradiction.

• Induction: When we want to prove a statement P(n) for each element n of the natural numbers, we often use induction. This is done by proving that the statement holds for a particular natural number n_0, and then showing that if the statement holds for n, then it must hold for n+1. The textbook example for this is showing that n^2 <= 2^n for n >= 5.

There are many other tools for discovering proofs, but they tend to be more specialized, depending on the branch of mathematics in which we are trying to find a proof. For example, in real analysis, we may try to show that a property P(x) holds for every x on the real number line. To do this, we may show instead that the set of values x such that P(x) holds, {x : P(x)}, is both open and closed. Then, from another theorem in topology, we can conclude that P(x) holds for every real number.

Your next question is: if there are all these techniques for creating proofs, then where does creativity come in? Well, creativity is used in fitting all the pieces together in a way that makes sense. Moreover, it is used when all the techniques are just not enough to complete a proof, which happens remarkably often. This is when new techniques are invented, and they may become very common or just limited to a few special cases.

Finally, is this sort of imagination different from using a computer to just try every possible road in a proof to see if we can find what we want? Well, one could perhaps say that we are just using the same techniques over and over, and that this could be programmed into a computer. However, this would likely take enormous amounts of computation time, longer than the lifespan of the universe. The difference is that when we create our rigorous proofs, we often have a dim outline of how we want to proceed, and the rigor comes afterwards. The creativity is in coming up with and idea of how we want to move forward in a proof: the intuition behind why something is true. This requires imagination and insight.