Re: [Metamath] Writing a pdf that organizes the introductory logic portion of set.mm.

[Johnathan Mercer]

That Figure is a gem - thanks for sharing! {typed with my thumbs} On Jul 17, 2023, at 11:31 AM, Ken Kubota <m...@kenkubota.de> wrote:  My recommendation is Peter B. Andrews’ textbook from 2002, as mentioned here: https://owlofminerva.net/files/fom_2018.pdf#page=2 In terms of expressing mathematics naturally I haven’t seen anything better, although it is still simple type theory (without type variables). Kind regards, Ken Kubota ____________________________________________________ Ken Kubota https://doi.org/10.4444/100 Am 17.07.2023 um 03:04 schrieb Marshall Stoner <mbstone...@gmail.com>: To Jim. I feel like a big problem with metamath is that it just isn't satisfying without some foundational understanding of mathematical logic.  Sure, you can follow proofs and see that each step is justified by digging down 100 layers, but it's not pretty.  For motivation on how to construct proofs from scratch and feel confident, you really need to understand classical logic from a higher perspective.  Sure, there are tools that fill in the gaps for you, but I'm the kind of person that really needs to understand all the nuts and bolts to feel good about something.  It's also hard to convince myself that I understand a topic if I am not able to explain it to others.  Writing a pdf is the way I'm learning. I think I might need to invest in a better text.  I've been trying to read Introduction to Mathematical Logic by Mandelson (because I found it for free), but can't stand the layout.  The author does nothing to make important definitions stand out and the proofs are all jammed into a single paragraph and not always worded well either.  I do have a good text on ZFC set theory ("Axiomatic Set Theory" by Suppes) and have taken a class on that a long time ago.  It just isn't super formal and doesn't cover logic or proof theory at all.  I'd like to find a better introduction to logic but I'd hate to buy a clone of Mendelson.  It's tough to tell how good a text is based on reviews. On Tuesday, July 4, 2023 at 7:08:50 PM UTC-4 kin...@panix.com wrote: On 7/4/23 15:07, Marshall Stoner wrote: > What I'm writing is not directly connected with meta-math, but > something that I feel could help explain it better for novices I'd advise you to follow where the inspiration leads you. If you end up with something which has a lot of metamath notation and reference to metamath theorems by name, that's great, and may indeed be helpful to put on the web site in one form or another if you want to contribute it in that fashion. If what you want to do (in terms of how it makes sense to present the material or whatever) ends up diverging more from metamath in detail and ends up being more of a general logic textbook, that's cool too. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/48543c4c-282a-4f69-b408-e8e7796de91an%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/84FD024B-ED9D-4952-BE13-924F3EE42258%40kenkubota.de. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/A84EED97-36B5-4BDD-8CEC-8B93F84515C4%40gmail.com.