<div class="csl-bib-body">
<div class="csl-entry">Manighetti, M. (2016). <i>Computational interpretations of Markov’s principle</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2016.37906</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2016.37906
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/1622
-
dc.description
Zusammenfassung in deutscher Sprache
-
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Logik
de
dc.subject
Beweistheorie
de
dc.subject
Typentheorie
de
dc.subject
Intuitionismus
de
dc.subject
Logic
en
dc.subject
Proof theory
en
dc.subject
Type theory
en
dc.subject
Intuitionism
en
dc.title
Computational interpretations of Markov's principle
en
dc.title.alternative
Berechnungsinterpretationen des Markov-Prinzip
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2016.37906
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Matteo Manighetti
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Aschieri, Federico
-
tuw.publication.orgunit
E104 - Institut für Diskrete Mathematik und Geometrie
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC13687273
-
dc.description.numberOfPages
63
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-97119
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-6461-5982
-
item.fulltext
with Fulltext
-
item.grantfulltext
open
-
item.cerifentitytype
Publications
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cf
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cf
-
item.openairetype
Thesis
-
item.openairetype
Hochschulschrift
-
item.openaccessfulltext
Open Access
-
crisitem.author.dept
E104 - Institut für Diskrete Mathematik und Geometrie