+++ title = "Hilbert Program" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["4c2"] forwardlinks = [] zettelid = "4c3" +++ Hilbert was under the impression that mathematics should be completely formalised in a minimal mathematical model (elementary methods), instead of the standard abstract methods that are used (axiom of choice). All proofs should be translated to this formalised mathematical representation, which differs from the social proofs that are normally made. This is the start of the proof-theory field of research. Hilbert considers these real formulas to be numerical equations, which can also be defined as $\Pi_1^0$-formulas (formulas that only have numbers in them and are preceded by a set amount of $\forall$). The idea is then that any elementary formula can be proven by an elementary proof, and that elementary mathematics is therefore complete. The idea is therefore that the Hilbert program states that any mathematical property could be expressed in elementary mathematics, and that it is therefore true iff there is an elementary proof of it. The program also defines the following concepts that must hold[^1]: Completeness : Proof that all true elementary mathematical statements are provable. Consistency : No contradiction can be obtained in elementary mathematics. Conservation : A proof that was obtained for real objects using ideal objects (such as uncountable sets), can be proven without the use of ideal objects. Decidability : That there exists an algorithm that can determine the truth or falseness of any elementary statement. [^1]: