Title: Computational interpretations of Markov's principle
Language: English
Authors: Manighetti, Matteo 
Qualification level: Diploma
Advisor: Hetzl, Stefan 
Assisting Advisor: Aschieri, Federico 
Issue Date: 2016
Number of Pages: 63
Qualification level: Diploma
Markov's principle is 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 different 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 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 different 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 different computational concepts (mainly, recursive functions and lambda calculi). This field of research gave origin to the well known paradigm often called Curry-Howrd isomorphism, or also propositions as types, that states a correspondence between proofs in logic and programs in computer science. Thanks to this the field 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 refined interpretation of Markov's principle. We will then use this results to investigate the logical properties of systems related to the principle, and introduce a proof transformation technique to interpret constructively some non-constructive proofs of arithmetic.
Keywords: Logik; Beweistheorie; Typentheorie; Intuitionismus
Logic; Proof theory; Type theory; Intuitionism
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-97119
Library ID: AC13687273
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Page view(s)

checked on Jul 11, 2021


checked on Jul 11, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.