41
$\begingroup$

I haven't read very many proofs. The majority of the ones that I've read, I've read in my first-year proofs textbook. Nevertheless, its first chapter expatiates on the proper use of English in mathematical proofs, so I suspect that most proof authors do use both English (or another natural language) and formal proof systems for writing their proofs. However, I can't imagine many circumstances where mathematical notation and a formal proof system wouldn't suffice to convey the author's pertinent thoughts.

I suspect that proof authors have good reasons for making use of both English and formal expressions in their proofs, but I can't think of what those reasons are. Why do proof authors use English and formal expressions to write proofs? Are there stylistic rules (or guidelines) that state how, and in what parts of the proof, an author should, and shouldn't, use English?

$\endgroup$
9
  • 51
    $\begingroup$ Because any moderately complicated proof is a hellish beast in anything resembling a formal language. One writes to be understood, and that means one uses natural language [the mathematical dialect] with some semi-formal ingredients. $\endgroup$ Nov 18, 2014 at 15:26
  • 44
    $\begingroup$ In most cases, proofs are meant to be read by people. $\endgroup$
    – James
    Nov 18, 2014 at 15:27
  • 3
    $\begingroup$ See some of the formal proofs on MSE to get the gist of why it would be very impractical to do so. $\endgroup$
    – Git Gud
    Nov 18, 2014 at 15:33
  • $\begingroup$ There seems to be a presumption that natural language can't be part of a formal proof system. Mathematical language seems regimented enough that it might qualify as a formal system. For example, very specific meanings are given to some natural language constructions (like "almost everywhere" or "if ... then ..."). $\endgroup$
    – Seamus
    Nov 19, 2014 at 13:50
  • 2
    $\begingroup$ @DanielFischer As a countering argument, some proofs written mostly in natural languages (especially, in my experience, in Topology) are so poorly written, that they are impossible to follow (or worse) contain errors. $\endgroup$
    – imallett
    Nov 20, 2014 at 0:31

5 Answers 5

67
$\begingroup$

An ordinary mathematical proof1 is a piece of expository prose. Its purpose is to convince the reader that the theorem is true. Obviously it should be mathematically correct and logically sound, but it should also be clear and easy to follow. Writing in (paragraphs of) sentences, and using words for the connective tissue that gives a road map for the logic of the argument, generally makes the prose more readable. By all means use symbols when they’re appropriate: the quadratic formula is much easier to follow when expressed symbolically than when written out in words! But don’t fall into the trap of thinking that the more symbolism you use, the more professional your argument looks.

For an actual (and fairly simple) example you might look at this question and my answer to it.

1 The word proof is also used for a formal object in mathematical logic. Trying to follow a formal proof is rather like trying to figure out what a computer program does by looking at the machine language.

$\endgroup$
2
  • 16
    $\begingroup$ The machine-code vs source-code comparison is a brilliant one. There are volumes upon volumes about how to make your source-code more readable and easier to follow, and the entire point of programming languages is to make the creation of machine-code easier and more natural. $\endgroup$
    – corsiKa
    Nov 19, 2014 at 5:27
  • 5
    $\begingroup$ @corsiKa on the other hand if we want very high assurance of correctness we need to use machine-verifiable proofs in programming as well. For example the entire Windows Hyper-V hypervisor has been verified to be free of certain kinds of errors because it is such a security-critical component. $\endgroup$
    – usr
    Nov 19, 2014 at 9:47
45
$\begingroup$

The following is a purely formal proof of the irrationality of $\sqrt 2$, formalized using the HOL theorem prover Coq. It is equivalent to this human-language proof:

If there is an $n$ such that for some $p$, $n^2 = 2p^2$, then let's take the least positive such $n$ and the corresponding positive $p$, in this case we have (i) $(2p-n)^2=2(n-p)^2$ and (ii) $(2p-n) < n$, thus a contradiction.

Your question should now answer itself.


Require Import ZArith ZArithRing Omega Zwf.
Open Scope Z_scope.

