View source for 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635401.png" />. This may be a complicated theory, the [[Semantics|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635402.png" /> is non-contradictory or whether some mathematical principle (e.g. the [[Axiom of choice|axiom of choice]]) is compatible with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635403.png" />. In order to clarify this question one constructs at first a precise logico-mathematical language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635404.png" /> such that all statements in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635405.png" /> of interest can be described by formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635406.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635407.png" /> from the axioms and formulas already derived. Thus, a formal system (or, in other words, a formal axiomatic theory, a calculus) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635408.png" /> arises that exactly describes some fragment of the meaningful theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m0635409.png" /> of interest. It is essential here that in stating <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354010.png" /> one does not use an exhaustive penetration into the, possibly very complicated, semantics of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354011.png" />. The calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354012.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354013.png" />, and, secondly, of investigating <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354014.png" /> by means of some meaningful theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354015.png" />. In this case, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354016.png" /> is called the object theory, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354017.png" /> its meta-theory.

From the point of view of the foundations of mathematics it is important that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354018.png" /> is related to more reliable theories than <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354019.png" />, so that investigating <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354020.png" /> by means of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354021.png" /> can be regarded as a real clarification and justification of the unclear part of the semantics of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354022.png" /> using the more convincing theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354023.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354024.png" /> but only in the simple fact of derivability or non-derivability of certain formulas in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354025.png" />, it is natural to investigate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354026.png" /> by means of any previously established mathematical theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354027.png" /> that is convincing for the investigator, without imposing a priori restrictions.

One may further analogously investigate the meta-theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354028.png" />, by constructing a formal system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354029.png" /> and by studying <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354030.png" /> by means of some meta-meta-theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m063/m063540/m06354031.png" />. The investigations in [[Proof theory|proof theory]] are of this nature.

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1951)</TD></TR></table>



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  R. Sikorsky,   "The mathematics of metamathematics" , Polska Akad. Nauk  (1963)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  P. Suppes,   "Introduction to logic" , v. Nostrand  (1957)  pp. §9.8</TD></TR></table>