You want proof? I'll show you proof!
Mathematical proofs have a special place in the spectrum of human knowledge. In no other field are the claims so certain, the conclusions so universally accepted as correct. Why is this? What is the secret behind mathematical proofs that accounts for their incredible success?
Intuition and Objectivity
There are two traits which characterize a good mathematical proof of a claim. First, it should provide an explanation that will help the reader understand on an intuitive level why the given claim is true. Second, it must be objective. The veracity and correctness of the proof should not depend on subjective opinion of anyone.
But these two claims are sometimes not mutually compatible. What if two people have a different intuitive impression of the same claim? One intuitively believes it is true, another believes it is false? How can we referee such a situation to maintain the objective nature of our mathematical results? How can we achieve objectivity in our proofs?
One solution is to take intuition and subjectivity out of the picture completely by devising a completely algorithmic mechanism for determining if our proof is correct. If a machine, an electromechanical device with presumably no intuition whatsoever can verify that our proof is correct, then we can be confident that no personal subjective bias or intuition is required. Proofs of this sort, which can be verified algorithmically by a computer (in theory) in a finite amount of time are often referred to as formal proofs.
One drawback to formal proofs is that they can be quite lengthy and detailed and tedious, sometimes obscuring the intuitive understanding we wish to achieve with our proofs. Most of the mathematical proofs found in math textbooks and journals are not formal proofs. Instead an experienced mathematician tries to convey to his audience two things: (1) a lucid intuitive explanation of why the claim being proved must be valid and (b) enough details about the key steps in a formal proof of the claim that his audience could, if needed, produce a formal proof of the statement. Thus, a typical mathematician uses many shortcuts and convenience conventions to convey to give his proofs the brevity and clarity needed for intuitive understanding of the proof, while providing sufficient information to reconstruct a formal proof of the same claim, thus effectively providing the objective certainty we also demand.
In this introduction to mathematical proofs, we will first introduce you to formal proofs, and then later add shortcuts and convenient conventions that allow you to slowly make the transition from formal proofs to the standard kinds of mathematical proofs found in books and journals. In this way you will first gain a solid, rigorous, objective method of constructing proofs, and later relax the formality to obtain more intuitive informal mathematical proofs. Having a bridge between these two types of proofs, by having a formal proof skeleton and a repertoire of rigorous, well-defined shortcuts for making them more human readable and intuitive, will allow the best of both worlds in our proofs: intuitive understanding and objective certainty.
Toy Proofs!
As you might expect, formal mathematical proofs can be somewhat complicated beasties. Thus, we begin by introducing smaller "Toy" proof systems that illustrate some of the basic features of a real formal proof system, but do it in small incremental steps that illustrate the common mechanisms involved.
In some sense making a formal proof is like playing a game. The kinds of games we have in mind have the following features in common.
- Toys: These are the objects you play with in your game. Toys can be anything: a single number, a list of numbers, a word, a sentence, a geometric shape, a mathematical statement like x2 + y2 = z2, an assumption, a color. (In a formal mathematics proof the toys are usually mathematical statements.)
- A Goal: The game must have a special toy called the goal. The object of the game is to produce that particular goal toy. If you successfully produce the goal, you win! (In a formal mathematics proof the goal is the statement that you are trying to prove.)
- The Starting Position: The game provides you with zero or more toys to start with that you can use to build other toys. (In a formal mathematics proof these are the 'Givens' or hypotheses.)
-
The Rules: What would a game be without rules? This is a set
of one or more rules that allow you to construct other toys in the
game from the toys that you already have and other information. The
essential feature that all such rules must have is that the are
completely precise, unambiguous, and algorithmic in nature. (In a
formal mathematics proof these are the rules of inference that are
used to deduce that one statement follows from other statements.)
Each such rule will have the following features.
- Inputs: The inputs usually consist of zero or more toys that you already have available (either because you constructed them or they were given to you as part of the Starting Position) and other information that you might provide.
- Output: The output usually consists of a single toy that is produced by the rule. We say that such a toy have been 'constructed' or 'justified' by the rule and is then usually added to your collection of available toys.
Each of these aspects are illustrated in the games that follow.
Let's Play!
In this collection there are currently four games: Stars!, Scrambler!, TrixGame, and Circle-Dot. You can read the help file for each game before you begin if you wish, but they are fairly self-explanatory if you want to dive right in and try them. Each illustrates the concept of a formal proof in a way that is simpler than what you will encounter when you do actual formal mathematical proofs. There is also some sophisticated mathematics hidden behind the first two games. Beware - all three games can be quite addictive!