Gödel’s Completeness Theorem

Abstract

This articleis part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Gödel’s famous completeness theorem (K. Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalkuls”, Monatshefte für Mathematik und Physik 37 (1930), 349–360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article contains the proof of a simplified completeness theorem for a countable relational language without equality.