Computational interpretations of Markov’s principle

Por • 3 abr, 2020 • Sección: Educacion

Matteo Manighetti

Abstract In this thesis we are concerned with Markov’s principle, a statement that originated in the Russian school of Constructive Mathematics and stated originally that “if it is impossible that an algorithm does not terminate, then it will terminate”. This principle has been adapted to many dierent contexts, and in particular we are interested in its most common version for arithmetic, which can be stated as “given a total recursive function f, if it is impossible that a there is no n for which f(n) = 0, then there exists an n such that f(n) = 0”. This is in general not accepted in constructivism, where stating an existential statement requires one to be able to show at request a witness for the statement: here there is no clear way to choose such an n. We introduce more in detail the context of constructive mathematics from dierent points of view, and we show how they are related to Markov’s principle. In particular, several realizability semantics are presented, which provide interpretations of logical systems by means of diferent computational concepts (mainly, recursive functions and lambda calculi). This eld of research gave origin to the well known paradigm often called Curry-Howard isomorphism, or also propositions as types, that states a correspondence between proofs in logic and programs in computer science. Thanks to this the eld of proof theory, that is the metamathematical investigations of proofs as mathematical objects, became of interest for computer science and in particular for the study of programming languages. By using modern research on the Curry-Howard isomorphism, we will obtain a more re- ned interpretation of Markov’s principle. We will then use this results to investigate the logical properties of systems related to the principle.


submitted in partial fulfillment of the requirements for the degree of Master of Science in Computational Logic Registration Number 1528764  to the Faculty of Informatics at the TU Wien  Vienna, 30th September, 2016

Post to Twitter

Escribe un comentario