diff options
Diffstat (limited to 'content/zettel/4c3.md')
| -rw-r--r-- | content/zettel/4c3.md | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/content/zettel/4c3.md b/content/zettel/4c3.md new file mode 100644 index 0000000..64a9b2c --- /dev/null +++ b/content/zettel/4c3.md @@ -0,0 +1,44 @@ ++++ +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]: <https://en.wikipedia.org/wiki/Hilbert%27s_program> |