# Accessible formal specification and explanation of First Order Logic?

I am trying to get good at proofs by working through How To Prove It. Unfortunately I am very bothered by the fact that I do not understand all the formalities in First Order Logic + set theory (FOL+ST) and this makes it difficult to motivate myself to practice. Is there a good resource for learning the formalities of FOL+ST? I want a good grasp of things such as

• what notions are taken as basic and how the formal terms and rules are built from those
• when you're allowed to do different inference steps
• how some common basic mathematical steps are accomplished (say applying a theorem or definition, converting between quantifiers, converting between equivalent terms), even if they take place outside the theory

I don't mind having the formalities explained (partially) in terms of FOL+ST since I am already familiar with how it works (just not especially good at it and not yet comfortable with it).

I found the explanations of various Type Theory formal systems in Benjamin Pierce's Types and Programming Languages and Robert Harper's Practical Foundations for Programming Languages satisfying, so something along those lines would work well.

-
I personally find formal logic quite useless as a tool for proving theorems, unless you're working in this very area. –  Yuval Filmus Jun 21 '11 at 5:15
I think I have not explained myself clearly. It is not that I think formal logic will be especially helpful for proving theorems. Most true theorems are proved without it, so clearly it's not necessary and probably not helpful. My problem is that I am mentally uncomfortable working in the system when I don't understand in a more rigorous way. My brain constantly throws up objections like 'how do you know you can transform a this term into that term that way?' and 'how does the process of proving an implication actually work?'. This is unpleasant and makes work more difficult than it should be. –  John Salvatier Jun 21 '11 at 16:28

As a logician, I agree it is not necessary to know formal logic or axiomatic set theory to study most areas of math. In fact, few mathematicians are deeply familiar with those areas.

So if you are interested in learning about logic and set theory in order to do mathematics, I think you may find it more helpful to look at an introductory non-axiomatic set theory book such as Naive set theory by Halmos. That sort of book describes the basic set-theoretic techniques that are used in all areas of math, and by reading it you will also learn many of the reasoning techniques about sets that are useful in other areas.

Books on formal logic generally focus on logic itself, rather than spending a lot of time discussing how it applies to other areas of math. Also, many logic books assume you are already familiar with both natural-language mathematical proof and basic set theory before you start to learn formal logic. This is because mathematical logic books take the viewpoint that they are studying logic with the usual tools of mathematics, which include set theory and mathematical reasoning.

If you do want to learn the actual rules of logic, I highly recommend Enderton's book A mathematical introduction to logic. There are many "introductory" logic books, but that one is particularly focused on the material you mention, uses modern terminology, and is very well written. On the other hand, if you are just getting used to proofs, it will take some effort to work through any rigorous textbook on logic or any other area of mathematics.

-
I second Carl's recommendation of Enderton's remarkable book. It's rigorous, respectable, and not a word is wasted. –  ShyPerson Jun 21 '11 at 20:53