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 deductiontheoretic 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