The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 (and a rewritten version of the dissertation, published as an article in 1930) is not easy to read today; it uses concepts and formalism that are outdated and terminology that is often obscure. The version given below attempts to faithfully represent all the steps in the proof and all the important ideas, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.
Definitions and assumptions
We work with first-order predicate calculus. Our languages allow constant, function and relation symbols. Structures consist of (non-empty) domains and interpretations of the relevant symbols as constant members, functions or relations over that domain.
We fix some axiomatization of the predicate calculus: logical axioms and rules of inference. Any of the several well-known axiomatisations will do; we assume without proof all the basic well-known results about our formalism (such as the normal form theorem or the soundness theorem) that we need.
We axiomatize predicate calculus without equality, i.e. there are no special axioms expressing the properties of equality as a special relation symbol. After the basic form of the theorem is proved, it will be easy to extend it to the case of predicate calculus with equality.
Full article ▸