Meta-theory

The totality of mathematical methods and means intended for the description and definition of some formal axiomatic theory, as well as for the investigation of its means. A meta-theory is an important component of the formalization method, which is one of the most central methods in mathematical logic.

The essence of this method may briefly be described as follows. Suppose that one is interested in some meaningful mathematical theory $ T _ {1} $. This may be a complicated theory, the semantics of which is intuitively not sufficiently clear (e.g. it may be set theory, mathematical analysis, second-order arithmetic, etc.). One is interested in whether $ T _ {1} $ is non-contradictory or whether some mathematical principle (e.g. the axiom of choice) is compatible with $ T _ {1} $. In order to clarify this question one constructs at first a precise logico-mathematical language $ \Omega $ such that all statements in $ T _ {1} $ of interest can be described by formulas in $ \Omega $. Then the logical principles that are used in the theory to derive new facts are formalized as axioms and derivation rules; these are used to derive new formulas in the language $ \Omega $ from the axioms and formulas already derived. Thus, a formal system (or, in other words, a formal axiomatic theory, a calculus) $ \widetilde{T} _ {1} $ arises that exactly describes some fragment of the meaningful theory $ T _ {1} $ of interest. It is essential here that in stating $ \widetilde{T} _ {1} $ one does not use an exhaustive penetration into the, possibly very complicated, semantics of $ \widetilde{T} _ {1} $. The calculus $ \widetilde{T} _ {1} $ is constructed by simple laws as a purely symbolic system and for understanding its operation one need not penetrate into the sense of the formulas that are derived in it.

Such an approach opens, first, the possibility of mathematically formulating the problems of interest, related to the derivability of certain formulas in $ \widetilde{T} _ {1} $, and, secondly, of investigating $ \widetilde{T} _ {1} $ by means of some meaningful theory $ T _ {2} $. In this case, $ \widetilde{T} _ {1} $ is called the object theory, and $ T _ {2} $ its meta-theory.

From the point of view of the foundations of mathematics it is important that $ T _ {2} $ is related to more reliable theories than $ T _ {1} $, so that investigating $ \widetilde{T} _ {1} $ by means of $ T _ {2} $ can be regarded as a real clarification and justification of the unclear part of the semantics of $ T _ {1} $ using the more convincing theory $ T _ {2} $. In this connection special preference has been given to sufficiently reliable meta-theories reflecting finite parts of mathematics, as well as to theorems constructed within the frame of intuitionism or constructive mathematics. Moreover, outside the foundations of mathematics this restriction is superfluous. If one is interested not in the question of intuitive clarity of $ T _ {1} $ but only in the simple fact of derivability or non-derivability of certain formulas in $ \widetilde{T} _ {1} $, it is natural to investigate $ \widetilde{T} _ {1} $ by means of any previously established mathematical theory $ T _ {2} $ that is convincing for the investigator, without imposing a priori restrictions.

One may further analogously investigate the meta-theory $ T _ {2} $, by constructing a formal system $ \widetilde{T} _ {2} $ and by studying $ \widetilde{T} _ {2} $ by means of some meta-meta-theory $ T _ {3} $. The investigations in proof theory are of this nature.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)

References

[a1]	R. Sikorsky, "The mathematics of metamathematics" , Polska Akad. Nauk (1963)
[a2]	P. Suppes, "Introduction to logic" , v. Nostrand (1957) pp. §9.8