Metatheorem

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.

A formal system is determined by a formal language and a deductive system (axioms and rules of inference). The formal system can be used to prove particular sentences of the formal language with that system. Metatheorems, however, 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.

Examples

Examples of metatheorems include:

gollark: > Cherenkov radiation (/tʃəˈrɛŋkɒf/;[1] Russian: Черенков) is electromagnetic radiation emitted when a charged particle (such as an electron) passes through a dielectric medium at a speed greater than the phase velocity of light in that medium. A classic example of Cherenkov radiation is the characteristic blue glow of an underwater nuclear reactor. The phenomenon is named for Soviet physicist Pavel Cherenkov, who shared the 1958 Nobel Prize in Physics for its discovery. (praise wikipedia, etc)
gollark: ???
gollark: Neutrinos are not charged.
gollark: Ah, it's specifically CHARGED particles, I checked.
gollark: No, I mean is Cherenkov radiation not... caused by alpha/beta radiation, not neutrinos?

See also

References

  • Geoffrey Hunter (1969), Metalogic.
  • Alasdair Urquhart (2002), "Metatheory", A companion to philosophical logic, Dale Jacquette (ed.), p. 307
  • Meta-theorem at Encyclopaedia of Mathematics
  • Barile, Margherita. "Metatheorem". MathWorld.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.