type theory | Gyre&Gimble

This post outlines the way that proofs are used in mathematical writing. I have been revising the chapter on Proofs in abstractmath.org, and I felt that giving an overview would keep my mind organized when I was enmeshed in writing up complicated details.

Proofs are the sole method for ensuring that a math statement is correct.

Evidence that something is true gooses us into trying to prove it, but as all research mathematicians know, evidence only means that some instances are true, nothing else.
Intuition, metaphors, analogies may lead us to come up with conjectures. If the gods are smiling that day, they may even suggest a method of proof. And that method may even (miracle) work. Sometimes. If it does, we get a theorem, but not a Fields medal.
Students may not know these facts about proof. Indeed, students at the very beginning probably don’t know what a proof actually is: “Proof” in math is not at all the same as “proof” in science or “proof” in law.

A proof has two faces: Its logical structure and its presentation.

The logical structure of a proof consists of methods of compounding and quantifying assertions and methods of deduction.

The logical structure is usually expressed as a mathematical object.
The most familiar such math objects are the predicate calculus and type theory.
Mathematical logic does not have standard terminology (see Math reasoning.) Because of that, the chapter on Proofs uses English words, for example “or” instead of symbols such as $P\lor Q$ or $P+Q$ or $P||Q$.
For beginning students, throwing large chunks of mathematical logic at them doesn’t work. The expressions and the rules of deduction need to be introduced to them in context, and in my opinion using few or no logical symbols.

Students vary widely in their ability to grasp foreign languages, and symbolic logic in any of its forms is a foreign language. (So is algebra; see my rant.)
The rules of deduction do not come naturally to the students, and yet they need to have the rules operate automatically and subconsciously. They should know the names of the nonobvious rules, like “proof by contradiction” and “induction”, but teaching them to be fluent with logical notation is probably a waste of time, since they would have to learn the rules of deduction and a new foreign language at the same time.
I hasten to add, a waste of time for beginning students. There are good reasons for students aiming at certain careers to be proficient in type theory, and maybe even for predicate calculus.

Presentation of proofs

Proofs are usually written in narrative form
A major source of difficulties is that the presentation of a proof (the way it is written in narrative form) omits the reasons that most of the proof steps follow from preceding ones.
Some of the omitted reasons may depend on knowledge the reader does not have. “Let $S\subset\mathbb{Q}\times\mathbb{Q}$. Let $i:S\to\mathbb{N}$ be a bijection…” Note: I am not criticizing someone who writes an argument like this, I am just saying that it is a problem for many beginning students.
Some reasons are given for some of the steps, presumably ones that the writer thinks might not be obvious to the reader.
Sometimes the narrative form gives a clue to the form of proof to be used. Example: “Prove that the length $C$ of the hypotenuse of a right triangle is less than the sum of the other two sides $A$ and $B$. Proof: Assume $C\geq A+B$…” So you immediately know that this is going to be a proof by contradiction. But you have to teach the student to recognize this.
Another example: in proving $P$ implies $Q$, the author will assume that $Q$ is false implies $P$ is false without further comment. The reader is suppose to recognize the proof by contrapositive.

Translation problem

The Translation problem is the problem of translating a narrative proof into the logical reasoning needed to see that it really is a proof.
Many experienced professional mathematicians say it is so hard for them to read a narrative proof that they read the theorem and the try to recreate the proof by thinking about it and glancing at the written proof for hints from time to time. That is a sign of how difficult the translation problem really is.
Nevertheless, the students need to learn the unfamiliar proof techniques such as contrapositive and contradiction and the wording tricks that communicate proof methodology. Learning this is hard work. It helps for teachers to be more explicit about the techniques and tricks with students who are beginning math major courses.

References

Added 2014-12-19

There’s more to mathematics than rigour and proofs. Post by Terry Tao. The comments on Terry’s post are extraordinarily interesting. Thanks to David Roberts for this reference.

This work is licensed under a Creative Commons Attribution-ShareAlike 2.5 License.

Send to Kindle

This post uses the word intensional, which is not the word "intentional" and doesn't mean the same thing.

The connection between rich view/rigorous view and intensional/extensional

In the abmath article Images and Metaphors I wrote about the rigorous view of math, in contrast to the rich view which allows metaphors, images and intuition. F. Kafi has proposed the following thesis:

The rigorous mode of thinking deals with the extensional meaning of mathematical objects while the metaphoric mode of thinking deals with the intensional meaning of mathematical objects.

This statement is certainly suggestive as an analogy. I have several confused and disjointed thoughts about it.

What does "intensional" mean?

Philosophy

Philosophers say that "the third largest planet in the solar system" has intensional meaning and "Neptune" has extensional meaning. Among other things we might discover a planet ridiculously far out that is bigger than Neptune. But the word "Neptune" denotes a specific object.

The intensional meaning of "the third largest planet in the solar system" has a hidden time dimension that, if made overt, makes the statement more nearly explicit. (Don't read this paragraph as a mathematical statement; it is merely thrashing about to inch towards understanding.)

Computing science

Computer languages are distinguishes as intensional or extensional, but their meaning there is technical, although clearly related to the philosophers' meaning.

I don't understand it very well, but in Type Theory and in Logic, an intensional language seems to make a distinction between declaring two math objects to be equal and proving that they are equal. In an extensional language there is no such distinction, with the effect that in a typed language typing would be undecidable.

Here is another point: If you define the natural numbers by the Peano axioms, you can define addition and then prove that addition is commutative. But for example a vector space is usually defined by axioms and one of the axioms is a declaration that addition of vectors is commutative. That is an imposed truth, not a deduced one. So is the difference between intensional and extensional languages really a big deal or just a minor observation?

What is "dry-bones rigor"?

Another problem is that I have never spelled out in more than a little detail what I mean by rigor, dry-bones rigor as I have called it. This is about the process mathematicians go through to prove a theorem, and I don't believe that process can be given a completely mathematical description. But I could go into much more detail than I have in the past.

Suppose you set out to prove that if $f(x)$ is a differentiable function and $f(a)=0$ and the graph going from left to right goes UP before $x$ reaches $a$ and then DOWN for $x$ to the right of $a$, then $a$ has to be a maximum of the function. That is a metaphorical description based on the solid physical experience of walking up to the top of a hill. But when you get into the proof you start using lots of epsilons and deltas. This abandons ideas of moving up and down and left to right and so on. As one of the members of Bourbaki said, rigorous math is when everything goes dead. That sounds like extensionality, but isn't their work really based on the idea that everything has to be reduced to sets and logic? (This paragraph was modified on 2013.11.07)

Many perfectly rigorous proofs are based on reasoning in category theory. You can define an Abelian group as a categorical diagram with the property that any product preserving functor to any category will result in a group. This takes you away from sets altogether, and is a good illustration of the axiomatic method. It is done by using nodes, arrows and diagrams. The group is an object and the binary operation is an arrow from the square of the object. Commutativity is required by stating that a certain diagram must commute. But when you prove that two elements in an Abelian group (an Abelian topological group, an Abelian group in the category of differentiable manifolds, or whatever) can be added in either order, then you find yourself staring at dead arrows and diagrams rather than dead collections of things and so you are still in rigor mortis mode.

I will write a separate post describing these examples in much more detail than you might want to think about.

Metaphors and intensionality

One other thing I won't go into now: How are thinking in metaphors and intensional descriptions related? It seems to me the two ideas are related somehow, but I don't know how to formulate it.