Proof theory and Martin-Löf type theory
pp. 257-279
in: Pascal Boldini, Michel Bourdeau, Gerhard Heinzmann (eds), One hundred years of intuitionism (1907–2007), Berlin, Springer, 2008Abstract
It is the goal of ordinal theoretic proof theory to reduce the consistency of theories for formalising mathematical proofs to the well-foundedness of ordinal notation systems. In order to obtain a satisfactory solution to the consistency problem, this reduction needs to be supplemented by a second step, namely by proofs of the well-foundedness of the ordinal notation systems in "safe' theories, for which one has an argument that everything shown in these theories is valid. Because of Gödel's incompleteness theorem, a mathematical correctness proof can prove only relative correctness, but never provide an absolute proof of correctness. In order to obtain an argument which provides absolute trust, the only possibility is to have a philosophical correctness argument. Although there are other theories that could serve as such safe theories, the theories for which such arguments have best been worked out at present are extensions of Martin-Löf type theory (MLTT).
