2
$\begingroup$

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.

  • 3
    I personally find formal logic quite useless as a tool for proving theorems, unless you're working in this very area.2011-06-21
  • 0
    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.2011-06-21

2 Answers 2