First-Order Logic: Completeness, Compactness, Skolem-Lo¨wenheim Theorem

This chapter proves one of the major results in first-order logic-the completeness theorem for first-order tableaux, which is that every valid formula of first-order logic is provable by the tableau method. Lowenheim proved the remarkable result that if a formula is satisfiable at all, then it is satisfiable in a denumerable domain. Later, Skolem proved the even more celebrated and important result that, for any denumerable set S of formulas, if S is satisfiable at all (if there is, in some domain, an interpretation under which all elements of S are true) then S is satisfiable in a denumerable domain. This result, the Skolem-Lowenheim Theorem, is of fundamental importance for the entire foundation of mathematics. Any axiom system that is intended to apply to a non-denumerable domain can be re-interpreted to apply to a denumerable domain; it cannot force the domain of interpretation to be non-denumerable.