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 <[email protected]>: > > 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 [email protected] 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 [email protected] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/48543c4c-282a-4f69-b408-e8e7796de91an%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/48543c4c-282a-4f69-b408-e8e7796de91an%40googlegroups.com?utm_medium=email&utm_source=footer>. -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/84FD024B-ED9D-4952-BE13-924F3EE42258%40kenkubota.de.
