@MISC{HENMODEL.MIZ,
  AUTHOR = {Braselmann, Patrick and Koepke, Peter},
  TITLE = {Equivalences of Inconsistency 
and {H}enkin Models},
  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 and Equivalences of Inconsistency},
  SECTION2 = {Unions of Consistent Sets},
  SECTION3 = {Construction of a Henkin Model},
  SECTION4 = {Some Properties of the Henkin Model},
  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 establishes some
              equivalences of inconsistency. It is proved that a
              countable union of consistent sets is
              consistent. Then the concept of a Henkin model is
              introduced. The contents of this article correspond
              to Chapter IV, par. 7 and Chapter V, par. 1 of Ebbinghaus,
              Flum, Thomas.}}

