Logic as a Tool

Chapter 4Deductive Reasoning in First-order Logic

Validity, logical consequence, and equivalence in first-order logic can be established by using deductive systems, like for propositional logic.

In this chapter I present and illustrate with examples extensions of the propositional deductive systems introduced in Chapter 2, obtained by adding additional axioms (for Axiomatic Systems) and inference rules (for Propositional Semantic Tableaux and Natural Deduction) for the quantifiers or additional procedures handling them (for Resolution), that are sound and complete for first-order logic.

That such sound and complete deductive systems for first-order logic exist is not a priori obvious at all. The first proof of completeness of (an axiomatic) deductive system for first-order logic was first obtained by Kurt Gödel¹ in his doctoral thesis in 1929, and is now known as Gödel's Completeness Theorem. In supplementary Section 4.6, generic proofs of soundness and completeness of the deductive systems are sketched for first-order logic introduced here.

Differently from the propositional case, however, none of these deductive systems can be guaranteed to always terminate their search for a derivation, even if such a derivation exists. This can happen, for instance, when the input formula is not valid but can only be falsified in an infinite counter-model.

This is not an accidental shortcoming of the deductive systems. In fact, one of the most profound and important results in mathematical ...