@MISC{CALCUL_1.MIZ,
  AUTHOR = {Braselmann, Patrick and Koepke, Peter},
  TITLE = {A Sequent Calculus for First-Order Logic},
  NOTE = {This research was carried out within the project
              ``Wissensformate'' and was
              financially supported by the Mathematical Institute
              of the University of Bonn  (http://www.\-wissensformate.uni-bonn.de). 
	      Preparation of the Mizar
              code was part of the first author's graduate work
              under the supervision of the second author.
The authors thank Jip Veldman for his work on the final version 
of this article.},
  SECTION1 = {Preliminaries},
  SECTION2 = {A Sequent Calculus},
  SECTION3 = {Derived Rules},
  DAY = {25},
  MONTH = {September},
  YEAR = {2004},
  ADDRESS1 = {University of Bonn},
  ADDRESS2 = {University of Bonn},
  SUMMARY = {This article is part of a series of Mizar articles
              which constitute a formal proof (of a basic version)
              of Kurt G{\"o}del's famous completeness theorem
              (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der
              Axiome des logischen Funktionenkalk{\"u}ls'',
              Monatshefte f\"ur 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.}}

