n. the motivating problem of metamathematics, proposed by Hilbert in 1920 in support of his formalism in the foundations of mathematics, of formalizing all of mathematics and showing by purely syntactic means that finitary methods could never lead to contradiction. This is equivalent to finding a decision algorithm for all of mathematics, and although it was shown unattainable by Gödel's proof in 1931, the project nonetheless led to the development of proof theory and computability theory. See also turing machine.