Title (eng)
Semantic methods in bounded arithmetic
Parallel title (deu)
Semantische Methoden in Bounded Arithmetic
Author
Thomas Imre
Advisor
Sy-David Friedman
Co-Advisor
Moritz Müller
Assessor
Sy-David Friedman
Abstract (deu)
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 (eng)
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$.
Keywords (eng)
Bounded arithmeticConservationPropositional translations
Keywords (deu)
Beschränkte ArithmetikKonservativitätAussagenlogische Übersetzungen
Subject (deu)
Type (deu)
Persistent identifier
https://phaidra.univie.ac.at/o:1323378
rdau:P60550 (deu)
89 S.
Number of pages
90
Association (deu)
Title (eng)
Semantic methods in bounded arithmetic
Parallel title (deu)
Semantische Methoden in Bounded Arithmetic
Author
Thomas Imre
Abstract (deu)
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 (eng)
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$.
Keywords (eng)
Bounded arithmeticConservationPropositional translations
Keywords (deu)
Beschränkte ArithmetikKonservativitätAussagenlogische Übersetzungen
Subject (deu)
Type (deu)
Persistent identifier
https://phaidra.univie.ac.at/o:1323379
Number of pages
90
Association (deu)
License
Citable links
Other links
Managed by
Details
Metadata
Export formats
Universitätsring 1, 1010 Wien | T
T +43-1-4277-0