[Math] Towards Proof Writing as a Skill In Itself
In the vein of Nate, David and TT, I’m currently reading through and working on a review of Halmos’s Naïve Set Theory, from the MIRI course reading list.
My background in higher mathematics is so far two 300-level courses I have taken the past two quarters at Northwestern University:
MATH 306, Combinatorics, which was mostly calculations and light on formal proofs until the end, and
MATH 300, Introduction to Higher Mathematics, which is about… Nothing but formal proofs.
MATH-300 is intentionally limited in scope so that we only prove trivial statements, until near the very end. At first I thought this would be an easy A, and a bit of a waste of time. It turned out to be neither of those things.
Writing rigorous proofs, when you don’t have a lot of practice, is always harder than you would expect, even for trivially obvious statements. A few reasons I noticed:
You need to hew very closely to definitions and “allowed actions” in terms of inference. It’s easy to make an ‘obvious’ logical leap that fails to convince the reader at all. It truly is like learning to cross inferential distances at a snail’s pace.
You need to learn the common tricks of the trade—for example, “A if and only if B” is usually proved by proving “if A then B” and then separately proving “if B then A”, making it essentially a 2 sub-proof project. “If A then B” is logically equivalent to “if not B then not A”, which is sometimes much easier to prove (EDIT: although discouraged, because this makes the proof non-constructive—see comments). Et cetera, et cetera.
You need to become diligent about proofreading, especially if you’re typesetting with LaTeX. A single misplaced symbol will cost you a point, because the whole point is to drill the rigor into you to proofread your damn homework.
Imagine trying to build all of that, while actually learning new concepts. It’s going to take you forever.
(Personal story time, feel free to skip.) I actually started with another proof-based course, Graph Theory. I dropped it, not because my grades were at all poor, but because my homework took. So. Damn. Long. And after hours of effort, I would still lose points for very small errors in places I thought were perfect.
It was infuriating. I backed off, realized that I hadn’t built my skills in the right order, and dropped the course, so that I would only take the proof writing one this quarter. I don’t regret that at all. The next time I take Graph Theory, I am confident that it will go much smoother, because I actually know how to write a proof.
(Having the first few homeworks already done in LaTeX won’t hurt, either. 😉)
Nate, David and TT all remark on how NST is a dense read. Dense yes, difficult not necessarily at all. I’m finding my experience after a proof writing class to make the text very easy to read, despite (or maybe due to!) the frequent breaks to attempt proofs of the authors’ statements myself.
My NST experience suggests to me, then, that proof writing is an excellent example of a component skill. Principle 4 of How Learning Works states that
To develop mastery, students must acquire component skills, [then] practice integrating them, and [finally] know when to apply what they have learned. [emphasis mine]
So learn it in isolation first, if you can. It will make all future endeavors in proof-based math much smoother.
This hits home, and reminds me that perhaps I should go back and drill a bit more. I do feel that I am starting to get a sense for whether sufficient rigor is present in my proofs. However, perhaps more certitude would feel better than my constant, self-imposed paranoia about whether I’m secretly handwaving the details.
Also, you can use emoji in LW posts?! 😈
Careful here, because this transformation is enough to make your proof non-constructive! Since we’re learning “how to write proofs”, it’s worthwhile to follow good proof-structuring rules, one of which is to keep things constructive as far as practicable.
Can you elaborate? What is a constructive proof? Why should one care?
A proof is “constructive” if it doesn’t depend (implicitly or explicitly) on proof by contradiction. A roughly equivalent way to say this is, which I think is the reason for the name “constructive”, is that if you want to prove “there exists x such that P(x)” you need to do it by actually exhibiting such an x, rather than by saying “suppose there is none …” and deriving a contradiction.
Some mathematicians outright reject the tactic of proof by contradiction, and correspondingly also reject the “law of the excluded middle” which states that for any p, either p or not-p must be true. (These mathematicians are rather puzzlingly called “intuitionists”. The original motivation for this position was the idea that mathematics is a human creation, that when one asserts a mathematical proposition one is really gesturing towards some sort of mental construction that corresponds to it; so, say the intuitionists, when you assert that some mathematical entity exists, you’d better actually have an instance of it in mind.) Others consider that non-constructive proofs are valid but that constructive proofs are better.
Why would one prefer a constructive proof? The obvious reason is that in some sense it tells you more. If you have a constructive proof that a certain kind of thing exists, you can (in principle) use that to find such a thing; if you only have a non-constructive proof then you might remain unable to do that.
Another reason would be that you actually do want to allow some propositions to have no truth-values, or truth-values other than “true” and “false”. E.g., you might want a system that allows explicitly for ambiguity or uncertainty or something of the kind. Intuitionism kinda falls into this category; the “third” truth value might be called “incomplete” or “unknown” or something.
There are also interesting connections between the kind of restricted logic you need to use to invalidate non-constructive proofs (in which, as I mentioned above, “p or not-p” is not a theorem) and computer programs. Specifically, there’s a thing called the Curry-Howard isomorphism that says that types (in the programming-language sense) correspond to propositions in logic, and then explicit objects of those types correspond to constructive proofs of those propositions.
Disclaimer: it’s years since I studied any of this stuff, so there may be errors in the above; and I have never been an intuitionist nor found intuitionism credible, so I may not have presented it very fairly.
https://en.wikipedia.org/wiki/Constructive_proof
I am very inexperienced in this particular part of formal set theory, but I was always informally told that the main reason the distinction between constructive and non-constructive proofs is related to the Curry-Howard Correspondence, which informally states that constructive proofs can be rewritten into computer algorithms, whereas non-constructive proofs can not.
I got permission from the math department at Rutgers to skip the proof-writing class… I think I must have picked up the skill elsewhere, because I didn’t feel like I had any trouble with the proof-based linear algebra and real analysis classes that would normally require the proof writing class as a prerequisite.
(The most likely places I learned the skill was from non-textbook books on mathematics and from the philosophy department’s classes on formal logic that I used to cheat on my degree’s humanities requirement.)
Nice dude!
I don’t think this refutes my essential point, but it does add a caveat to it that might help exceptions realize when such a course wouldn’t actually help them much. I’ve never taken a course in logic, and have in fact only recently cracked open a book on FOL proper.
This confirms my experience so far. I tried to read Naive Set Theory, but after like 3 chapters I realized that the author already expects me to know how proofs work. I used the book How to prove it by Daniel J. Velleman to learn how to write proofs. I cannot say whether this is the best book out there, but it is definitely useful for self-study. It has a lot of exercise problems after every section and solutions for 30-50% of them. I went through roughly half of the book. I am currently taking linear algebra and real analysis in university and I feel more comfortable about the class than a lot of my classmates.