Lemma Zabs_square : forall x, Zabs x ^ 2 = x ^ 2.
intros; case (Zabs_dec x); intros Heq; ring [Heq].
Qed.

Lemma Zabs_st_pos : forall x, x <> 0 -> 0 < Zabs x.
intros; assert (H':= Zabs_pos x); case (Zabs_dec x); intros; omega.
Qed.
Hint Resolve Zabs_pos Zabs_square Zabs_st_pos.

Theorem integer_statement :  ~exists n, exists p, n ^2 = 2* p^2 /\ n <> 0.
intros [n [p [He Hz]]]; pose (q := Zabs n); pose (r :=Zabs p).
assert (H : (0 < q /\ 0 <= r) /\ q ^2 = 2* r ^2).
  assert (F : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs p ^ 2 = p ^ 2 /\
            Zabs n ^ 2 = n ^ 2) by auto.
  destruct F as [H1 [H2 [H3 H4]]];  unfold q, r; split; auto; ring [H3 H4 He].
generalize r H; elim q using (well_founded_ind (Zwf_well_founded 0)); clear.
assert (fact_sq : forall x, x^2=x*x) by (intros; ring).
intros n IHn p [[Hn Hp] Heq].
assert (Hmain_eq: (2*p-n)^2 = 2*(n-p)^2) by ring [Heq].
assert (Hs: 0 < n^2) by (rewrite fact_sq; apply Zmult_lt_0_compat; auto).
assert (Hpn : p < n).
  apply Znot_ge_lt; intros Habs.
  assert (2*p^2 <= p^2).
    rewrite <- Heq; repeat rewrite fact_sq; 
    apply Zmult_le_compat; auto with zarith.
  omega.
assert (Hn2p: n < 2*p).
  elim (Zle_or_lt (2*p) n); auto; intros Habs'.
  assert (2*n^2 <= n^2).
    replace (2*n^2) with ((2*p)^2) by ring [Heq].
    repeat rewrite fact_sq; apply Zmult_le_compat; auto with zarith.
  omega.
assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; omega).
apply (IHn (2*p-n) Hzwf (n-p)); omega.
Qed.
$\endgroup$
13
  • 17
    $\begingroup$ The fact that this formal non-English proof is hard to read doesn't mean they all are... $\endgroup$
    – jtbandes
    Nov 18, 2014 at 19:05
  • 20
    $\begingroup$ You are lacking the (formal) proof that the code you provided is the least complicated formal proof for the given theorem. (Given enough time, I think can make an equivalent natural-language proof that is more complicated to understand than the formal proof you provided.) $\endgroup$
    – Alexander
    Nov 18, 2014 at 20:07
  • 10
    $\begingroup$ @Alexander: I don't doubt it, but the point is really the reverse: Can you make a formal proof that's as concise as the natural-language one? $\endgroup$
    – user139000
    Nov 18, 2014 at 22:29
  • 11
    $\begingroup$ @Alexander Anyone coming up with a formal language which also as precise and comprehensible (or even close to being so) as natural language will be doing well, to say the least. $\endgroup$
    – Keith
    Nov 19, 2014 at 1:55
  • 2
    $\begingroup$ @Keith There are some attempts, for example in this dissertation naproche.net/downloads/2013/doktor.pdf $\endgroup$
    – neo
    Nov 19, 2014 at 13:00
9
$\begingroup$

Why? Because this has been the most efficient way to communicate proofs, as shown by the answers of Brian M Scott and Pew.

But that may not always be so.

Mathematical theorems in journals now often reach tens or hundreds of pages, for example, the famous proof of Wiles's Theorem, or the Classification of All Finite Simple Groups (itself an ongoing project with key theorems still being coded into proof checkers). As knowledge expands, two things happen: either new fields (of subject matter, not the commutative ring with invertible multiplication) are explored, or the complexity of "technologies" increases. A proof often now reaches the complexity of a medium sized class library; something akin to tens of thousands of lines of high level computer code. In the early days of high level language programming, individual programmers cut and tested their own codes, which, once "proven" (by enough testing) were seldom disected again by other people, whom such codes were often incomprehensible to. Procedures and paradigms evolved to handle more and more software complexity: structured programming championed by such workers as Niklaus Wirth; later object oriented programming and various management theories for software quality control. A well documented piece of code is very like a natural language mathematical proof in many ways: its comments, design and structure should show the reader exactly how it does what it claims to do and the actual high level statements themselves provide the recipe to be encoded by the compiler.

