Mathematics and proof

One of the great myths of mathematicians is that mathematical knowledge, once proven, is solid, and not subject to later contestation.   Thus, Oxford mathematician Marcus du Sautoy, writing in the New Scientist (2006-08-26), says:

Proof is supposed to be what sets mathematics apart from the other sciences. Traditionally, the subject has not been an evolutionary one in which the fittest theory survives. New insights don’t suddenly overturn the theorems of the previous generation. The subject is like a huge pyramid, with each generation building on the secure foundations of the past. The nature of proof means that mathematicians, to use Newton’s words, really do stand on the shoulders of giants.
In the past, those shoulders have been extremely steady. After all, in no other science are the discoveries of the Ancient Greeks still as valid today as they were at the time. Euclid’s 2300-year-old proof that there are infinitely many primes is perhaps the first great example of a watertight proof.

The reason for this widespread view is that mathematics uses deduction to reach its conclusions.  At least, that is true of pure mathematics, or was so until computers began to be used in proofs (a topic which du Sautoy discusses in that article).  But all deduction does is to show that, given some assumptions and given some rules of inference, a certain conclusion follows from those assumptions by applying those rules of inference.  If either the assumptions are false or the rules of inference not acceptable, then the stated conclusions will not, in fact, follow.
Du Sautoy is quite wrong to claim that new insights do not overturn the theorems of the previous generation.  The history of pure mathematics is replete with examples where proven conclusions were later revealed to depend on assumptions not made explicit, or on assumptions previously thought to be obvious but which were later shown to be false, or on rules of inference later considered invalid.   For over a century, mathematicians thought that everywhere-continuous functions were also everywhere-differentiable, until shown a counter-example.  For a similar period, they thought that the convergent limit of an infinite sequence of continuous functions was itself also continuous, until shown a counter-example.  They thought that there could not exist a one-to-one and onto mapping between the real unit interval and the real unit square, until shown such a mapping (a so-called space-filling curve).  In fact, there are infinitely-many such mappings; indeed, an uncountable infinity of them.  In all these case, “proofs” of the erroneous conclusions existed, which is why the earlier mathematicians believed those conclusions.  The proofs were later shown to be flawed, because they depended on (usually-implicit) assumptions which were false.   For the differential calculus, the fixing effort was begun by Cauchy and Weierstrauss, using epsilon-delta arguments which were more rigorous than the proofs of the earlier generation of analysts.
Not only does Du Sautoy have his history wrong, but there is shurely shome mishtake in his mentioning Euclid here.  The 19th century was consumed by a controversy over the truth-status of Euclidean geometry, and the discovery of apparently-logical alternatives to it.   As clever a man as the logician and philosopher Gottlob Frege (an intellectual hero of Wittgenstein) could not get his head around the idea that these different versions of geometry could all simultaneously be true.   Yet that is the conclusion mathematicians came to: that, depending on the assumptions you made about the surface on which you doing geometry, there were in fact valid alternatives to the discoveries of the Greeks:  draw your triangles on the surface of a sphere, instead of on a flat plane, for example, and you could readily draw triangles whose three angles did not sum to 180 degrees.  You choose your assumptions, you gets your geometry!  This is not a secure pyramid of knowledge, but many pyramids, post-modernist style.
And in the first part of the 20th century, pure mathematics was consumed with a bitter argument over whether a particular rule of inference – reductio ad absurdem (RAA), or reasoning from an assumption thought to be false – was valid in deductive proofs of the existence of mathematical objects.   The dissidents created their own school of pure mathematics, constructivism, which is still being studied.  Indeed, it turns out that a closely-related logic, intuitionistic logic, appears naturally elsewhere in mathematics (as part of the internal structure of a topos). Once again, you choose your rules of inference, you gets your mathematical theorems.
There is no single, massive pyramid of knowledge here, as du Sautoy claims, but lots of smaller pyramids.  Every so often, a great mathematician is able to devise a new conceptual framework which allows some or all of these baby pyramids to appear to be part of some larger pyramid, as Pieri and Hilbert did with geometry in the 1890s, or as Lawvere and others did with category theory as a foundation for mathematics in the 1960s.   But, based on past experience, new baby pyramids will continue to be created by mathematicians arguing about the assumptions or rules of inference used in earlier proofs.    To consider this process of contestation, splitting, and attempted re-unification to be somehow different to what happens in other domains of human knowledge may be comforting to mathematicians, but is myth nonetheless.

