5   More about first order logic

As in the case of propositional logic, we need to explore the system of first order (quantified) logic semantically as well as syntactically. In this chapter we first define the concept of an interpretation of the first order language, and then consider how to use semantic tableaux to reason about formulae and sequents in terms of their satisfying interpretations. We also look at the sequent calculus, which is an approach intended to unify the deduction-theoretic and the semantic accounts of logic. Finally, we tidy up some loose ends by extending the calculus a little to accommodate restricted (binary) quantifiers along with the unrestricted ones used so far.

---

• Modelling quantifiers Formal definition of interpretations for first order logic
• Quantifiers in semantic tableaux Rules for analysing ALLx A and SOMEx A
• Sequent calculus Another take on deduction and on semantic reasoning
• Restricted quantifiers revisited The rules ALLI_R, ALLE_R, SOMEI_R and SOMEE_R
• Examples Proofs with restricted quantifiers
• First order tableau exercises Sample problems with solutions
• Restricted quantifier exercises Sample natural deduction problems with solutions