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, and consider what is involved in showing that the sequents which are derivable using natural deduction are exactly the ones which are valid according to the semantic story. 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
• Soundness and Completeness Showing that deducibility and validity coincide
• Extra (math) Propositional logic is complete for its semantics
• Sequent calculus Another take on deduction and on semantic reasoning
• Extra (math) Cut is admissible in the sequent calculus
• 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