Metatheorem
Encyclopedia
In logic
, a metatheorem is a statement about a formal system
proven in a metalanguage
. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory
, and may reference concepts that are present in the metatheory
but not the object theory
.
is determined by a formal language and a deductive system
(axiom
s and rules of inference). The formal system can be used to prove particular sentences of the formal language with that system.
Metatheorems, on the other hand, are proved externally to the system in question, in its metatheory. Common metatheories used in logic are set theory
(especially in model theory
) and primitive recursive arithmetic
(especially in proof theory
). Rather than demonstrating particular sentences to be provable, metatheorems may show that each of a broad class of sentences can be proved, or show that certain sentences cannot be proved.
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, a metatheorem is a statement about a formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
proven in a metalanguage
Metalanguage
Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...
. Unlike theorems proved within a given formal system, a metatheorem is proved within a metatheory
Metatheory
A metatheory or meta-theory is a theory whose subject matter is some other theory. In other words it is a theory about a theory. Statements made in the metatheory about the theory are called metatheorems....
, and may reference concepts that are present in the metatheory
Metatheory
A metatheory or meta-theory is a theory whose subject matter is some other theory. In other words it is a theory about a theory. Statements made in the metatheory about the theory are called metatheorems....
but not the object theory
Object theory
Object theory is a theory in philosophy and mathematical logic concerning objects and the statements that can be made about objects.- An informal theory :...
.
Discussion
A formal systemFormal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
is determined by a formal language and a deductive system
Deductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
(axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s and rules of inference). The formal system can be used to prove particular sentences of the formal language with that system.
Metatheorems, on the other hand, are proved externally to the system in question, in its metatheory. Common metatheories used in logic are set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
(especially in model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
) and primitive recursive arithmetic
Primitive recursive arithmetic
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist...
(especially in proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
). Rather than demonstrating particular sentences to be provable, metatheorems may show that each of a broad class of sentences can be proved, or show that certain sentences cannot be proved.
Examples
Examples of metatheorems include:- The deduction theoremDeduction theoremIn mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional...
for first-order logic says that a sentence of the form φ→ψ is provable from a set of axioms A if and only if the sentence ψ is provable from the system whose axioms consist of φ and all the axioms of A. - Consistency proofConsistency proofIn logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
s of systems such as Peano arithmetic