|
|
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...
|
|
|
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...
|
|
|
Interpolation in modal logics
Bílková, Marta ; Pudlák, Pavel (advisor) ; Švejdar, Vítězslav (referee) ; Iemhoff, Rosalie (referee)
Since Craig's landmark result on interpolation for classical predicate logic, proved as the main technical lemma in [14], interpolation is considered one of the centra! concepts in pure logic. Various interpolation properties find their applications in computer science and have many deep purely logical consequences. We focus on two propositional versions of Craig interpolation property: Craig Interpolation Property: for every provable implication (A -+ B) there is an interpolant I containing only only common variables of A and B such that both implications (A -+ I) and (I-+ B) are provable. Craig interpolation, although it seems rather technical, is a deep logical property. It is dosely related to expressive power of a logic - as such it entails Beth's definability property, or forces functional completeness. It is also related to Robinson's joint consistency of two theories that agree on the common language. Craig interpolation has an important algebraic counterpart - it entails amalgamation or superamalgamation property of appropriate algebraic structures. In case of modal provability logics, Craig interpolation entails fixed point theorem. There are other interpolation properties, defined w.r.t. a consequence relation rather then w.r.t. a provable implication. In presence of deduction theorem the two...
|
guest ::
