# Metamathematics

Metamathematics is the mathematical consideration of the fundamentals of mathematics .

In 1920 the mathematician David Hilbert put forward the demand that mathematics be placed on the basis of a complete and consistent system of axioms . This endeavor became known as the Hilbert program . For the analysis of the fundamentals of mathematics with mathematical methods, he coined the term metamathematics (based on metaphysics ).

The Hilbert program seemed to fail since Gödel's incompleteness theorem showed that there is no system of axioms that meets all of Hilbert's requirements. In particular, it is not possible to develop a formal system in which all true statements can also be proven.

After proof of consistency for parts of arithmetic by Leopold Löwenheim , Albert Thoralf Skolem , Jacques Herbrand and Mojżesz Presburger , Gerhard Gentzen succeeded in proof of consistency for Peano arithmetic of the first stage, using what is known as transfinite induction . However, what all these proofs have in common is that they - according to Gödel's incompleteness theorem - could not be carried out within the arithmetic itself.

There were important results about decidability from Alonzo Church , who was able to show the undecidability of the quantifier logic at all levels. The concept of recursivity is equivalent to that of predictability .

In 1951 Paul Lorenzen carried out a proof of freedom from contradictions for the branched type theory. This proof provides the consistency of parts of classical analysis. In his book Metamathematik , published in 1962, he understands metamathematics as "mathematics of metatheories", whereby a metatheory is a (constructive or axiomatic) theory about axiomatic theories.

By using the rule (infinite induction) one obtains a complete semi-formalism (K. Schütte) of arithmetic and thus a consistency proof of constructive mathematics through inclusion in Gentzen's main theorem . ${\ displaystyle \ omega}$