Metatheorem


Also found in: Wikipedia.

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

IU. A. GASTEV

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.
Observe that the Deduction Metatheorem states that a conditional is derivable from a set of formulas, if its consequent is derivable from the set of formulas augmented with the antecedent.
Let us call this special case of Metatheorem 1 by the name of Metalemma 1.
No doubt these are the kinds of practices that Fine had in mind when he referred to 'realist-laden' phenomena in his statement of Metatheorem 1.
We have seen this argument already - it is a special application of his 'proof' of Metatheorem 1, according to which there is a better instrumentalist account corresponding to every realist account.
These are neutrosophic metatheorems of the mathematical neutrosophic theory where they are employed.
Kohlenbach: Some logical metatheorems with applications in functional analysis, Trans.
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.