@MISC{SUBSTUT2.MIZ,
  AUTHOR = {Braselmann, Patrick and Koepke, Peter},
  TITLE = {Substitution in First-Order Formulas. 
{P}art {II}. 
{T}he Construction of First-Order Formulas},
  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 = {Further Properties of Substitution},
  SECTION2 = {Facts about Substitution and Quantifiers of a Formula},
  SECTION3 = {Results about the Construction of Formulas},
  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 that every
              substitution can be applied to every formula as in
              Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus,
              Flum, Thomas. After that, it is observed that
              substitution doesn't change the number of
              quantifiers of a formula. Then further details about
              substitution and some results about the construction
              of formulas are proven.}}

