[cubefox]

When I was first introduced to mathematical proofs, I was perplexed by how fuzzy and intuition-based the notion of proof was. A "convincing argument", really?! There is no knowing, as a novice, how detailed those "arguments" have to be, what parts you can simply assert without further justification. Usually the teachers themselves can't explain what the criteria for an "obvious" and "not obvious" step is, they just know it intuitively from experience. Writing proofs, then, is a lot like having to learn to ride a bike: Instructions are mostly unavailable or useless.

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.

[hackermailman]

Some universities now have a Lean proof assistant logic course that teaches natural deduction http://leanprover.github.io/logic_and_proof/

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

[cubefox]

That course looks like a great introduction!

(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.)

[vkazanov]

I studied CS and electric engineering for 6-7 years total, and both degrees included some pretty math-intense courses, proofs and all. I remember how I really, really wanted an explanation of the underlying proof system but all I got was just more intuitive explanations, all of which felt out of place.

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.

[checkyoursudo]

Philosophy was the only field where I learned formal logic at all. I went into higher math, did some CS, and also got a law degree[1], and am now doing a Ph.D. in informatics, and still the only place I have really been exposed to formal logic was my undergrad degree in philosophy.

[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.

[lixtra]

Law is not about logic. It’s about hermeneutics. It’s closer to religion than to math.

[Solvency]

Which is why the most successful lawyers are more akin to the most successful evangelists: the ability to hoodwink groups of people with their interpretation.

[constantcrying]

> 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.

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.

[141205]

> 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.

[constantcrying]

>I don't know what college you go to where that is a thing, but it would be exceedingly rare.

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.

[l33t233372]

> As part of the first semester you take linear algebra and analysis, starting out with the basics of formal logic

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.

[constantcrying]

For me basic formal logics means learning the symbols (conjunction, disjunction, implication, equivalency, not, etc.) and the rules of inference to maniuplate these symbols and using these rules to prove new things.

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.

[Tainnor]

> For me basic formal logics means learning the symbols (conjunction, disjunction, implication, equivalency, not, etc.) and the rules of inference to maniuplate these symbols and using these rules to prove new things.

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.

[l33t233372]

That level of logic taught to every mathematics and computer science student, and it’s really not what I was thought others in this thread were talking about.

[Solvency]

Your student filtration system sounds like a long and expensive waste of everyone's time.

[constantcrying]

Not really. First year courses usually have hundreds of students in large halls. There is some more effort as you need more tutors, but that is basically it. (Students usually do not live on campus)

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.

[sukilot]

Formal logic is taught in Mathematical Logic class (intermediate, optional) or Discrete math (intro/intermediate, often not taken)

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.

[cubefox]

To be fair, I think some people just quickly and intuitively "get" what's expected from them when doing proofs, without any formal introduction. But for others (like me) it is very much helpful to at least list the basic natural deduction inference rules, and to do a bunch of exercises where they have to use these rules explicitly. Otherwise they are floating in thin air, with only a hazy idea of what a "valid logical step" even is.

[hiatus]

> When I was first introduced to mathematical proofs, I was perplexed by how fuzzy and intuition-based the notion of proof was.

This was precisely my issue when studying proofs in school. Do you have any suggestions for resources to get started down the right path?

[cubefox]

The lecture notes for some introductory logic class of an analytic philosophy department may be quite good, but unfortunately I can't recommend something specific for English.

[yep31]

>some introductory logic class

like forall x from openlogicproject?

[cubefox]

Yes! It looks like a great introduction. Perhaps even better than the Lean course mentioned above. Here is the link:

https://forallx.openlogicproject.org/

[vkazanov]

"How to prove it" is the best book you can find

[layer8]

How do you prove that?

[vkazanov]

With an intuitive explanation!

[cubefox]

"a sequence of thoughts convincing a sound mind" (Gödel 1953, p. 341)

[auxi]

"How to Read and Do Proofs" by Daniel Solow, also there is a playlist on YT with the video lectures, very beginner friendly in my opinion https://www.youtube.com/watch?v=lOnsQUFFUEE&list=PL8GFp_SBW-...

[ithinkso]

> Moreover, mathematicians rarely prove anything from axioms, they start from other statements which are considered more trivial.

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

[cubefox]

There are are a lot of "folk theorems" in mathematics, and things which are simply considered obvious or common knowledge relative to a conjecture in question, without anyone being able to actually cite a proof for that. Mathematical proof is really just for convincing other mathematicians, there is no need to prove things which are considered obvious.

[ithinkso]

None of what you said is true except for

> 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)

[constantcrying]

>There are are a lot of "folk theorems" in mathematics

Can you name some? Preferably in analysis.

[rdlw]

I found this, unfortunately it is about category theory: "manuscripts [...] that are cited but never became widely available"

https://ncatlab.org/nlab/show/list+of+lost+manuscripts+in+ca...

[constantcrying]

Any particular theorem? This links to hard/impossible to access materials, but does any of them actually contain a theorem which proof is not accessible in some form?

Further is it any relevant theorem, which has been cited many times?

[rdlw]

From the link I posted:

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

[spacemadness]

