4 ms·

I am currently trying to learn formal logic and proof systems. I’ve always been interested in learning higher level math, but was consistently mystified by the

I am currently trying to learn formal logic and proof systems. 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.

haltist 3y ago
Type Theory and Formal Proof is one of the better books I've found. It starts with untyped lambda calculus and works up to a dependently typed proof calculus in gradual steps. So if you are looking for a book then that's one of the better introductions and has a bunch of good exercises.[1] 1: https://www.cambridge.org/core/books/type-theory-and-formal-proof/0472640AAD34E045C7F140B46A57A67C# https://www.cambridge.org/core/books/type-theory-and-formal-...
- sunday_serif 3y ago
  Thank you for the recommendation! I will add that to my list. So far, the following 3 books have been very useful to me (in the following order). 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!

haltist 3y ago

Type Theory and Formal Proof is one of the better books I've found. It starts with untyped lambda calculus and works up to a dependently typed proof calculus in gradual steps. So if you are looking for a book then that's one of the better introductions and has a bunch of good exercises.[1] 1: https://www.cambridge.org/core/books/type-theory-and-formal-proof/0472640AAD34E045C7F140B46A57A67C# https://www.cambridge.org/core/books/type-theory-and-formal-...

sunday_serif 3y ago
Thank you for the recommendation! I will add that to my list. So far, the following 3 books have been very useful to me (in the following order). 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!