Previous Up Next Citations From References: 0 From Reviews: 0 MR3060023 (Review) 00A35 03A05 03E20 Boute, Raymond T. (B-GHNT-NDM) How to calculate proofs: bridging the cultural divide. Notices Amer. Math. Soc. 60 (2013), no. 2, 173–191. The paper under review covers a broad range of topics. It raises several important issues concerning the nature of proof. In addition, it treats both the evolution of our understanding of proof and how proof has been taught. The reviewer-a mathematically trained logician who has been publishing in history of logic, philosophy of logic, philosophy of mathematics, and mathematical logic for over fifty years-found this paper very difficult and challenging to read: the author often seemed unaware of how difficult the material is and what needs to be said to convey it to a reader. It is incomprehensible how the paper could be intended for "mathematics educators" or students. Nevertheless, the reviewer found the paper fascinating, rewarding, and hard to put down. It provides a lot of food for thought. To give the reader the flavor of the paper, this review begins with two quotations: one composed of three sentences from the paper's first page and one composed of three sentences from its conclusion, which begins on page 188. From the first page: "This article argues that one of the most neglected opportunities in many branches of mathematics is symbolic reasoning for the 'logical' parts rather than just for the algebraic, analytic, etc., parts, where symbolic calculation has been a well-established routine since Viète and Descartes. [. . . ] The treatment is introductory, addressing anyone interested in augmenting their palette of reasoning strategies, including mathematics educators and, directly or indirectly, students. [. . . ] Equations form such a powerful tool in problem solving because they delegate substantial parts of reasoning (especially the tricky ones) to symbolic calculation." There is no abstract and there is no reference on the first page to the meaning of the title. From the conclusion: "As for many issues, education is a crucial element in bridging a methodological gap. Ample evidence has been given that learning to practice faithful formalization and true symbolism (not syncopation) should be an integral part of mathematics education. Most effective for dealing with logical arguments is the ability to calculate with predicates and quantifiers as fluently as is customary for derivatives and integrals." The paper never does explain its title. In particular, the reader is never told what the paper takes a proof to be. Readers who think that a proof of a proposition establishes the proposition's truth-or, more subjectively, that a proof of a proposition persuades or convinces people of the proposition's truth-will be surprised by some of the paper's statements. For example, on page 185 the author says that the idea of persuading or convincing someone else by a proof is illusory. Moreover, the paper never explains what it means to "calculate proofs". Normally, calculation contrasts with proof. A calculation is a mechanical process having input and output, the conclusion of which is not known in advance. A proof is a creative process whose conclusion is given at the outset. Calculations produce objects; proofs produce knowledge. The paper's juxtapositions 'calculational proof', 'calculational argument', and the like seem almost contradictory. This rambling, hefty 18-page paper has 51 references. Its prose is vague, elliptical, and at times harshly judgmental. The body of the paper contains several remarks lamenting what the author regards as the deplorable state of the arts of teaching and notating proofs in mathematics and computer science. The paper scolds well-known writers for what the author regards as errors. The scolding is not always accurate. An example from page 188 follows. "A pervasive form of sloppiness concerns some of the most useful forms of expression in mathematics: variables and functions. In particular, the distinction between free and bound variables and the rules governing them seem to be insufficiently appreciated. For instance, in [51] the definition 'Truth set of P (x) = {x:P (x)}' has x occurring free on the left and bound on the right of the equality sign. The incorrect appearance of (x) in 'the truth set of P (x)' is analogous to talking about 'the function f(x)' when actually meaning 'the function f ', which invoked the justified wrath of calculus professors fifty years ago!" The reference [51] refers to a well-received, popular, and respected text: [D. J. Velleman, How to prove it, second edition, Cambridge Univ. Press, Cambridge, 2006; MR2200345]. The "definition" is on page 30. Of course, by "variables and functions" the paper must mean "forms of expression about variables and functions": variables and functions are not forms of expression. Moreover, by "the distinction between free and bound variables" the paper must mean "the distinction between free and bound occurrences of variables": there is no such thing as a free variable or a bound variable. Some readers would say that the paper's expression "has x occurring free" should be "has 'x' occurring free" but other readers accept autonymous usage-using a string to mention itself. Further, the paper's word "wrath" must be an exaggeration; perhaps "disapproval" would be warranted. It is also worth noting, contrary to the paper, that, although 'x' occurs free in expressions that 'P (x)' stands for, it does not occur free in the 'Truth set of P (x)', the left side of the equation. This is a mistake in the paper's criticism of Velleman's "sloppiness". The letter 'x' does not even occur free in the four-character expression 'P (x)'. In 'Truth set of P (x)' the letter 'x' is part of a four-character string 'P (x)' that refers to a formula-a formula that may have arbitrarily many characters and in which 'x' has at least one free occurrence, possibly very many. Velleman, an accomplished mathematician, is a former editor-in-chief of The American Mathematical Monthly. When he is criticized, people pay careful attention. Charges against him are likely to be examined carefully. To some readers, this mistaken charge might discredit the paper's author and perhaps also the journal's editors and referees. It is the paper's author who "insufficiently appreciated" the rules governing variables. Notice also that the letter 'x' does not occur bound in 'Truth set of P (x)'. When 'P (x)' is used to mention a statement, the occurrence of the letter 'x' is being used orthographically like the 'x' in 'Texas', not as a variable, and, thus, its occurrence is neither free nor bound. In the previous sentence, 'x' occurs four times but not as a variable; hence in it the occurrences of the letter 'x' are neither free nor bound. The occurrence of the letter 'x' in 'Texas' is neither free nor bound. Moreover, the Velleman expression 'Truth set of P (x) = {x:P (x)}'-called a definition in this paper-is not called a definition by Velleman. His definition of truth set is the following: "The truth set of a statement P (x) is the set of all values of x that make P (x) true". Here none of the three occurrences of 'x' is as a variable. Its second occurrence is autonymous; the other two are orthographic. If one wished to restate the definition fully using the bracket-variable-colon-formula-bracket notation, one would write something like the following where 'P (x)' is a metavariable whose three occurrences are all bound: For every statement P (x), the truth set of P (x) is {y: y is a value of 'x' that makes P (x) true}. In the restatement, 'x' is still not used as a variable; 'y' is used as a variable that occurs twice bound. In 'values of x', the letter 'x' is not a variable but an autonymous name of a variable. That point is clarified in the restatement. The ideas used above concerning occurrences of one and the same letter as a variable- where substitutions are possible-and as an orthographic element-where substitutions are not possible-are well known from Alfred Tarski's classic truth-definition paper. See §1, especially pages 159ff, of the English translation found in the 1956 collection of articles by Tarski [Logic, semantics, metamathematics. Papers from 1923 to 1938, translated by J. H. Woodger, Oxford at the Clarendon Press, 1956; MR0078296 (17,1171a); second edition, Hackett, Indianapolis, IN, 1983; MR0736686 (85e:01065)]-referred to below as LSM. In Velleman's definition, the four-character string 'P (x)' is a metalanguage variable ranging over statements having 'x' occurring free one or more times and no other variable occurring free. The universal quantifier 'For every statement P (x)' is tacitly omitted, as is usual in definitions expressed in idiomatic mathematical prose. Velleman is defining a function from a certain set of statements, viz. the range of 'P (x)', into the powerset of the universe of discourse. The occurrence of the letter 'x' in the variable 'P (x)' is neither free nor bound. In Velleman's definition, the substituends of the metalanguage variable 'P (x)' are not statements-to use Velleman's terminology-having 'x' occurring free but names of such statements. Such names have no variable occurring free. For example, 'x' occurs free in the statement '(x < 2)' but not in its name ' '(x < 2)' '. The five-character formula '(x < 2)' has a truth set, but its seven-character name ' '(x < 2)' ' does not. For iterated-quote names, see pages 159–161 in LSM. Velleman's expression "Truth set of P (x) = {x:P (x)}", which the paper mistakenly took to be his definition, is part of an informal explanation: the omission of the definite article signals rough informality. As it stands, it cannot easily be understood as an elliptical expression of a definition. Consider one possibility. For every statement P (x), the truth set of P (x) = {x:P (x)}. Taking 'P (x)' as above, substituting a name of the above statement yields the following: The truth set of '(x < 2)' = {x: '(x < 2)'}. However, this is incoherent in view of the quotation marks that render the enclosed occurrence of 'x' a non-variable and thus unfree. Compare LSM, page 160. Alternatively, Velleman's expression "Truth set of P (x) = {x:P (x)}" might have been intended as a schema having an unusual side-condition: its instances are obtained by replacing the placeholder 'P (x)' on the right by a statement having 'x' free and replacing 'P (x)' on the left by a name of that statement [see J. Corcoran, Bull. Symbolic Logic 12 (2006), no. 2, 219–240; MR2223922 (2007j:03003)]. This is a non-homogeneous schema: different occurrences of the same placeholder are replaced differently. The reviewer does not know of others who have used such nonhomogeneous schemata. A name of a formula having 'x' free does not have 'x' free, even if the formula is being used autonymously. Velleman could have-and some would say should have-made a homogeneous schema such as the following where 'P (x)' is a placeholder whose two occurrences are neither free nor bound: The truth set of a statement P (x) is {y: y is a value of 'x' that makes P (x) true}. Here, to make an instance one would replace both occurrences of 'P (x)' by one and the same name of a formula having 'x' free, a name not having 'x' free. Replacing 'P (x)' by a name of '(x < 2)', the instance is the following: The truth set of a statement '(x < 2)' is {y: y is a value of 'x' that makes '(x < 2)' true}. Anyway, the paper identified a problematic passage in [51], but it failed to analyze the passage, it failed to identify any of the problems and, in fact, it made two inaccurate claims about the passage. Also, on page 175, the paper cites Leibniz as the first mathematician to conceive of formalized symbolic reasoning as an ideal and it credits Boole with making the first progress in realizing the Leibnizian ideal: "Progress in this direction started with Boole, and the developments in formal logic over the subsequent one hundred fifty years are well documented". No evidence is given for either claim. J. Corcoran References 1. Vladimir I. Arnold, On Teaching Mathematics, 1997. http://pauli.uni-muenster. de/∼munsteg/arnold.html MR1618209 (99k:00011) 2. Ralph Back, Jim Grundy, and Joakim Von Wright, Structured calculational proof, Formal Aspects of Computing 9 (1997), 469–483. http://crest.abo.fi/publications/public/ 1997/Structured Calculational ProofA. pdf 3. Ralph Johan Back and Joakim Von Wright, Mathematics with a Little Bit of Logic: Structured Derivations in High-School Mathematics, Åbo Akademi University, 2006. 4. bellaG. Bashmakova and Galina S. Smirnova, The birth of literal algebra, The American Mathematical Monthly 106 (1999), no. 1, 57–66. MR1674194 (99m:01003) 5. bella G. Bashmakova, Galina S. Smirnova, The literal algebra of Viète and Descartes, The American Mathematical Monthly 106 (1999), no. 3, 260–263. 6. Richard Blahut, Principles and Practice of Information Theory, Addison-Wesley, 1987. 7. Jon Blntley, Programming Pearls, 2nd edition, Addison-Wesley, 2000. 8. Raymond Boute, The Geometry of Bandpass Sampling: A Simple and Safe Approach", IEEE Signal Processing Magazine 29, 4, pp. 90–96 (July 2012). 9. Raymond Boute, The Euclidean definition of the functions div and mod, ACM TOPLAS 14 (1992), no. 2, 127–144. 10. Raymond Boute, Functional declarative language design and predicate calculus: A practical approach, ACM TOPLAS 27(2005), no. 5, 988–1047. 11. Carl B. Boy and Uta C. Merzbach, A History of Mathematics, second edition, Wiley, 1991. MR0996888 (90f:01001) 12. Ronald N. Bracewell, The Fourier Transform and Its Applications, second edition, McGraw-Hill, 1978. MR0549484 (81k:42011) 13. Peter J. Cameron, Sets, Logic and Categories, Springer, 1999. MR1700271 (2001b:03001) 14. Jeffrey Clark, Derivative sign patterns, The College Mathematics Journal 42 (2011), no. 5, 379–383. 15. Mary Jona Collison, The unique factorization theorem: Fforb Euclid to Gauss, Mathematics Magazine 53 (1980), no. 2, 96–100. MR0567958 (82f:01006) 16. Edsger W. Dijkstra, How computing science created a new mathematical style, EWD 1073 (1990). http://www.cs.utexas.edu/users/EWD/ewd10xx/ EWD1073.PDF MR1175013 (93i:68004) 17. Paulo J. S. G. Ferreira and Roeland Higgins, The establishment of sampling as a scientific principle, Notices of the AMS 58 (2011), no. 10, 1446–1450. MR2884025 (2012m:94193) 18. Wim H. J. Feyen, Antoinetta J. M. Van Gasteren, David Gries, and Jayadev Misra, eds., Beauty Is Our Business, Springer, 1990. MR1147649 (92i:68005) 19. Mohna Ganesalingam, The Language of Mathematics, Ph.D. thesis, University of Cambridge, 2009. http://people.pwf.cam.ac.uk/mg262/ GanesalingamMdi s.pdf 20. Mohna Ganesalingam, The Language of Mathematics, presentation, 2010. http://www.srcf.ucam.org/principia/ files/ganesali ngam.pdf 21. Bonnie Gold, How your philosophy of mathematics impacts your teaching. The College Mathematics Journal 42 (2011), no. 3, 174–182. 22. David Gries, Improving the curriculum through the teaching of calculation and discrimination, Communications of the ACM 34 (1991), no. 3, 45–55. 23. David Gries, and fred B. Schneider, A Logical Approach to Discrete Math, Springer, 1993. MR1247233 (94j:03002a) 24. David Gries, fred B. Schneider, Teaching math more effectively, through calculational proofs, The American Mathematical Monthly 102 (1995), no. 8, 691–697. MR1542732 25. Paul Halmos and Steven Givant, Logic as Algebra, volume 21 of The Dolciani Mathematical Expositions, The Math. Assoc. of America, 1998. MR1612588 (99m:03001) 26. John Harrison, Formal proof-theory and practice, Notices of the AMS 55 (2008), no. 11, 1395–1406. MR2463992 (2010h:03013) 27. John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge, 2009. MR2503047 (2011d:68157) 28. Israel N. Herstein, Topics in Algebra, Xerox College Publishing, 1964. MR0356988 (50 #9456) 29. Randall Holmes, Elementary Set Theory with a Universal Set, http://math.boisestate.edu/∼ho1mes/ holmes/head.pdf 30. John L. Kelley, General Topology, Van Nostrand, 1953. MR0070144 (16,1136c) 31. Morris Kline, Mathematics in Western Culture, Oxford University Press, 1953. MR0061056 (15,769a) 32. Steven G. Krantz, Real Analysis and Foundations, second ed., Chapman & Hall/CRC, 2005. MR2107580 (2005g:00003) 33. Leslie Lamport, How to write a proof, The American Mathematical Monthly 102 (1995), no. 7, 600–608. http://www.jstor.org/pss/2974556, or the 1993 manuscript at http://research.rnicrosoft.com/ en-us/um/people/1amport/pubs/1amporthowto-wri te.pdf 34. Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Pearson Education Inc., 2002. 35. Leslie Lamport, How to Write a 21st Century Proof, technical note, Microsoft, November 2011. 36. Eeward A. Lee and Pravin Varaiya, Introducing signals and systems-the Berkeley approach, in First Signal Processing Education Workshop, Hunt, Texas, October 2000. http://ptolemy.eecs.berkeley.edu/publications/papers/00/spel 37. Eeward A. Lee, Pravin Varaiya, Structure and Interpretation of Signals and Systems, Addison-Wesley, 2003. 38. S. K. Lui, An interview with Vladimir Arnoi'd, Notices of the AMS 44 (1997), no. 4, 432–438. MR1435453 (97k:01039) 39. Richard G. Lyons, Understanding Digital Signal Processing, Prentice Hall, 2004. 40. JohnH.Mason, On the use and abuse of word problems for moving from arithmetic to algebra, in The Future of the Teaching and Learning of Algebra, Proc. 12th ICMI Study Conference, Helen Chick, Kaye Stacey, Jill Vincent, and John Vincent (eds.), December 2001, pp, 430–437. 41. Reviel Netz and William Noel, The Archimedes Codex, Phoenix, London, 2008. MR2479401 (2009m:01005) 42. Dag Prawitz, Natural Deduction, a Proof-Theoretical Study, Dover, 2006. 43. Walter Rudin, Principles of Mathematical Analysis, McGraw-Hill, 1964. MR0166310 (29 #3587) 44. Lucio Russo, The Forgotten Revolution, Springer, 2004. MR2038833 (2004k:01006) 45. Yoram Saher, What Pythagoras could have done, The American Mathematical Monthly 95 (1988), no. 2, 117. MR1541252 46. Chris Sangwin, Modelling the journey from elementary word problems to mathematical research, Notices of the AMS 58 (2011), no. 10, 1436–1445. MR2884024 (2012j:00010) 47. Patrick Suppes, Axiomatic Set Theory, Dover, 1972. MR0349389 (50 #1883) 48. Alfred Tarski and Steven Givant, A Formalization of Set Theory without Variables, AMS Colloquium Publications, volume 41, American Mathematical Society, Providence, Rhode Island, 1987. MR0920815 (89g:03012) 49. Paul Taylor, Practical Foundations of Mathematics, no. 59 in Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1999. http://www.cs.man.ac.uk/∼pt/ Practi cal Foundations/htm1/s10.html. 50. Antoinetta J. M. Van Gasteren, On the Shape of Mathematical Arguments, Springer Lecture Notes in Computer Science, no. 445, Springer, 1990. http://www.springerlink.com/content/ 978–3-540–52849-4 MR1069949 (92f:68109) 51. Daniel J. Velleman, How to Prove It: A Structured Approach, second ed., Cambridge, 2006. MR2200345 Note: This list reflects references listed in the original paper as accurately as possible with no attempt to correct errors. c© Copyright American Mathematical Society