A Sequent Calculus for First-Order Logic 1
Patrick Braselmann, Peter Koepke · 2005
Summary. This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Godel's famous completeness theorem (K. Godel, Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls, Monatshefte fur 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 introduces a sequent calculus for first-order logic. The correctness of this calculus is shown and some important inferences are derived. The contents of this article correspond to Chapter IV of Ebbinghaus, Flum, Thomas.