|
|
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (advisor) ; Beckmann, Arnold (referee) ; Iemhoff, Rosalie (referee)
In the Light of Intuitionism: Two Investigations in Proof Theory This dissertation focuses on two specific interconnections between the clas- sical and the intuitionistic proof theory. In the first part, we will propose a formalization for Gödel's informal reading of the BHK interpretation, using the usual classical arithmetical proofs. His provability interpretation of the propositional intuitionistic logic, first appeared in [1], in which he introduced the modal system, S4, as a formalization of the intuitive concept of prov- ability and then translated IPC to S4 in a sound and complete manner. His work suggested the search for a concrete provability interpretation for the modal logic S4 which itself leads to a concrete provability interpretation for the intutionistic logic. In the first chapter of this work, we will try to solve this problem. For this purpose, we will generalize Solovay's provabil- ity interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. Then, using the mentioned Gödel's translation, we will propose a formalization for the BHK interpretation via classical proofs. As a consequence, it will be shown that the BHK interpretation is powerful enough to admit many different formalizations that surprisingly capture dif- ferent propositional logics, including...
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (advisor) ; Thapen, Neil (referee) ; Kolodziejczyk, Leszek (referee)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
|
|
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (advisor) ; Beckmann, Arnold (referee) ; Iemhoff, Rosalie (referee)
In the Light of Intuitionism: Two Investigations in Proof Theory This dissertation focuses on two specific interconnections between the clas- sical and the intuitionistic proof theory. In the first part, we will propose a formalization for Gödel's informal reading of the BHK interpretation, using the usual classical arithmetical proofs. His provability interpretation of the propositional intuitionistic logic, first appeared in [1], in which he introduced the modal system, S4, as a formalization of the intuitive concept of prov- ability and then translated IPC to S4 in a sound and complete manner. His work suggested the search for a concrete provability interpretation for the modal logic S4 which itself leads to a concrete provability interpretation for the intutionistic logic. In the first chapter of this work, we will try to solve this problem. For this purpose, we will generalize Solovay's provabil- ity interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. Then, using the mentioned Gödel's translation, we will propose a formalization for the BHK interpretation via classical proofs. As a consequence, it will be shown that the BHK interpretation is powerful enough to admit many different formalizations that surprisingly capture dif- ferent propositional logics, including...
|
|
|
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
|
|
|
On the Power of Weak Extensions of V0
Müller, Sebastian Peter ; Krajíček, Jan (advisor) ; Thapen, Neil (referee) ; Kolodziejczyk, Leszek (referee)
Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....
|
guest ::
