2.1: Naïvely
( \newcommand{\kernel}{\mathrm{null}\,}\)
What is it that makes mathematics different from other academic subjects? What is it that distinguishes a mathematician from a poet, a linguist, a biologist, or a civil engineer? We are sure that you have many answers to that questions, not all of which are complimentary to the authors of this work or to the mathematics instructors that you have known!
We would like to suggest that one of the things that sets mathematics apart is the insistence upon proof. Mathematical statements are not accepted as true until they have been verified in a very particular manner. This process of verification is central to the subject and serves to define our field of study in the minds of many. Allow us to quote a famous story from John Aubrey's Brief Lives:
[Thomas Hobbes] was 40 years old before he looked on Geometry; which happened accidentally. Being in a Gentleman's Library, Euclid's Elements lay open and 'twas the 47 El. libri 1 [the Pythagorean Theorem]. He read the Proposition. By G--, sayd he (he would now and then sweare an emphaticall Oath by way of emphasis) this is impossible! So he reads the Demonstration of it, which referred him back to such a Proposition; which proposition he read. Et sic deinceps [and so on] that at last he was demonstratively convinced of that trueth. This made him in love with Geometry.
Doesn't this match pretty well with your image of a mathematical proof? To prove a proposition, you start from some first principles, derive some results from those axioms, then, using those axioms and results, push on to prove other results. This is a technique that you have seen in geometry courses, college mathematics courses, and in the first chapter of this book.
Our goal in this chapter will be to define, precisely, something called a deduction. You probably haven't seen a deduction before, and you aren't going to see very many of them after this chapter is over, but our idea will be that any mathematical proof should be able to be translated into a (probably very long) deduction. This will be crucial in our interpretation of the results of Chapters 3 and 5, where we will discuss the existence and nonexistence of mathematical proofs.
If you think about what a proof is, you probably will come up with a characterization along the lines of: A proof is a sequence of statements, each one of which can be justified by referring to previous statements. This is a perfectly reasonable starting point, and it brings us to the main difficulty we will have to address as we move from an informal understanding of what constitutes a proof to a formal definition of a deduction: What do you mean by the word justified?
Our answer to this question will come in three parts. We will start by specifying a set
The proofs that you have seen in your mathematical career have had a couple of nice properties. The first of these is that proofs are easy to follow. (OK, they aren't always easy to follow, but they are supposed to be.) This doesn't mean that it is easy to discover a proof, but rather that if someone is showing you a proof, it should be easy to follow the steps of the proof and to understand why the proof is correct. The second admirable property of proofs is that when you prove something, you know that it is true! Our definition of deduction will be designed to make sure that deductions, too, will be easily checkable and will preserve truth.
In order to do this, we will impose the following restrictions on our logical axioms and rules of inference:
- There will be an algorithm (i.e., a mechanical procedure) that will decide, given a formula
, whether or not is a logical axiom. - There will be an algorithm that will decide, given a finite set of formulas
and a formula , whether or not is a rule of inference. - For each rule of inference
, will be a finite set of formulas. - Each logical axiom will be valid.
- Our rules of inference will preserve truth. In other words, for each rule of inference
, .
The idea here is that although it may require no end of brilliance and insight to discover a deduction of a formula