First-Order Logic

Abstract Now we turn to arguments that involve quantifier expressions ‘There is’ and ‘For all‐, as we promised at the beginning of Chapter 5. We study what these expressions mean in mathematics (Sections 7.1–7.2), we build a formal semantics that gives necessary and sufficient conditions for a first-order sentence to be true in a structure (Section 7.3), we find natural deduction rules for these sentences (Section 7.4) and we prove a completeness theorem for the proof calculus got by adding these rules to those of earlier chapters (Section 7.6). The logic that we reach by adding these expressions and rules is called first-order logic. Sometimes you will also hear it called predicate logic or elementary logic or classical logic. Do not confuse it with traditional logic, which is the logic that was studied up till the middle of the nineteenth century—see (7.8) below.