Basics of Proofs (2017) [pdf](theory.stanford.edu) |
Basics of Proofs (2017) [pdf](theory.stanford.edu) |
I later learned that there is indeed a precise way of learning proofs which doesn't rely on intuitions of what counts as a rigours inference step: Formal logic together with a natural deduction proof system. Natural deduction is a formal proof system which resembles actual ("natural") proofs in mathematics, unlike other proof systems.
In such a proof system, inference rules, like modus tollens or universal instantiation, are strictly defined. Only the given inference rules (and those which are provable from the given rules) may be used. Coming up with such proofs still requires creativity, there is no algorithm. But there is no ambiguity in what counts as a valid or invalid proof or inference step.
Of course, this is far too tedious for actual mathematical proofs, since every little step needs to be done explicitly, e.g. even applications of modus ponens (rule: "A, if A then B, therefore B"). Moreover, mathematicians rarely prove anything from axioms, they start from other statements which are considered more trivial. But I think it would be helpful for many people to first learn logic and deduction "the precise way", and then do actual mathematical proof where you can jump over more obvious parts.
But that's not how it is teached in mathematics or computer science. Students are thrown into the cold water, and only receive tips&tricks, but no rigorous introduction. Ironically, the one subject which often teaches formal logic as an early introductory class for undergraduates isn't mathematics, computer science, or physics, it's philosophy.
Whenever I have asked professors in the past how they first learned proofs the answer was always from doing Euclid in highschool which is no longer taught
(A small downside is, in my opinion, that is uses trees instead of a more classical sequential presentation in the style of Suppes and Kleene.
https://en.wikipedia.org/wiki/Natural_deduction#Different_pr...
Trees may be more elegant, but actual, informal proofs in mathematics are written sequentially. So I think trees defeat the purpose of "natural" deduction a bit. But that's complaining on a high level.)
What is unusual is that I kept looking. "How to Prove It" was something I really wish I read ahead of calculus. It is only after this book it clicked for me, all of it. Having understood the rules of the game it became possible to play with math..! Which I still do from time to time.
I think that this material should be taught at high school. Bits of it even earlier.
[1] It is amazing (or not, depending on your view of lawyers) that lawyers are basically not taught anything about making and proving formal arguments, at least in my experience.
Absolutely. And I can not imagine a mathematics degree which doesn't place formal logic front and center in the first semester. When you are starting out you absolutely need to suffer through the rigourous formal arguments.
>Ironically, the one subject which often teaches formal logic as an early introductory class for undergraduates isn't mathematics, computer science, or physics, it's philosophy.
I can not believe that this is the case. Even engineering undergrads have to learn formal logic in their first semester.
I got my engineering B.S. from a top 5 college in the US, and have known many people who have gone to similar schools. None of us have had to take a class that goes into first order logic or proof writing. I don't know what college you go to where that is a thing, but it would be exceedingly rare.
Geometry class in high school sometimes teaches some of it.
Computer science Binary logic teaches some of (De Morgan's laws)
Outside of New Math of the 1970s, it is a glaring omission from the curriculum.
Even enriched classes like Art of Problem Solving that put heavy emphasis on proofs, do not teach formal logic.
This was precisely my issue when studying proofs in school. Do you have any suggestions for resources to get started down the right path?
Not more trivial but from the ones already proved and those closer to the thing you are proving. There is no need to go back to the axioms if you know, and can reference, proof of step N-1, just go from there.
There is also this 'misconception' that mathematical theorems follow from the axioms. They do, of course, but the axioms were choosen just right to make things that were working to still work, with some weird consequences like axiom of choice
Some people are just wired differently.
I agree that full formal logic could be too much irrelevant information, but I think many experienced people underestimate how non-obvious the basic inference rules are to novices, and how confused people are about just being told to produce "convincing arguments". The important part is that the argument has to be truth preserving, unlike a "convincing argument" or "proof" an attorney might give in court. It is very hard to understand this difference if one has only a hazy idea of logic and deduction vs induction.
A lot of people are exposed to Geometry in High School. It might not be universal, but it's pretty close. IIRC, Eucid's Elements was the second most read book, after the Bible. Many cities even have a street named after the guy.
I know, it's not the same as a formal logic course. But it's not that far off, either. There is some preparation in earlier years of schooling.
https://docs.google.com/document/d/1_uwl3WDZk_BxNOUL7W0FiPMM...
I literally gave everyone that handout and told them, "To make sense of it, you're all going to do the next proof. I'll just prompt you." They thought this was impossible. But I told them to trust me and I began.
I went around the room. I asked one person what the next step in the flowchart was. I asked the next person to do it. I just wrote down what they said. Kept going until they had produced a complete proof of a result that, at the beginning, they did not know why it might be true.
The best comment I got from that class later was, "Proofs are easy. It is kind of like filling out a shopping list."
For example, I broke down problems with to-dos, such as:
1. Find the definition for what math_term_X means in a particular problem.
2. (For breaking down part of the problem): Figure out how to show that a particular object is lesser than or equal to another project.
3. Write down headings for each case I need to prove.
...and so on.
Writing down explicit steps was far more practically helpful to me, than my previous conception of problem-solving from the quote about how Feynman solves problems (that is: "Write down the problem, think real hard, write down the solution"). Some people may not need to write down steps, but I was personally able to learn a lot more with a specific, more verbalized approach.
It's very neat and helpful to have a flowchart suited to any general problem, which I'll try out in addition to my current approach of writing down a list of to-dos for solving specific problems. Thanks a lot for sharing.
Are you beginning to doubt whether it's true?
Try to think of a counterexample.
Is there something that keeps getting in the way of a counterexample working? Can you prove that that always happens?
:-)
[0]https://www.amazon.com/Proof-Art-Mathematics-Examples-Extens... [1] https://twitter.com/paulg/status/1662065331727155202
[1] https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...
Lemma: ......
Proof: ....
etc.
Theorem: Let epsilon < K, ....
Proof: ....
--QED--
which we all dutifully copied into our notebooks. Very uninspiring.
But when I got to the University of Waterloo for graduate studies, I had a real competitive advantage over my peers for the theory courses I took: I knew what a proof was, and how to do one.
I had 5 years of that, a very enjoyable time.
This is the third time I notice such a coincidence on HN. Is this something that HN does on purpose? Like, does the site match posts with similar titles on the front page to encourage discussion in both? Note that (at the time of writing) this article has 91 points and the other one 45, so the two articles are not ordered by upvote count.
Also, I need a catchy name for this phenomenon (just 'cause I want to name the folder where I keep screenshots documenting it, like). Suggestions?
No, the HN algorithm is extremely simple and does not consider syntactic similarities of the titles.
Can't really give an example question, it's been well over a decade (closer to two) since I took it.
For example, the above Stanford document on proof basics doesn't even mention elementary inference rules like modus tollens. It briefly refers to "the contrapositive", but without explaining what the contraposition rule even is. It was clearly written by someone who regards all these as too obvious to be mentioned in such a document (he only explains proof by contradiction), but they are not obvious to novices.
Anyway, your comment reminds of an interesting paper[1] by Yehuda Rav, where he defends the autonomy of informal proof with original arguments against the "formalists". You might be interested, I think your intuitions are going in a similar direction.
[1] http://sgpwe.izt.uam.mx/files/users/uami/ahg/1999_Rav.pdf
The thing is, formal rules can only model what you already understand. A formal rule can tell you exactly WHAT and HOW, but not WHY. But especially with basic proof rules like modus ponens, that is essential. So intuitive understanding is prior to formal rules. Of course, lots can be gained from the interplay of intuition and formality, I am the last one to deny that.
For me, that is an important issue, because I am a big proponent of doing logic on the computer, which necessarily is formal. Nevertheless, the goal here is to make logic on the computer as intuitiv as possible, something many people in the field don't seem to have a desire for. I also don't want the next generation to think exclusively in formal systems, in terms of, oh, if my formal system doesn't allow that, what I want to do must be wrong, or at least stupid. There is already enough of that going around with type theorists.
That's because first-order logic (and any system that extends it) is formally undecidable, so there can be no algorithm that, for a given statement, determines whether it is a valid theorem. If you restrict yourself to propositional logic, you gain decidability but, in the general case, it's still extremely inefficient (unless P=NP).
Of course, in order to prove these things, you have to formally develop what logic is.
> Mathematical proof is really just for convincing other mathematicians
which is precisely the point of a proof, but 'convince' means something different than you seem to think it means (in the field of mathematics)
Can you name some? Preferably in analysis.
https://ncatlab.org/nlab/show/list+of+lost+manuscripts+in+ca...
Further is it any relevant theorem, which has been cited many times?
German technical university. I was a tutor there. AFAIK this is normal.
As part of the first semester you take linear algebra and analysis, starting out with the basics of formal logic. Of course the courses are less focused on proof writing than the mathematics "major" courses.
I should also point out that German universities have very loose entry standards (except when places are very rare compared to applicants) and use the first two semesters to filter out students. These courses are often designed to have around a 50% failure rate.
There is not enough time to learn the basics of formal logic and linear algebra and/or analysis in a single class, but I think what you’re referring to is an introduction to proof techniques like induction, modus tollens, quantifiers, etc.
Every math and computer science department in the US that I’ve ever heard of teaches these topics, but I wouldn’t call it a formal logic class.
How can you teach analysis without that anyway. It is absolutely essential for set theory and how would you e.g. define the reals (in a "proper" math course, not engineering) without a good understanding of set theory?
If you don't believe me, here is a link to the contents of a first semester engineering math course from some german technical university: https://page.math.tu-berlin.de/~joswig/teaching/notes/Joswig...
The symbols should be enough to tell you what the contents are.
The enormous upside is that all students are judged equally on their ability to academically succeed in their chosen field. I think US university admissions are ridicolous for many reasons.
John Beck's Monadicity Theorem is cited in "many sources" but a manuscript has been found and "The proof is reproduced for instance in (MacLane, p. 147-150, Riehl 2017, 5/5/)".
Fred Linton cites Michael Barr for a "Universal property of the Kleisli construction" and no copy has been found.
I don't know enough about the subject to say how difficult these proofs would be to recreate or whether they exist elsewhere, but these definitely seem to be specific theorems.
I'd like to see a specific theorem in any field that was once proven and accepted but all existing proofs have been lost. That would be extremely tantalizing
The first one isn't lost at all, the second is just a single lost citation.
All of this is very far away from mathematicians building upon thr shaky grounds of mythical theorems. Also, in all my mathematical experience (going up to recent research in analysis) I never encountered something like this. In all textbooks I ever read either everything was proven or was cited to other works, which every time I checked included the proof.
That's really only baby logic. Which, probably, is what will be sufficient for most mathematician most of the time.
A real first introduction to formal logic would introduce an actual formal proof system and go at least as far as proving completeness of first order logic.
Instead of (literally) infantalizing the name, you could also call it basic formal logic.
If you do want to study logic formally, the basics start with well-formed formulas, signatures, etc.
I guess what you call it doesn't matter a lot, but the discussion seems to have started with the assertion that most students, even in mathematics, never really learn formal logic, and I would agree with that (under my definition of "formal logic"), while also agreeing with you that you can't pursue a degree in maths without knowing how induction works or what a bijection is. But still, most people don't need to know exactly how to formalise induction and that it's actually (in its full form) a second-order axiom.
Formalization? Like a computer checked proof?
Lean: https://leanprover-community.github.io/mathlib_docs/logic/fu...
Coq: https://github.com/bmsherman/finite/blob/63706fa4898aa05296c...
Isabelle: https://isabelle.in.tum.de/website-Isabelle2009-2/dist/libra...
Yes, that would be an example, though not all formalizations are written in software. I was originally talking just about standard formal logic, which is just first-order predicate calculus. Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)
So I can't actually read these proof assistant languages, as they are using some advanced type theory based language. So just a few comments.
Lean: It looks suspicious that this seems to involve just one to two lines. Are they actually proving anything here? It doesn't look at all like Cantor's diagonal argument.
Coq: This looks better, at least from the description, and that it actually looks like a proof (Coq actually has a Qed keyword!). Though they, unlike Cantor, don't talk about real numbers here, just about sequences of natural numbers. Last time I read a discussion about it, it was mentioned that this exactly was a problem for the formal proof: Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.
Isabelle: That seems to be a formalization of Cantor's powerset argument, not his diagonal argument.
Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y. X could be simply a different proof, or one which is similar but uses stronger or question begging assumptions, etc. One such example is informal proofs (like Cantor's) which didn't work in any axiomatized system, and where it isn't clear how much you can assume for a formal version without being question begging.
The lean proof seens correct, I can't read lean well, but it appears to just be a formalization of the standard proof. It at least constructs the set needed for the proof.
>Proof assistants use much more powerful systems in order to gain the same expressibility as the natural language which is used in informal proofs. (Which is kind of strange: In using natural language mathematicians don't seem to be using some advanced type theory.)
Look up "Curry-Howard isomorphism".
>Overall, this highlights a major problem with formalization of existing proofs. There is no way (at least no obvious way) to "prove", that a formal proof X actually is a formalization of some informal proof Y.
And? This seems not relevant to the question at hand. Surely some textbook contains an insufficient proof, which couldn't be formalized without more steps. Why does that matter. The question still is whether "folk theorems" are real. Certainly Cantor's theorem is no such folk theorem, as you have just been given a fully formal proof.
>Though they, unlike Cantor, don't talk about real numbers here
Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.
>Every natural number sequence (with a decimal point) corresponds to some real number, but real numbers don't necessarily have just one decimal expression, e.h. 0.999...=1. So real numbers and sequences can't straightforwardly be identified.
This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.
>because informal proofs treat all the most obvious parts as obvious.
No, they treat the most obvious parts as previously proven (which they are). That is an enormous difference.
I really have no idea what the difference to a "fully formal" and the standard proof would be, except the later argument includes verbose commentary, instead of logical symbols. But saying "since a is true and we formerly proved a implies b, we know b is true" instead of "(a and (a => b)) => b", does only seem to be a pedantic difference.
>Last time I checked there was still no formal version of Cantor's diagonalization argument.
AFAIK it is part of the standard libraries of multiple proof assistants, which means it is as fully formal as it can ever be.
> No, they treat the most obvious parts as previously proven (which they are).
Well, I don't agree here. If you look at the history of mathematics, it shows that it progressed often in the opposite direction, where many "basics" were proven very late, e.g. by Dedekind, Peano, and Russell/Whitehead. Not to mention all these details which are now are getting expressed in languages for proof assistants. Many of these details couldn't even have been proved earlier, because the necessary formal systems were only invented recently.
> I really have no idea what the difference to a "fully formal" and the standard proof would be
Just look at actual formal proofs. They are very different from informal ones. To approximate the natural language of informal proofs, proof assistant languages actually have to use logics with advanced type systems, which most people who just write informal proofs wouldn't even understand.
> But saying "since a is true and we formerly proved a implies b, we know b is true" instead of "(a and (a => b)) => b", does only seem to be a pedantic difference.
It's more like they write "A, therefore B" (or even "A, then one easily sees that B") where the step from A to B is considered obvious by the guy who wrote the proof (a reviewer might reject it and ask for more intermediate steps, if he feels the "A therefore B" step isn't obvious), and where usually no commentary like "and we formerly proved A |= B" is included. Proofs are in fact not plastered with such commentaries, and if they were, people would expect a reference to where this was proven previously. But they don't expect references to obvious steps, because they are obvious, not because they necessarily expect they were proven previously somewhere. That wouldn't even make sense, since many theories were not, or are still not, axiomatized, so respective proofs have to rely on things that are considered obvious.
I already cited Yehuda Rav's 1999 paper "Why Do We Prove Theorems?"[1][2] elsewhere in this thread, and it's again relevant here.
From p. 13:
> A proof in mainstream mathematics is set forth as a sequence of claims, where the passage from one claim to another is based on drawing consequences on the basis of meanings or through accepted symbol manipulation, not by citing rules of predicate logic.4 The argument-style of a paper in mathematics usually takes the following form: '... from so and so it follows that..., hence...; as is well known, one sees that...; consequently, on the basis of Fehlermeister's Principal Theorem, taking in consideration α, β, γ, ..., ω, one concludes..., as claimed'. Why is it so difficult, in general, to understand a proof? Why does one need so much background information, training and know-how in order to follow the steps of a proof, when the purely logical skeleton is supposed to be nothing more than first-order predicate calculus with its few and simple rules of inference?
From p. 14f:
> In reading a paper or monograph it often happens—as everyone knows too well—that one arrives at an impasse, not seeing why a certain claim B is to follow from claim A, as its author affirms. Let us symbolise the author's claim by 'A —> B' . (The arrow functions iconically: there is an informal logical path from A to B. It does not denote formal implication.) Thus, in trying to understand the author's claim, one picks up paper and pencil and tries to fill in the gaps. After some reflection on the background theory, the meaning of the terms and using one's general knowledge of the topic, including eventually some symbol manipulation, one sees a path from A to A_1, from A_1 to A_2, ..., and finally from A_n to B. This analysis can be written schematically as follows:
> A —> A_1, A_1 —> A_2, ..., A_n —> B.
> Explaining the structure of the argument to a student or non-specialist, the other may still fail to see why, for instance, A_1 ought to follow from A. So again we interpolate A —> A', A' —> A_1. But the process of interpolations for a given claim has no theoretical upper bound. In other words, how far has one to analyse a claim of the form 'from property A, B follows' before assenting to it depends on the agent.
[1] https://doi.org/10.1093/philmat/7.1.5 [2] http://sgpwe.izt.uam.mx/files/users/uami/ahg/1999_Rav.pdf
> In other words, how far has one to analyse a claim of the form 'from property A, B follows' before assenting to it depends on the agent.
Or just prove the implication instead of inventing 'informal logical paths'
Still, the question is, are there "folk theorems", where no proof exist which could be written down fully formal?
I didn't say that Cantor's theorem is a folk theorem, only that some proofs aren't even trivial to formalize. Many other things are trivial to formalize, but they still require filling in a lot of obvious steps. It often wouldn't be practically feasible to prove them with a standard first-order calculus, otherwise proof system languages wouldn't need higher order systems with advanced type theory.
> Cantors theorem usually refers to the existence of uncountable sets, which can be proven by showing that there is no bijection between N and R, but also by showing that there is no bijection between a set and its powerset.
Yes, but I was talking about his diagonal argument, not his powerset argument. That's a different proof from a different paper.
> This is only relevant if you say that the real numbers are "infinte strings of digits", which is not a formal definition and therefore not used in mathematics.
Well, I'm not saying that, but the Coq proof seems to assume it. That was the problem I was talking about.
[1] https://doi.org/10.1093/mind/IV.14.278 [2] https://en.wikipedia.org/wiki/What_the_Tortoise_Said_to_Achi... [3] https://www.jstor.org/stable/2253263