Metatheorem

a theorem on objects—concepts, definitions, axioms, proofs, rules of inference, or theorems—of a particular scientific theory, called the object theory, that can be proved by means of the metatheory of this theory. The term “metatheorem” is primarily used in reference to theorems on objects of formalized theories (that is, in those cases in which the object theory is a calculus or formal system).

If a metatheorem belonging to a given logical-mathematical calculus is proved using what are called finitary methods, which do not employ the abstraction of actual infinity in any form, it falls into metamathematics. Examples of such metatheorems are the deduction theorem for the propositional calculus or the predicate calculus, GodePs incompleteness theorem for formal arithmetic and richer systems, Church’s theorem on the unsolv-ability of the decision problem in the predicate calculus, and Tarski’s theorem of the indefinability of the truth predicate for a broad class of calculi using the means available in the calculi themselves. But if neither finitary nor constructive limitations are imposed on the nature of the concepts treated in the meta-theorem and (or) on the methods of proving the metatheorem, then such a metatheorem belongs to what is called the set-theoretic predicate logic. Examples include Gödel’s completeness theorem for the predicate calculus and the Löwenheim-Skolem theorem on the interpretability of any consistent theory in the domain of natural numbers and, in general, any proposition in which one speaks of an “arbitrary interpretation,” “set of all interpretations,” “universal validity,” and so on (in particular, all the results on the categoricalness of different axiomatic systems—that is, the isomorphism of arbitrary interpretations of the axioms—that may satisfy certain additional conditions). Metatheorems also include any theorems regarding theorems of informal mathematical theories, for example, many “duality principles” for different branches of mathematics (projective geometry, many algebraic theories).