|
|
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (vedoucí práce) ; Beckmann, Arnold (oponent) ; Iemhoff, Rosalie (oponent)
Vo svetle intuicionizmu: dve štúdie v teórii dôkazov Táto práca pojednáva o dvoch špecifických aspektoch vzt'ahu medzi klasickou a intuicionistickou teóriou dôkazov. V prvej časti zavedieme, s použitím odvodení v klasickej aritmetike, formalizáciu pre Gödelov neformálny výklad BHK interpretácie. Gödelova interpretácia dokazatel'nosti pre intuicionistic- kú výrokovú logiku bola prvý raz publikovaná v [1]. Definoval tu modálny systém S4 ako formalizáciu pre intuitívny koncept dokazatel'nosti, a po- tom preložil IPC na S4 pri zachovaní korektnosti a úplnosti. Gödelova práca navrhuje hl'adat' interpretáciu dokazatel'nosti pre modálnu logiku S4 s použitím aritmetických dôkazov, ktorá samotná vedie k takejto interpretácii dokazatel'nosti pre intuicionistickú logiku. V prvej kapitole sa pokúsime vyriešit' tento problém. Zovšeobecníme Solovayovu interpretáciu dokazatel'- nosti pre modálnu logiku GL, aby sme zachytili iné modálne logiky, konkrétne K4, KD4 a S4. S použitím už spomínaného Gödelovho prekladu navrhneme formalizáciu BHK interpretácie pomocou dôkazov v klasickej logike. Ako dôsledok ukážeme, že BHK interpretácia je dostatočne silná a umožňuje viacero rôznych formalizácií, ktoré prekvapivo zachytávajú rôzne výrokové logiky...
|
|
|
In the Light of Intuitionism: Two Investigations in Proof Theory
Akbartabatabai, Seyedamirhossein ; Pudlák, Pavel (vedoucí práce) ; Beckmann, Arnold (oponent) ; Iemhoff, Rosalie (oponent)
Vo svetle intuicionizmu: dve štúdie v teórii dôkazov Táto práca pojednáva o dvoch špecifických aspektoch vzt'ahu medzi klasickou a intuicionistickou teóriou dôkazov. V prvej časti zavedieme, s použitím odvodení v klasickej aritmetike, formalizáciu pre Gödelov neformálny výklad BHK interpretácie. Gödelova interpretácia dokazatel'nosti pre intuicionistic- kú výrokovú logiku bola prvý raz publikovaná v [1]. Definoval tu modálny systém S4 ako formalizáciu pre intuitívny koncept dokazatel'nosti, a po- tom preložil IPC na S4 pri zachovaní korektnosti a úplnosti. Gödelova práca navrhuje hl'adat' interpretáciu dokazatel'nosti pre modálnu logiku S4 s použitím aritmetických dôkazov, ktorá samotná vedie k takejto interpretácii dokazatel'nosti pre intuicionistickú logiku. V prvej kapitole sa pokúsime vyriešit' tento problém. Zovšeobecníme Solovayovu interpretáciu dokazatel'- nosti pre modálnu logiku GL, aby sme zachytili iné modálne logiky, konkrétne K4, KD4 a S4. S použitím už spomínaného Gödelovho prekladu navrhneme formalizáciu BHK interpretácie pomocou dôkazov v klasickej logike. Ako dôsledok ukážeme, že BHK interpretácia je dostatočne silná a umožňuje viacero rôznych formalizácií, ktoré prekvapivo zachytávajú rôzne výrokové logiky...
|
|
|
Interpolation in modal logics
Bílková, Marta ; Pudlák, Pavel (vedoucí práce) ; Švejdar, Vítězslav (oponent) ; Iemhoff, Rosalie (oponent)
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...
|
host ::
RSS.