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 . 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
is non-contradictory or whether some mathematical principle (e.g. the axiom of choice) is compatible with
. In order to clarify this question one constructs at first a precise logico-mathematical language
such that all statements in
of interest can be described by formulas in
. 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
from the axioms and formulas already derived. Thus, a formal system (or, in other words, a formal axiomatic theory, a calculus)
arises that exactly describes some fragment of the meaningful theory
of interest. It is essential here that in stating
one does not use an exhaustive penetration into the, possibly very complicated, semantics of
. The calculus
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 , and, secondly, of investigating
by means of some meaningful theory
. In this case,
is called the object theory, and
its meta-theory.
From the point of view of the foundations of mathematics it is important that is related to more reliable theories than
, so that investigating
by means of
can be regarded as a real clarification and justification of the unclear part of the semantics of
using the more convincing theory
. 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
but only in the simple fact of derivability or non-derivability of certain formulas in
, it is natural to investigate
by means of any previously established mathematical theory
that is convincing for the investigator, without imposing a priori restrictions.
One may further analogously investigate the meta-theory , by constructing a formal system
and by studying
by means of some meta-meta-theory
. The investigations in proof theory are of this nature.
References
[1] | S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951) |
Comments
References
[a1] | R. Sikorsky, "The mathematics of metamathematics" , Polska Akad. Nauk (1963) |
[a2] | P. Suppes, "Introduction to logic" , v. Nostrand (1957) pp. §9.8 |
Meta-theory. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Meta-theory&oldid=47824