Theatre Lakatos

Last night, I caught a new Australian play derived from the life of logician Kurt Godel, called Incompleteness.  The play is by playwright Steven Schiller and actor Steven Phillips, and was peformed at Melbourne’s famous experimental theatrespace, La Mama, in Carlton. Both script and performance were superb:  Congratulations to both playwright and actor, and to all involved in the production.
Godel was famous for having kept every piece of paper he’d ever encountered, and the set design (pictured here) included many file storage boxes.  Some of these were arranged in a checkerboard pattern on the floor, with gaps between them.  As the Godel character (Phillips) tried to prove something, he took successive steps along diagonal and zigzag paths through this pattern, sometimes retracing his steps when potential chains of reasoning did not succeed.   This was the best artistic representation I have seen of the process of attempting to do mathematical proof:  Imre Lakatos’ philosophy of mathematics made theatrical flesh.
 

There is a photograph of the La Mama billboard at Paola’s site.

The Mathematical Tripos at Cambridge

From the 18th century until 1909, students at Cambridge University took a compulsory series of examinations, called the Mathematical Tripos, named after the three-legged stool that candidates originally sat on.  Until the mid-18th century, these examinations were conducted orally, and only became written examinations over faculty protests.   Apparently, not everyone believed that written examinations were the best or fairest way to test mathematical abilities, a view which would amaze many contemporary people – although oral examinations in mathematics are still commonly used in some countries with very strong mathematical traditions, such as Russia and the other states of the former USSR.
The Tripos became a notable annual public event in the 19th century, with The Times newspaper publishing articles and biographies before each examination on the leading candidates, and then, after each examination, the results.   There was considerable public interest in the event each year, not just in Cambridge or among mathematicians, and widespread betting on the outcomes.
Continue reading ‘The Mathematical Tripos at Cambridge’

Australian logic: a salute to Malcolm Rennie

Recently, I posted a salute to Mervyn Pragnell, a logician who was present in the early days of computer science.  I was reminded of the late Malcolm Rennie, the person who introduced me to formal logic, and whom I acknowledged here.   Rennie was the most enthusiastic and inspiring lecturer I ever had, despite using no multi-media wizardry, usually not even an overhead projector.  Indeed, he mostly just sat and spoke, moving his body as little as possible and writing only sparingly on the blackboard, because he was in constant pain from chronic arthritis.   He was responsible for part of an Introduction to Formal Logic course I took in my first year (the other part was taken by Paul Thom, for whom I wrote an essay on the notion of entailment in a system of Peter Geach).   The students in this course were a mix of first-year honours pure mathematicians and later-year philosophers (the vast majority), and most of the philosophers struggled with non-linguistic representations (ie, mathematical symbols).  Despite the diversity, Rennie managed to teach to all of us, providing challenging questions and discussions with and for both groups.   He was also a regular entrant in the competitions which used to run in the weekly Nation Review (and a fellow-admirer of the My Sunday cartoons of Victoria Roberts), and I recall one occasion when a student mentioned seeing his name as a competition winner, and the class was then diverted into an enjoyable discussion of tactics for these competitions.
Continue reading ‘Australian logic: a salute to Malcolm Rennie’

Great mathematical ideas