The complexity that can be handled in these new paradigms is astounding: whereas the development of Fortran under the leadership of John Backus (of the Backhus-Naur metalanguage fame) took 18 staff years, computer science students now write their own compiler as late undergraduate or early undergraduate exercises and, with a bit of reading, the principles of compiler working are readily understood by almost anyone with training (see, for example, Appel, Andrew W. (1998),“Modern Compiler Implementation in C”, Cambridge University Press, New York, Cambridge. ISBN 0-521-58390-X. See esp. Chapter 2.).

Likewise Mathematics has evolved its own complexity handling paradigms. Two great examples of this are Noether's notion of Begriffliche Mathematik, which drove much of the modern approach abstract algebraic structures and category theory, although a logical, mathematical language in itself, also plays this role of giving a very large scale, top-down view of a mathematical problem: it bears a great deal of likeness to several software modelling metalanguages insofar that the latter are aimed at identifying and studying morphisms between objects within categories: in software design more often described as the something like the formal definition of "use-cases" or "processes" comprising "collaboration" between "actors" or "agents". The language of category theory is even heavily borrowed in software design and architecture.

But it may be that natural language in mathematics, or, equivalently, high-level languages and modelling languages in software design is reaching the limits of its capability. Fascinatingly, formal proof checkers are now finding their way into the proving of critical software systems. For example:

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish1, Thomas Sewell, Harvey Tuch, Simon Winwood, "seL4: Formal Veri cation of an OS Kernel" in In 22nd ACM Symposium on Operating Systems Principles (SOSP) (2009)

