Buch | Kapitel
Proof theory and Martin-Löf type theory
pp. 257-279
Abstrakt
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).
Publication details
Published in:
Boldini Pascal, Bourdeau Michel, Heinzmann Gerhard (2008) One hundred years of intuitionism (1907–2007): the Cerisy conference. Dordrecht, Springer.
Seiten: 257-279
DOI: 10.1007/978-3-7643-8653-5_16
Referenz:
Setzer Anton (2008) „Proof theory and Martin-Löf type theory“, In: P. Boldini, M. Bourdeau & G. Heinzmann (eds.), One hundred years of intuitionism (1907–2007), Dordrecht, Springer, 257–279.