blob: 64a9b2c39474904c7fae5f4e48800baeb63b2e0a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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>
|