describes in detail the proof of the correctness of implementation (i.e. the equality of the software's behaviour with a formal specification) in the theorem prover Isabelle. One thing is for sure: formal theorem provers will become more and more important as softare systems, and mathematical proofs, rise above the complexity that can be handled by one human being. One of the comments also alludes to other like projects:

...on the other hand if we want very high assurance of correctness we need to use machine-verifiable proofs in programming as well. For example the entire Windows Hyper-V hypervisor has been verified to be free of certain kinds of errors because it is such a security-critical component. (User usr)

Just to close: using a software theorem prover to "prove" the soundness of software may seem like question begging, but it isn't really. The core of the theorem prover is simply a parser which tests the conformance of the proof steps with formal definitions of the rules of inference. If you read the Appel reference "Modern Compiler Implementation" I cited above, you can come to understand that a parser is actually a very simple program taking up at most a few pages of high level code and whose working has been thoroughly described in high level language and thoroughly understood by thousands of reviewers. Of course, something like Isabelle is much more than this, but it doesn't matter if there are bugs in the proof construction tools in Isabelle: as long as a constructed proof is sound (complies with the correct rules of inference), it will pass the proof checker. If a bug arose in the proof construction tools that led to an incorrect proof, it would be picked up in the last checking phase.

$\endgroup$
9
$\begingroup$

You wrote

I can't imagine many circumstances where mathematical notation and a formal proof system wouldn't suffice to convey the author's pertinent thoughts.

The case is, mathematical proofs contain lot of hand-waving argument such as referring to symmetry or to consistent change of variables. Editors are eager to accept these arguments but theorem provers are not. The formalisation of such arguments is an active area of research. One example is nominal sets which develops a full algebraic theory of the mentioned change of variables. It has an implementation in the Isabelle theorem prover called Nominal Isabelle and it requires some work to use.

There is a vast literature on what a proof is, a good place to start is the paper Social Processes and Proofs of Theorems and Programs.

$\endgroup$
3
  • $\begingroup$ Also, the quoted sentence is called logicism, see here: en.wikipedia.org/wiki/Logicism $\endgroup$
    – Gergely
    Nov 20, 2014 at 7:06
  • $\begingroup$ The Logicism or the Social Processes article? $\endgroup$
    – Gergely
    Nov 20, 2014 at 14:58
  • 2
    $\begingroup$ The social processes one. $\endgroup$ Nov 20, 2014 at 15:08
0
$\begingroup$

I write software, and I would like to draw an analogy using programming languages.

Math proofs can be traced at the bottom level to formal systems. The systems can be compared to the bottom level of computer hardware composed of CPUs, memory, buses, and possibly GPUs for heterogeneous systems. Rules of deduction in the formal system are analogous to electrical behaviors of devices. Theoretically, an excellent engineer knowing everything about computer hardware should be able to use sequences of 0 (low voltage) and 1 (high voltages) to control computers for specific purposes. But in reality, engineers typically don't do that. It is ridiculous for software engineers at Google, Amazon, Facebook and Microsoft to write programs using hardware languages, even if they can, as there exist programming languages much more efficient, like C/C++, JAVA, etc. These high-level languages are designed so that when applied, they generate common results on different hardware. Engineers do not have to know exactly what happens in hardware, but they only need to trust that each sentence written in a high-level language corresponds to a specific behavior in hardware, which will finally generate the CORRECT result ensured by the documentation of the high-level language. Experts in programming languages design languages so that they are of behaviors described in the documentation. These experts have to understand hardware thoroughly to design correct hardware behaviors of languages.

Similarly, different formal systems are like different hardware. Daily languages such as English and Chinese are like high-level programming languages. Proofs from experienced mathematicians, whatever language they are written in, have to correspond to formal languages in some way. We are confident that the correspondence exists, but we do not specify what it is. Logicians have to design and verify such correspondence. But all mathematicians are not logicians. They are "engineers" who construct proofs.

The question "why don't we construct proofs in formal languages" is analogous to the question "why don't we write computer programs in machine language". The answer is, it is inefficient. But engineers who knows machine languages may be more efficient in debugging, just as mathematicians who have formal systems in mind are less likely to make wrong deductions for complicated propositions.

$\endgroup$
6
  • $\begingroup$ "But engineers who knows machine languages definitely are better programmers, just as mathematicians who are logicians or linguists at the same time are probably better mathematicians." - I don't know about engineers, but a mathematician that is a logician or a linguist is not probably a better mathematician. Most (top) mathematicians in the world are neither logicians nor linguists. $\endgroup$ Dec 26, 2020 at 4:55
  • $\begingroup$ @RandyMarsh May be of a better potential to be a better mathematician? $\endgroup$
    – Ziqi Fan
    Dec 26, 2020 at 4:58
  • $\begingroup$ Also no. If that were the case, every PhD course in mathematics would heavily emphasize logic or linguistics. $\endgroup$ Dec 26, 2020 at 4:59
  • $\begingroup$ Your edited statement "mathematicians who have formal systems in mind are less likely to make wrong deductions for complicated propositions" is still false. Mathematicians don't generally have formal systems in mind when they are deducing theorems, except those working on or in the vicinity of formal systems. If there was a piece of knowledge that would guarantee any mathematician less mistakes, all mathematicians would be trained in it. $\endgroup$ Dec 26, 2020 at 5:10
  • $\begingroup$ @RandyMarsh Well. I respect your opinion, but I have to reserve my opinion on the role of logical training. I am an engineer, and I have to learn a lot about digital circuits in undergraduate. We had to experiment a lot to get familiar with hardware behavior. In my opinion, students in math should learn something about first order logic. Actually, I believe set theory has to be taught to math students, and I see that as a rigorous training in logic. I am not a mathematician, but from independent thinking, I cannot think of a reason why rigorous logical education do not help mathematicians. $\endgroup$
    – Ziqi Fan
    Dec 26, 2020 at 5:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.