Detailansicht
Semantic methods in bounded arithmetic
Thomas Imre
Art der Arbeit
Masterarbeit
Universität
Universität Wien
Fakultät
Fakultät für Mathematik
Studiumsbezeichnung bzw. Universitätlehrgang (ULG)
Masterstudium Mathematik
Betreuer*in
Sy-David Friedman
Mitbetreuer*in
Moritz Müller
DOI
10.25365/thesis.40566
URN
urn:nbn:at:at-ubw:1-30491.09220.671666-3
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
Der Schwerpunkt dieser Arbeit ist Bounded Arithmetic.
Im ersten Teil führen wir Herbrand-saturierte Strukturen ein und zeigen folgendes Theorem: Wenn jedes Herbrand-saturierte Modell einer universellen Theorie T' auch Modell einer Theorie T der gleichen Sprache ist, dann ist T $\forall\exists$-konservativ über T'. Als Anwendung dieses Theorems beweisen wir folgendes: Sei $UPV_i$ die Theorie aller wahren universellen Sätze in der Sprache, die aus den Funktionen besteht, die in polynomieller Zeit von einer Turing-Maschine mit $Sigma_{i-1}^p$-Orakel berechenbar sind. Darüber hinaus sei $US^1_2(FP_i)$ die Theorie $UPV_i$ mit zusätzlicher length minimization für strikte Sigma_1^b-Formeln in dieser Sprache. Dann ist $US^1_2(FP_i)$ konservativ über $UPV_i$ für $\forall\exists$-Sätze.
Das zweite große Thema, das in dieser Arbeit behandelt wird, ist die Simulation von Widerspruchsbeweisen aussagenlogischer Formeln. Wir entwickeln eine Methode, prädikatenlogische Formeln erster Stufe in aussagenlogische Formeln zu übersetzen. Anschließend führen wir eine Codierung dieser Übersetzung und von Widerspruchsbeweisen ein. Weiters definieren wir eine Wahrheitsformel für Codes aussagenlogischer Formeln. Wir wenden diese Resultate an, um das Haupttheorem dieses Kapitels zu beweisen: Sei $\varphi$ ein unnested Satz in einer größeren Sprache als der Sprache aller definierbaren Funktionen und Relationen im Standardmodell der Arithmetik und M ein abzählbares Nichtstandardmodell der Arithmetik. Wenn der Satz $\varphi$, bei dem alle Quantoren durch eine nichtstandard Zahl beschränkt sind, in einer Expansion von M wahr ist, dann existieren keine polynomiell großen Widerspruchsbeweise der aussagenlogischen Übersetzungen von $\varphi$.
Abstract
(Englisch)
The focus of this thesis is on Bounded Arithmetic.
In the first part, we introduce the notion of Herbrand-saturated structures and prove the main result of this chapter: If every Herbrand-saturated model of a universal theory T' is also a model of a theory T in the same language, then T is $\forall\exists$-conservative over T'. As an application of this theorem, we show the following: Let $UPV_i$ be the theory of all true universal sentences in the language consisting of polynomial time functions with $\Sigma_{i-1}^p$-oracle in the standard model and let $US^1_2(FP_i)$ be the theory $UPV_i$ plus length minimization for strict $\Sigma_1^b$-formulas in that language. Then $US^1_2(FP_i)$ is $\forall\exists$-conservative over $UPV_i$.
The second main topic discussed in this thesis is simulation of propositional refutations. In this chapter, we develop a method for translating first-order sentences into propositional formulas. Then we show how we code such formulas as well as refutations. Further, we introduce a truth formula for codes of propositional formulas. Combining all the results, we prove the main theorem of this part: Let $\varphi$ be an unnested sentence in a bigger language than the language of all definable functions and relations in the standard model of arithmetic and let M be a countable nonstandard model of arithmetic. If the sentence $\varphi$ with all quantifiers bounded by some nonstandard integer is true in an expansion of M, then there are no polynomial size refutations of the propositional translations of $\varphi$.
Schlagwörter
Schlagwörter
(Englisch)
Bounded arithmetic Conservation Propositional translations
Schlagwörter
(Deutsch)
Beschränkte Arithmetik Konservativität Aussagenlogische Übersetzungen
Autor*innen
Thomas Imre
Haupttitel (Englisch)
Semantic methods in bounded arithmetic
Paralleltitel (Deutsch)
Semantische Methoden in Bounded Arithmetic
Publikationsjahr
2015
Umfangsangabe
89 S.
Sprache
Englisch
Beurteiler*in
Sy-David Friedman
Klassifikation
31 Mathematik > 31.10 Mathematische Logik, Mengenlehre
AC Nummer
AC12699410
Utheses ID
35927
Studienkennzahl
UA | 066 | 821 | |