An introduction to mathematical logic

What Hacker News says

1. magical_spellNov 2024
   Related: E.J. Lemmon, in his book Beginning Logic, lists some important logic books and says that Chapter 0 of Church's Introduction to Mathematical logic ``deserves to be read several times by /all/ philosophers''.
   thread
2. sunday_serifOct 2023
   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!

   Show morethread
3. TainnorMay 2022
   Are you familiar with a general treatment of first order logic, including the completeness theorem? If not, I suggest starting there, for which I'd recommend:

   - Chiswell & Hodges, "Mathematical Logic" - This is very clear and careful and gives lots of motivations for introduced concepts, but moves somewhat slowly (introducing FOL in three stages, first propositional, then quantifier-free and then full FOL)

   - Leary & Kristiansen, "A Friendly Introduction to Mathematical Logic" (available online for free) - this moves somewhat faster and skips "lower" logics such as propositional logic and uses a different proof system. If you read up to Löwenheim-Skolem, you already have a little bit of Model Theory (the rest of the book is more about computability and logic).

   If you've already done FOL, I would recommend:

   - Kirby, "An Invitation to Model Theory". This doesn't presuppose much more than FOL (and even recapitulates it briefly) and some basic familiarity with undergraduate math concepts (e.g. groups, fields, vector spaces) and explains everything very carefully. I also think it has great exercises.

   Show morethread
4. auggieroseOct 2021
   Very helpful answer, thank you! I suspected that it has something to do with "Tarski's definition of truth", but there seem to be different ideas around about what this means. While Wikipedia agrees with yours, I can point to at least one popular book ("An Introduction to Mathematical Logic" by Richard E. Hodel) that equates Tarski truth just with model theoretic truth.

   I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptable in a termination proof of the algorithm for it to be practical for my purposes.

   Show morethread