Normblog has a regular feature, Writer’s Choice, where writers give their opinions of books which have influenced them.   Seeing this led me recently to think of the mathematical ideas which have influenced my own thinking.   In an earlier post, I wrote about the writers whose  books (and teachers whose lectures) directly influenced me.  I left many pure mathematicians and statisticians off that list because most mathematics and statistics I did not receive directly from their books, but indirectly, mediated through the textbooks and lectures of others.  It is time to make amends.
Here then is a list of mathematical ideas which have had great influence on my thinking, along with their progenitors.  Not all of these ideas have yet proved useful in any practical sense, either to me or to the world – but there is still lots of time.   Some of these theories are very beautiful, and it is their elegance and beauty and profundity to which I respond.  Others are counter-intuitive and thus thought-provoking, and I recall them for this reason.

  • Euclid’s axiomatic treatment of (Euclidean) geometry
  • The various laws of large numbers, first proven by Jacob Bernoulli (which give a rational justification for reasoning from samples to populations)
  • The differential calculus of Isaac Newton and Gottfried Leibniz (the first formal treatment of change)
  • The Identity of Leonhard Euler:  exp ( i * \pi) + 1 = 0, which mysteriously links two transcendental numbers (\pi and e), an imaginary number i (the square root of minus one) with the identity of the addition operation (zero) and the identity of the multiplication operation (1).
  • The epsilon-delta arguments for the calculus of Augustin Louis Cauchy and Karl Weierstrauss
  • The non-Euclidean geometries of Janos Bolyai, Nikolai Lobachevsky and Bernhard Riemann (which showed that 2-dimensional (or plane) geometry would be different if the surface it was done on was curved rather than flat – the arrival of post-modernism in mathematics)
  • The diagonalization proofof Gregor Cantor that the Real numbers are not countable (showing that there is more than one type of infinity) (a proof-method later adopted by Godel, mentioned below)
  • The axioms for the natural numbers of Guiseppe Peano
  • The space-filling curves of Guiseppe Peano and others (mapping the unit interval continuously to the unit square)
  • The axiomatic treatments of geometry of Mario Pieri and David Hilbert (releasing pure mathematics from any necessary connection to the real-world)
  • The algebraic topology of Henri Poincare and many others (associating algebraic structures to topological spaces)
  • The paradox of set theory of Bertrand Russell (asking whether the set of all sets contains itself)
  • The Fixed Point Theorem of Jan Brouwer (which, inter alia, has been used to prove that certain purely-artificial mathematical constructs called economies under some conditions contain equilibria)
  • The theory of measure and integration of Henri Lebesgue
  • The constructivism of Jan Brouwer (which taught us to think differently about mathematical knowledge)
  • The statistical decision theory of Jerzy Neyman and Egon Pearson (which enabled us to bound the potential errors of statistical inference)
  • The axioms for probability theory of Andrey Kolmogorov (which formalized one common method for representing uncertainty)
  • The BHK axioms for intuitionistic logic, associated to the names of Jan Brouwer, Arend Heyting and Andrey Kolmogorov (which enabled the formal treatment of intuitionism)
  • The incompleteness theorems of Kurt Godel (which identified some limits to mathematical knowledge)
  • The theory of categories of Sam Eilenberg and Saunders Mac Lane (using pure mathematics to model what pure mathematicians do, and enabling concise, abstract and elegant presentations of mathematical knowledge)
  • Possible-worlds semantics for modal logics (due to many people, but often named for Saul Kripke)
  • The topos theory of Alexander Grothendieck (generalizing the category of sets)
  • The proof by Paul Cohen of the logical independence of the Axiom of Choice from the Zermelo-Fraenkel axioms of Set Theory (which establishes Choice as one truly weird axiom!)
  • The non-standard analysis of Abraham Robinson and the synthetic geometry of Anders Kock (which formalize infinitesimal arithmetic)
  • The non-probabilistic representations of uncertainty of Arthur Dempster, Glenn Shafer and others (which provide formal representations of uncertainty without the weaknesses of probability theory)
  • The information geometry of Shunichi Amari, Ole Barndorff-Nielsen, Nikolai Chentsov, Bradley Efron, and others (showing that the methods of statistical inference are not just ad hoc procedures)
  • The robust statistical methods of Peter Huber and others
  • The proof by Andrew Wiles of The Theorem Formerly Known as Fermat’s Last (which proof I don’t yet follow).

Some of these ideas are among the most sublime and beautiful thoughts of humankind.  Not having an education which has equipped one to appreciate these ideas would be like being tone-deaf.

Myopic utilitarianism

