Metamathematics, sometimes called metalogic, is the branch of logic concerning the combination and application of mathematical symbols. The primary goal of metamathematics is to determine the nature of mathematical reasoning. It consists of basic principles, mainly concerned with proofs of consistency that attempt to formulate mathematical theories. Metamathematics today is mainly used as a mechanism of proving mathematical theories in an automated way.

Metamathematics arose during the attempts in the late 1800s to mechanize the verification of mathematical proofs. At that time precise mathematical logic coexisted on equal terms with vague intuitions and it was becoming apparent that a better, more firm basis for mathematics be developed. From the late 19th century studies in formal logic attempted to develop a complete, consistent formulation of mathematics such that proposals could be formally stated and proved or disproved using a limited number of symbols that had well defined meanings. Theorems...