Explorations

Future Paths of Phenomenology

1st OPHEN Summer Meeting

Repository | Book | Chapter

176469

Proof theory and Martin-Löf type theory

Anton Setzer

pp. 257-279

Abstract

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.

Pages: 257-279

DOI: 10.1007/978-3-7643-8653-5_16

Full citation:

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.