Also found in: Wikipedia.
The following article is from The Great Soviet Encyclopedia (1979). It might be outdated or ideologically biased.



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


The Great Soviet Encyclopedia, 3rd Edition (1970-1979). © 2010 The Gale Group, Inc. All rights reserved.
References in periodicals archive ?
However, Gentzen's cut-elimination metatheorem shows that cut 'is in principle dispensable in sequent calculus' (ibid.).
In Principia Mathematica, Russell proves a metatheorem to the effect that the scope of a single occurrence of a description in an extensional context does not matter, provided existence and uniqueness conditions are satisfied.
I present the metalogical results that show the property of satisfying Modus Ponens as a necessary and sufficient condition for the extended completeness of the system, and to the Deduction Metatheorem as a necessary and sufficient condition for the extended correctness of the system.
The inverse metalogical implication, known as the Deduction Metatheorem, is a very special property of an axiomatic system S.
Fine maintains that the foregoing argument proves what he calls 'Metatheorem 1':
Kohlenbach, "Some logical metatheorems with applications in functional analysis," Transactions of the American Mathematical Society, vol.
In [1], Kohlenbach defined hyperbolic space in his paper titled "Some Logical Metatheorems with Applications in Functional Analysis, Transactions of the American Mathematical Society, Vol.
These are neutrosophic metatheorems of the mathematical neutrosophic theory where they are employed.
Kohlenbach: Some logical metatheorems with applications in functional analysis, Trans.
As early as "Philosophy and the Form of Fiction," published in his first collection of essays, Fiction and the Figures of Life, Gass outlines the kind of writing he has consistently championed: There are metatheorems in mathematics and logic, ethics has its linguistic oversoul, everywhere lingos to converse about lingos are being contrived, and the case is no different in the novel.
The proofs of the various metatheorems (soundness and completeness) are found in separate sections, marked as optional.