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.