Our discrete mathematics professor leaned heavy on proofs, but also introduced pop quizzes for proofs of algorithms and other mathematical constructs as an experiment that term which sent my anxiety ablaze. You either had the intuition for that particular problem or you didn’t. Studying would not help you that much. The success rate on the quizzes was very low surprising no one.

[StrangeATractor]

Classes like this were funny. I often found that people who just knew the answer immediately had a lot of difficulty doing proofs, and the people good at doing proofs usually didn't arrive at the solution very quickly or seem to have an intuitive understanding of the problem at first.

Some people are just wired differently.

[dvwobuq]

That’s interesting. In your context what is “knowing the answer”? To me it seems like they “knew” a given statement was true but they didn’t know how to prove it which makes me wonder how they knew.

[StrangeATractor]

The teacher may start off a class with a question like "what is the most efficient way to satisfy this problem given these constraints?" Some people would know the answer immediately but couldn't do a proof for it hardly at all. Others could find a proof in class almost every time, but necer really saw the answer to the problem until they'd sat on it for a while and chewed over it.

Can't really give an example question, it's been well over a decade (closer to two) since I took it.

[DiscourseFan]

As someone who tutored a Formal Reasoning class for a top philosophy department, I don't think we should be teaching anyone logic. It's rigid, its made up, and it doesn't help much for most things. I think the way proofs are written in math is cool, and I think the fact that mathematicians are, in the end, aware that it is impossible to rigidly demonstrate anything is perfectly fine and it makes their proofs a lot easier to read and interpret. Formal logic should never be treated as first order or ever used as such, it will only hamper mathematics. I understand the need for a rigorous language to describe mathematics, I understand why people like it so much, and why it has found so much use. It is still not the groundwork (because there is none).

[cubefox]

Would you agree to at least list some of the common natural deduction inference rules in an introductory class, and do a few exercises with them? Like, for propositional logic, modus ponens, modus tollens, contraposition, transitivity of the conditional, conditional proof, proof by contradiction, de Morgan's laws, distributive laws, etc, and some inference rules for quantified predicate logic?

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.

[DiscourseFan]

I think all proofs are just "convincing arguments." Computation would make that seem meaningless, but computers don't operate based on truth, they are repetition machines, just like you and I. But I've been reading an Introductory Topology book recently (Munkres) and the entire first chapter is explicating at a relatively high level of detail all the things you describe and moreso. But its necessary, in some sense. A lot of the set theoretical rules were employed in topology to create more generalized forms of analysis. You have to learn them because otherwise its very difficult to understand the language that's being used. But as I've argued elsewhere, if we are aware that its all based on interpretation, then I think we need to be a bit anarchistic and let students have the freedom to break those rules without knowing it, if they might produce thereby fascinating proofs and arguments. If you give people a schematic for interpretation, they're just going to follow it, and they might have difficulty deviating from it at all. The spark of human creativity comes when people are forced to, as they say, re-derive certain theorems, and while doing so they might accidentally discover some new implication of the logic that was unseen before, and produce something entirely new.

[webnrrd2k]

Isn't (classical) geometry basically about proving properties from a few theorems? I.e., logic, proof, and deduction.

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.

[auggierose]

I like your analogy with riding a bike: If you want to ride a bike, what is more important, learning how to ACTUALLY DO IT, or to learn the physical and mechanical rules underlying it? Furthermore, technical knowledge will always be incomplete (and that applies also to logic in a very technical sense), while once you learnt how to ride a bike, your knowledge, in a way, is complete.

[cubefox]

A lot of things can be learned simply by practice, without any theory, but many things at least benefit from learning it in a more principled way. That's not feasible for riding bikes, since this relies on the the motor cortex, which doesn't understand and benefit from explicit knowledge about the physics of bike movement. Writing proofs is more intellectual, it benefits from principled understanding.

[auggierose]

Finding theorems and proofs is not intellectual at all, it is like riding a bike. You are probably not going to prove anything new and interesting by approaching it from an intellectual angle. You CAN turn it into an intellectual exercise, and at some point it is very beneficial to do so, for meta-mathematical insights. Just like it is beneficial to learn the physics and mechanics of cycling, if you want to construct bikes. It's also very helpful when you are wondering about the technical veracity of your theorems and proofs. It's not that helpful if you want to FIND those theorems and proofs in the first place. Starting out with a fixed rule system also has the danger of limiting your imagination about what's possible, given that no fixed rule system is ever going to be enough.

[cubefox]

Proving things with formal calculi still relies on something like creativity, which itself isn't captured by a precise algorithm, similar to informal proofs. The advantage of learning formal proof is, I claim, purely didactic, as it gives a clear idea on what a valid inference step is in the ideal case. I don't think there is really a danger of limiting your imagination, as you will probably stop thinking in formal terms as soon as you are good in doing informal proofs.

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

[auggierose]

Thanks for the link, looks like an interesting paper!

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.

[Tainnor]

> Proving things with formal calculi still relies on something like creativity, which itself isn't captured by a precise algorithm, similar to informal proofs.

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.

[cubefox]

Yeah. Though if one is loose with the word "algorithm" one can count an advanced machine learning model (a few years from now) as such an algorithm. It wouldn't be able to prove or disprove every given first-order statement, but perhaps the vast majority below a certain length. Maybe it could decide every conjecture we are interested in.