I’ve always been interested in learning higher level math, but was consistently mystified by the proofs. I could always come around to understand them, but I never understood how the authors knew that proof method was “allowed”.
Learning about the formal proof systems has been a very interesting diversion for me. It has helped me begin to understand the foundations of the math subjects I am interested in and definitely has upped my confidence reading intricate proofs.
But perhaps the best outcome of this learning has been that I now have a much stronger framework for sound reasoning. It is easier for me to express and argument clearly or pin down a shortcomings in other arguments.
It is unclear to me how applicable these learnings will be for my primary interest in software development, but it has been a very enlightening process nevertheless.
1: https://www.cambridge.org/core/books/type-theory-and-formal-...
1. Propositions and Predicate Calculus by Derek Goldrei: The first 3 chapters in this book helped me learn propositional logic and helped me learn the basic ideas about the relationship between models and logical statements (syntax vs. semantics). For some reason, this book's transition from propositional logic to first order logic left me in a daze, so I started up on the book below.
2. A friendly Introduction to Mathematical Logic by Christopher C Leary and Lars Kristiansen: The first 2 chapters of this book were a great way to see a fully fledged axiomatic first order proof system in action. They do a great job of setting up a complete proof system with all the gory detail. But this book only focuses on axiomatic proof systems before moving on to results about compactness and incompleteness. While the precision of this book is one of its best strengths, I found myself getting lost in the specifics of the particular axiomatic proof system they create. Felt like I was missing the forest for the trees a bit... and I wanted to learn more about other proof systems as well. This lead me to the book below.
3. Intermediate Logic By David Bostock: This book is a bit less rigorous than the previous two. It is more focused on philosophers than on mathematicians. For me though, this was a welcome change. Chapters 4 - 7 of this book are very useful because they develop 4 different proof systems. Semantic tableau (ch. 4), Axiomatic (ch. 5), Natural Deduction (ch. 6) and Sequent Calculus (ch. 7). This is the book that really helped the idea of formal proof "click". I don't think it would have been as effective had I not worked on the more rigorous previously mentioned books first though.
What excites me most about the book you mention is the connection to lambda calculus. That has been completely absent from the books I have read so far. Also excited to dive into it after seeing an article from quanta yesterday on HN about the Curry-Howard isomorphism connecting lambda calculus and types to proof systems.
Thanks!
On related note, studying a lot of maths, mainly in service of my interest in AI. I only took up through Calc I "back in the day" and that was like 30 years ago anyway. So trying to bone up on a lot of Calculus, Linear Algebra, Probability, etc.
And finally... I've signed up for a class that is one of the "earned entry" classes for an online Master's Degree program (@treprinum here on HN clued me in to that[1], so thanks for that!) and some of the programming assignments require Kotlin, so I'm literally sitting in the cafe at Barnes & Noble right now with my Kotlin book, working on getting up to speed on that.
For anyone else that tries this I recommend starting small and then gradually working your way up. I got a bad injury early on from doing too many miles too early. If you don't consistently do cardiovascular exercise then walking a mile or two every few days is a good way to develop the habit.
