Metamathematics
Encyclopedia
Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories
, which are mathematical theories about other mathematical theories. Metamathematical metatheorem
s about mathematics itself were originally differentiated from ordinary mathematical theorems in the 19th century, to focus on what was then called the foundational crisis of mathematics. Richard's paradox
(Richard 1905) concerning certain 'definitions' of real numbers in the English language is an example of the sort of contradictions which can easily occur if one fails to distinguish between mathematics and metamathematics. Something similar can be said around the well-known Russell's paradox
(Does the set of all those sets that do not contain themselves contain itself?).
The term "metamathematics" is sometimes used as a synonym for certain elementary parts of formal logic
, including propositional logic and predicate logic
.
, so that the early histories of the two fields, during the late 19th and early 20th centuries, largely overlap. More recently, mathematical logic has often included the study of new pure mathematics, such as set theory
, recursion theory
and pure model theory
, which is not directly related to metamathematics.
Serious metamathematical reflection began with the work of Gottlob Frege
, especially his Begriffsschrift
.
David Hilbert
was the first to invoke the term "metamathematics" with regularity (see Hilbert's program
). In his hands, it meant something akin to contemporary proof theory
, in which finitary methods are used to study various axiomatized mathematical theorems.
Other prominent figures in the field include Bertrand Russell
, Thoralf Skolem
, Emil Post, Alonzo Church
, Stephen Kleene, Willard Quine, Paul Benacerraf
, Hilary Putnam
, Gregory Chaitin
, Alfred Tarski
and Kurt Gödel
. In particular, arguably the greatest achievement of metamathematics and the philosophy of mathematics
to date is Gödel's incompleteness theorem
: proof that given any finite number of axioms for Peano arithmetic, there will be true statements about that arithmetic that cannot be proved from those axioms.
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....
, which are mathematical theories about other mathematical theories. Metamathematical metatheorem
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.- Discussion :A formal...
s about mathematics itself were originally differentiated from ordinary mathematical theorems in the 19th century, to focus on what was then called the foundational crisis of mathematics. Richard's paradox
Richard's paradox
In logic, Richard's paradox is a semantical antinomy in set theory and natural language first described by the French mathematician Jules Richard in 1905. Today, the paradox is ordinarily used in order to motivate the importance of carefully distinguishing between mathematics and metamathematics...
(Richard 1905) concerning certain 'definitions' of real numbers in the English language is an example of the sort of contradictions which can easily occur if one fails to distinguish between mathematics and metamathematics. Something similar can be said around the well-known Russell's paradox
Russell's paradox
In the foundations of mathematics, Russell's paradox , discovered by Bertrand Russell in 1901, showed that the naive set theory created by Georg Cantor leads to a contradiction...
(Does the set of all those sets that do not contain themselves contain itself?).
The term "metamathematics" is sometimes used as a synonym for certain elementary parts of formal logic
Formal logic
Classical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
, including propositional logic and predicate logic
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
.
History
Metamathematics was intimately connected to mathematical logicMathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, so that the early histories of the two fields, during the late 19th and early 20th centuries, largely overlap. More recently, mathematical logic has often included the study of new pure mathematics, such as 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...
, recursion theory
Recursion theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...
and pure model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
, which is not directly related to metamathematics.
Serious metamathematical reflection began with the work of Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
, especially his Begriffsschrift
Begriffsschrift
Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book...
.
David Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
was the first to invoke the term "metamathematics" with regularity (see Hilbert's program
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...
). In his hands, it meant something akin to contemporary 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...
, in which finitary methods are used to study various axiomatized mathematical theorems.
Other prominent figures in the field include Bertrand Russell
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
, Thoralf Skolem
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
, Emil Post, Alonzo Church
Alonzo Church
Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...
, Stephen Kleene, Willard Quine, Paul Benacerraf
Paul Benacerraf
Paul Joseph Salomon Benacerraf is an American philosopher working in the field of the philosophy of mathematics who has been teaching at Princeton University since he joined the faculty in 1960. He was appointed Stuart Professor of Philosophy in 1974, and recently retired as the James S....
, Hilary Putnam
Hilary Putnam
Hilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
, Gregory Chaitin
Gregory Chaitin
Gregory John Chaitin is an Argentine-American mathematician and computer scientist.-Mathematics and computer science:Beginning in 2009 Chaitin has worked on metabiology, a field parallel to biology dealing with the random evolution of artificial software instead of natural software .Beginning in...
, Alfred Tarski
Alfred Tarski
Alfred Tarski was a Polish logician and mathematician. Educated at the University of Warsaw and a member of the Lwow-Warsaw School of Logic and the Warsaw School of Mathematics and philosophy, he emigrated to the USA in 1939, and taught and carried out research in mathematics at the University of...
and Kurt Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
. In particular, arguably the greatest achievement of metamathematics and the philosophy of mathematics
Philosophy of mathematics
The philosophy of mathematics is the branch of philosophy that studies the philosophical assumptions, foundations, and implications of mathematics. The aim of the philosophy of mathematics is to provide an account of the nature and methodology of mathematics and to understand the place of...
to date is Gödel's incompleteness theorem
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic. The theorems, proven by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of...
: proof that given any finite number of axioms for Peano arithmetic, there will be true statements about that arithmetic that cannot be proved from those axioms.
Milestones
- Principia MathematicaPrincipia MathematicaThe Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...
(Whitehead and Russell 1925) - Gödel's completeness theoremGödel's completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
, 1930 - Gödel's incompleteness theorem, 1931
- Tarski's definition of model-theoretic satisfaction, now called the T-schemaT-schemaThe T-schema or truth schema is used to give an inductive definition of truth which lies at the heart of any realisation of Alfred Tarski's semantic theory of truth...
- The proof of the impossibility of the EntscheidungsproblemEntscheidungsproblemIn mathematics, the is a challenge posed by David Hilbert in 1928. The asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True" or "False" according to whether the statement is true or false...
, obtained independently in 1936–1937 by Church and Turing.