|
|
(Im)possibilty results in Proof Complexity and Arithmetic
Khaniki, Erfan ; Pudlák, Pavel (advisor) ; Buss, Samuel (referee) ; Kolodziejczyk, Leszek (referee)
Title: (Im)possibilty results in Proof Complexity and Arithmetic Author: Erfan Khaniki Department: Department of Algebra Supervisor: Prof. RNDr. Pavel Pudl'ak, DrSc Abstract: We study various problems in proof complexity, bounded arithmetic, and intuitionistic arithmetic. We focus on topics such as lower bounds for different proof systems, connections between proof complexity generators and models of arithmetic, jump operators in proof complexity, and the non-locality of certain Kripke models of Heyting arithmetic. Keywords: Proof complexity, Lower bounds, Bounded arithmetic, Independence, Heyt- ing arithmetic, Kripke models 1
|
|
|
Model constructions for bounded arithmetic
Garlík, Michal ; Krajíček, Jan (advisor) ; Buss, Samuel (referee) ; Thapen, Neil (referee)
Title: Model constructions for bounded arithmetic Author: Michal Garlík Abstract: We study constructions of models of bounded arithmetic theories. Us- ing basic techniques of model theory we give a new proof of Ajtai's completeness theorem for nonstandard finite structures. Working in the framework of restricted reduced powers (a generalization of the ultrapower construction) we devise two methods of constructing models of bounded arithmetic. The first one gives a new proof of Buss's witnessing theorem. Using the second method we show that the theory R1 2 is stronger than its variant strictR1 2 under a plausible computational assumption (the existence of a strong enough one-way permutation), and that the theory PV1 + Σb 1(PV ) − LLIND is stronger than PV1 + strictΣb 1(PV ) − LLIND under the same assumption. Considering relativized theories, we show that R1 2(α) is stronger than strictR1 2(α) (unconditionally). 1
|
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (advisor) ; Hrubeš, Pavel (referee) ; Buss, Samuel (referee)
The thesis consists of two parts. The first one deals with Gentzen's consistency proof of 1935, especially with the impact of his cut elimination strategy on the complexity of the proof. Our analysis of Gentzen's cut elimi- nation strategy, which eliminates uppermost cuts regardless of their comple- xity, yields that, in his proof, Gentzen implicitly applies transfinite induction up to Φω(0) where Φω is the ω-th Veblen function. This is an upper bound and Φω(0) represents an upper bound on heights of cut-free infinitary deriva- tions that Gentzen constructs for sequents derivable in Peano arithmetic (PA). We currently do not know whether this is a lower bound too. The first part also contains a formalization of Gentzen's proof of 1935. Based on the formalization, we see that the transfinite induction mentioned above is the only principle used in the proof that exceeds PA. The second part compares the performance of Gentzen's and Tait's cut elimi- nation strategy in classical propositional logic. Tait's strategy reduces the cut-rank of the derivation. Since the propositional logic does not use inference rules with eigenvariables, we managed to organize the cut elimination in the way that both strategies yield identical cut-free derivations in classical propositional logic.
|
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (advisor) ; Hrubeš, Pavel (referee) ; Buss, Samuel (referee)
The thesis consists of two parts. The first one deals with Gentzen's consistency proof of 1935, especially with the impact of his cut elimination strategy on the complexity of the proof. Our analysis of Gentzen's cut elimi- nation strategy, which eliminates uppermost cuts regardless of their comple- xity, yields that, in his proof, Gentzen implicitly applies transfinite induction up to Φω(0) where Φω is the ω-th Veblen function. This is an upper bound and Φω(0) represents an upper bound on heights of cut-free infinitary deriva- tions that Gentzen constructs for sequents derivable in Peano arithmetic (PA). We currently do not know whether this is a lower bound too. The first part also contains a formalization of Gentzen's proof of 1935. Based on the formalization, we see that the transfinite induction mentioned above is the only principle used in the proof that exceeds PA. The second part compares the performance of Gentzen's and Tait's cut elimi- nation strategy in classical propositional logic. Tait's strategy reduces the cut-rank of the derivation. Since the propositional logic does not use inference rules with eigenvariables, we managed to organize the cut elimination in the way that both strategies yield identical cut-free derivations in classical propositional logic.
|
|
|
Model constructions for bounded arithmetic
Garlík, Michal ; Krajíček, Jan (advisor) ; Buss, Samuel (referee) ; Thapen, Neil (referee)
Title: Model constructions for bounded arithmetic Author: Michal Garlík Abstract: We study constructions of models of bounded arithmetic theories. Us- ing basic techniques of model theory we give a new proof of Ajtai's completeness theorem for nonstandard finite structures. Working in the framework of restricted reduced powers (a generalization of the ultrapower construction) we devise two methods of constructing models of bounded arithmetic. The first one gives a new proof of Buss's witnessing theorem. Using the second method we show that the theory R1 2 is stronger than its variant strictR1 2 under a plausible computational assumption (the existence of a strong enough one-way permutation), and that the theory PV1 + Σb 1(PV ) − LLIND is stronger than PV1 + strictΣb 1(PV ) − LLIND under the same assumption. Considering relativized theories, we show that R1 2(α) is stronger than strictR1 2(α) (unconditionally). 1
|
|
|
Complexity theory in Feasible Mathematics
Pich, Ján ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee) ; Buss, Samuel (referee)
Title: Complexity Theory in Feasible Mathematics Author: Ján Pich Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., MAE Abstract: We study the provability of statements and conjectures from Complex- ity Theory in Bounded Arithmetic. First, modulo a hardness assumption, we show that theories weaker in terms of provably total functions than Buss's theory S1 2 cannot prove nk -size circuit lower bounds for SAT formalized as a Σb 2-formula LB(SAT, nk ). In particular, the true universal first-order theory in the language containing names for all uniform NC1 algorithms denoted TNC1 does not prove LB(SAT, n4kc ) where k ≥ 1, c ≥ 2 unless each function f ∈ SIZE(nk ) can be approximated by formulas Fn of subexponential size 2O(n1/c) with subexponential advantage: Px∈{0,1}n [Fn(x) = f(x)] ≥ 1/2 + 1/2O(n1/c) . Unconditionally, V 0 does not prove quasipolynomial nlog n -size circuit lower bounds for SAT. Considering upper bounds, we prove the PCP theorem in Cook's theory PV1. This includes a formalization of the (n, d, λ)-graphs in PV1. A consequence of the result is that Extended Frege proof system admits p-size proofs of tautologies encoding the PCP theorem. Keywords: Circuit Lower Bounds, Bounded Arithmetic, The PCP theorem
|
guest ::
