Substitution in First-Order Formulas. Part II. The Construction of First-Order Formulas

Abstract

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 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.