You are welcome. Page references for [Andrews, 2002] are available here: https://www.owlofminerva.net/files/formulae.pdf#page=825
____________________________________________________ Ken Kubota https://doi.org/10.4444/100 > Am 17.07.2023 um 18:06 schrieb Johnathan Mercer <[email protected]>: > > That Figure is a gem - thanks for sharing! > > {typed with my thumbs} > >> On Jul 17, 2023, at 11:31 AM, Ken Kubota <[email protected]> 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 <[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] >> <mailto:[email protected]>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/84FD024B-ED9D-4952-BE13-924F3EE42258%40kenkubota.de >> >> <https://groups.google.com/d/msgid/metamath/84FD024B-ED9D-4952-BE13-924F3EE42258%40kenkubota.de?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] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/A84EED97-36B5-4BDD-8CEC-8B93F84515C4%40gmail.com > > <https://groups.google.com/d/msgid/metamath/A84EED97-36B5-4BDD-8CEC-8B93F84515C4%40gmail.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/C3E328AD-9CFA-4549-9B6F-3FE7B7C5A630%40kenkubota.de.
