33
$\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$
  • 49
    $\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$ – Daniel Fischer Nov 18 '14 at 15:26
  • 39
    $\begingroup$ In most cases, proofs are meant to be read by people. $\endgroup$ – James Nov 18 '14 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 '14 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 '14 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 '14 at 0:31
60
$\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$
  • 14
    $\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 '14 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 '14 at 9:47
41
$\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$
  • 15
    $\begingroup$ The fact that this formal non-English proof is hard to read doesn't mean they all are... $\endgroup$ – jtbandes Nov 18 '14 at 19:05
  • 19
    $\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 '14 at 20:07
  • 9
    $\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 '14 at 22:29
  • 10
    $\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 '14 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 '14 at 13:00
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$
  • $\begingroup$ Also, the quoted sentence is called logicism, see here: en.wikipedia.org/wiki/Logicism $\endgroup$ – Gergely Nov 20 '14 at 7:06
  • $\begingroup$ Thanks for linking the article, I found it a really enjoyable read. $\endgroup$ – user2520938 Nov 20 '14 at 7:38
  • $\begingroup$ The Logicism or the Social Processes article? $\endgroup$ – Gergely Nov 20 '14 at 14:58
  • 2
    $\begingroup$ The social processes one. $\endgroup$ – user2520938 Nov 20 '14 at 15:08
8
$\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$

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.