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