What are the odds, eh?  On the same day that the Guardian publishes an obituary of theoretical computer scientist, Peter Landin (1930-2009), pioneer of the use of Alonzo Church’s lambda calculus as a formal semantics for computer programs, they also report that the Government is planning only to fund research which has relevance  to the real-world.  This is GREAT NEWS for philosophers and pure mathematicians! 
What might have seemed, for example,  mere pointless musings on the correct way to undertake reasoning – by Aristotle, by Islamic and Roman Catholic medieval theologians, by numerous English, Irish and American abstract mathematicians in the 19th century, by an entire generation of Polish logicians before World War II, and by those real-world men-of-action Gottlob Frege, Bertrand Russell, Ludwig Wittgenstein and Alonzo Church – turned out to be EXTREMELY USEFUL for the design and engineering of electronic computers.   Despite Russell’s Zen-influenced personal motto – “Just do!  Don’t think!” (later adopted by IBM) – his work turned out to be useful after all.   I can see the British research funding agencies right now, using their sophisticated and proven prognostication procedures to calculate the society-wide economic and social benefits we should expect to see from our current research efforts over the next 2300 years  – ie, the length of time that Aristotle’s research on logic took to be implemented in technology.   Thank goodness our politicians have shown no myopic utilitarianism this last couple of centuries, eh what?!
All while this man apparently received no direct state or commercial research funding for his efforts as a computer pioneer, playing with “pointless” abstractions like the lambda calculus.
And Normblog also comments.
POSTSCRIPT (2014-02-16):   And along comes The Cloud and ruins everything!   Because the lower layers of the Cloud – the physical infrastructure, operating system, even low-level application software – are fungible and dynamically so, then the Cloud is effectively “dark” to its users, beneath some level.   Specifying and designing applications that will run over it, or systems that will access it, thus requires specification and design to be undertaken at high levels of abstraction.   If all you can say about your new system is that in 10 years time it will grab some data from the NYSE, and nothing (yet) about the format of that data, then you need to speak in abstract generalities, not in specifics.   It turns out the lambda calculus is just right for this task and so London’s big banks have been recruiting logicians and formal methods people to spec & design their next-gen systems.  You can blame those action men, Church and Russell.

Creative writing

The English poet T. E. Hulme (1883-1917) talking about creative writing compared it to geometrical drawing.   Hulme had studied mathematics and philosophy at Cambridge, although without graduating.

The great aim is accurate, precise and definite description. The first thing is to recognize how extraordinarily difficult this is. It is no mere matter of carefulness; you have to use language, and language is by its very nature a communal thing; that is, it expresses never the exact thing but a compromise – that which is common to you, me and everybody. But each man sees a little differently, and to get out clearly and exactly what he does see, he must have a terrific struggle with language, whether it be with words or the technique of other arts. Language has its own special nature, its own conventions and communal ideas. It is only by a concentrated effort of the mind that you can hold it fixed to your own purpose. I always think that the fundamental process at the back of all the arts might be represented by the following metaphor. You know what I call architect’s curves – flat pieces of wood with all different kinds of curvature. By a suitable selection from these you can draw approximately any curve you like. The artist I take to be the man who simply can’t bear the idea of that “approximately”. He will get the exact curve of what he sees whether it be an object or an idea in the mind. Suppose that instead of your curved pieces of wood you have a springy piece of steel of the same types of curvature as the wood. Now the state of tension or concentration of mind, if he is doing anything really good in this struggle against the ingrained habit of technique, may be represented by a man employing all his fingers to bend the steel out of its own curve and into the exact curve which you want. Something different to what it would assume naturally.”

Reference:
T. E. Hulme, in the essay, “Romanticism and Classicism”, quoted in:   A. Alvarez [2003]: Making it new. The New York Review of Books, 15 May 2003,  Volume L, No. 8, pp. 28-30.

Nicolas Fatio de Duillier

Fatio de DuillierNicolas Fatio de Duillier (1664-1753) was a Genevan mathematician and polymath, who for a time in the 1680s and 1690s, was a close friend of Isaac Newton. After coming to London in 1687, he became a Fellow of the Royal Society (on 1688-05-15), as later did his brother Jean-Christophe (on 1706-04-03).  He played a major part in Newton’s feud with Leibniz over who had invented the differential calculus, and was a protagonist all his life for Newton’s thought and ideas.
Continue reading ‘Nicolas Fatio de Duillier’

Guerrilla logic: a salute to Mervyn Pragnell

When a detailed history of computer science in Britain comes to be written, one name that should not be forgotten is Mervyn O. Pragnell.  As far as I am aware, Mervyn Pragnell never held any academic post and he published no research papers.   However, he introduced several of the key players in British computer science to one another, and as importantly, to the lambda calculus of Alonzo Church (Hodges 2001).  At a time (the 1950s and 1960s) when logic was not held in much favour in either philosophy or pure mathematics, and before it became to be regarded highly in computer science, he studied the discipline not as a salaried academic in a university, but in a private reading-circle of his own creation, almost as a guerrilla activity.

