Original proof of Gödel's completeness theorem

related topics
{math, number, function}
{government, party, election}

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 ▸

related documents
Μ-recursive function
Pythagorean triple
Riemann integral
Grothendieck topology
Binomial coefficient
Discrete cosine transform
Travelling salesman problem
Lie group
Group theory
P-adic number
Class (computer science)
Lambda calculus
Dedekind domain
Orthogonal matrix
Hilbert's tenth problem
Lebesgue integration
Formal power series
Banach–Tarski paradox
Algebraic geometry
Red-black tree
Fast Fourier transform
Closure (computer science)
Continued fraction
Singleton pattern
Axiom of choice
Tensor product
Adjoint functors