Pragnell recruited people for his logic reading-circle by haunting London bookshops, approaching people he saw buying logic texts (Bornat 2009).  Among those he recruited to the circle were later-famous computer pioneers such as Rod Burstall, Peter Landin (1930-2009) and Christopher Strachey (1916-1975).  The meetings were held after hours, usually in Birkbeck College, University of London, without the knowledge or permission of the college authorities (Burstall 2000).  Some were held or continued in the neighbouring pub, The Duke of Marlborough.  It seems that Pragnell was employed for a time in the 1960s as a private research assistant for Strachey, working from Strachey’s house (Burstall 2000).   By the 1980s, he was apparently a regular attendee at the seminars on logic programming held at the Department of Computing in Imperial College, London, then (and still) one of the great research centres for the application of formal logic in computer science.

Pragnell’s key role in early theoretical computer science is sadly under-recognized.   Donald MacKenzie’s fascinating history and sociology of automated theorem proving, for example, mentions Pragnell in the text (MacKenzie 2001, p. 273), but manages to omit his name from the index.  Other than this, the only references I can find to his contributions are in the obituaries and personal recollections of other people.  I welcome any other information anyone can provide.

UPDATE (2009-09-23): Today’s issue of The Guardian newspaper has an obituary for theoretical computer scientist Peter Landin (1930-2009), which mentions Mervyn Pragnell.

UPDATE (2012-01-30):  MOP appears also to have been part of a production of the play The Way Out at The Little Theatre, Bristol in 1945-46, according to this web-chive of theatrical info.

UPDATE (2013-02-11):  In this 2001 lecture by Peter Landin at the Science Museum, Landin mentions first meeting Mervyn Pragnell in a cafe in Sheffield, and then talks about his participation in Pragnell’s London reading group (from about minute 21:50).

UPDATE (2019-07-05): I have learnt some further information from a cousin of Mervyn Pragnell, Ms Susan Miles.  From her, I understand that MOP’s mother died in the Influenza Pandemic around 1918, when he was very young, and he was subsequently raised in Cardiff in the large family of a cousin of his mother’s, the Miles family.  MOP’s father’s family had a specialist paint manufacturing business in Bristol, Oliver Pragnell & Company Limited, which operated from 25-27 Broadmead.  This establishment suffered serious bomb damage during WW II.   MOP was married to Margaret and although they themselves had no children, they kept in close contact with their relatives.  Both are remembered fondly by their family.   (I am most grateful to Susan Miles, daughter of Mervyn Miles whose parents raised MOP, for sharing this information.)

References:

Richard Bornat [2009]:  Peter Landin:  a computer scientist who inspired a generation, 5th June 1930 – 3rd June 2009.  Formal Aspects of Computing, 21 (5):  393-395.

Rod Burstall [2000]:  Christopher Strachey – understanding programming languages.  Higher-Order and Symbolic Computation, 13:  51-55.

Wilfrid Hodges [2001]:  A history of British logic.  Unpublished slide presentation.  Available from his website.

Peter Landin [2002]:  Rod Burstall:  a personal note. Formal Aspects of Computing, 13:  195.

Donald MacKenzie [2001]:  Mechanizing Proof:  Computing, Risk, and Trust.  Cambridge, MA, USA:  MIT Press.

Computer science, love-child: Part 2

This post is a continuation of the story which began here.
Life for the teenager Computer Science was not entirely lonely, since he had several half-brothers, half-nephews, and lots of cousins, although he was the only one still living at home.   In fact, his family would have required a William Faulkner or a Patrick White to do it justice.
The oldest of Mathematics’ children was Geometry, who CS did not know well because he did not visit very often.  When he did visit, G would always bring a sketchpad and make drawings, while the others talked around him.   What the boy had heard was that G had been very successful early in his life, with a high-powered job to do with astronomy at someplace like NASA and with lots of people working for him, and with business trips to Egypt and Greece and China and places.  But then he’d had an illness or a nervous breakdown, and thought he was traveling through the fourth dimension.  CS had once overheard Maths telling someone that G had an “identity crisis“, and could not see the point of life anymore, and he  had become an alcoholic.  He didn’t speak much to the rest of the family, except for Algebra, although all of them still seemed very fond of him, perhaps because he was the oldest brother.
Continue reading ‘Computer science, love-child: Part 2’