velikost textu

In the Light of Intuitionism: Two Investigations in Proof Theory

Upozornění: Informace získané z popisných dat či souborů uložených v Repozitáři závěrečných prací nemohou být použity k výdělečným účelům nebo vydávány za studijní, vědeckou nebo jinou tvůrčí činnost jiné osoby než autora.
Název:
In the Light of Intuitionism: Two Investigations in Proof Theory
Název v češtině:
Vo svetle intuicionizmu: dve štúdie v teórii dôkazov
Typ:
Disertační práce
Autor:
Seyedamirhossein Akbartabatabai, Ph.D.
Školitel:
prof. RNDr. Pavel Pudlák, DrSc.
Oponenti:
Arnold Beckmann
Rosalie Iemhoff, Ph.D.
Id práce:
164209
Fakulta:
Matematicko-fyzikální fakulta (MFF)
Pracoviště:
Matematický ústav AV ČR, v.v.i. (32-MUAV)
Program studia:
Matematika (P1101)
Obor studia:
Algebra, teorie čísel a matematická logika (4M1)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
20. 12. 2018
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Klíčová slova:
interpretácia dokazateľnosti, BHK interpretácia, proof mining, aritmetika s obmedzenou indukciou
Klíčová slova v angličtině:
Provability Interpretation, BHK Interpretation, Proof Mining, Bounded Arithmetic
Abstrakt:
Vo svetle intuicionizmu: dve štúdie v teórii dôkazov Táto práca pojednáva o dvoch špecifických aspektoch vzť 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 dokazateĺ 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 dokazateĺ nosti, a po- tom preložil IPC na S4 pri zachovaní korektnosti a úplnosti. Gödelova práca navrhuje hĺ adať interpretáciu dokazateĺ nosti pre modálnu logiku S4 s použitím aritmetických dôkazov, ktorá samotná vedie k takejto interpretácii dokazateĺ nosti pre intuicionistickú logiku. V prvej kapitole sa pokúsime vyriešiť tento problém. Zovšeobecníme Solovayovu interpretáciu dokazateĺ - 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 vrátane intuicionistickej, minimálnej a Visser-Ruitenburgovej basic logiky. Napokon prezentujeme negatívne výsledky ukazujúce, že neexistu- je interpretácia dokazateĺ nosti pre ĺ ubovoĺ né rozšírenie systémuKD45 a v súlade s očakávaním neexistuje žiadna BHK interpretácia pre klasickú výrokovú logiku. V druhej polovici dizertácie sa sústredíme na d’alší spomínaný aspekt a budeme skúmať aplikáciu intuicionistického hĺ adiska v teórii dôkazov kla- sickej logiky. Za týmto účelom zovšeobecníme klasickú verziu Dialectica in- terpretácie tak, aby brala do úvahy zložitosť dôkazov a využijeme ju pri skúmaní podsystémov aritmetiky s obmedzenou indukciou. Konkrétne, de- finujeme pojem výpočtový tok (computational flow), čo bude dvojica po- zostávajúca z postupnosti výpočetných problémov istého typu a postupnosti redukcií medzi nimi. Na základe teórie, ktorú vypracujeme pre výpočtové toky, získame korektnú a úplnú interpretáciu pre podsystémy aritmetiky s obmedzenou indukciou. Tieto vlastnosti využijeme pri transformácii pr- vorádových aritmetických dôkazov na postupnosti výpočetných redukcií, po- mocou ktorých extrahujeme výpočetný obsah niektorých tvrdení v niektorých k podsystémoch aritmetiky vrátane I∆0, Tn , I∆0(exp) a PRA. V poslednej časti zobecníme toky konečných dĺžok na toky nekonečné a presunieme náš záujem zo systémov s obmedzenou indukciou na systémy PA a PA + TI(α) s neobmedzenou indukciou. Kĺ účové slová: interpretácia dokazateĺ nosti, BHK interpretácia, aritmetika s obmedzenou indukciou, proof mining References [1] K. Gödel, Eine Interpretation des Intuitionistichen Aussagenkalküls, Ergebnisse Math Colloq. Vol. 4 (1933), pp. 39-40. 2
Abstract v angličtině:
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 intuitionistic logic, minimal logic and Visser-Ruitenburg’s basic logic. We will also present some negative results to show that there is no provability interpretation for any extension of the system KD45 and as we expected there is no BHK interpretation for the classical propositional logic. In the second half of the dissertation, we change our focus to the other direc- tion of the interconnection to investigate the applications of the intuitionistic viewpoint in the realm of classical proof theory. For this purpose, we will develop a complexity sensitive version of the classical Dialectica interpreta- tion to deal with the bounded theories of arithmetic. More precisely, we will define a notion called the computational flow which is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. We will develop a theory for these flows to provide a sound and complete interpretation for bounded theories of arithmetic. This property helps us to transform a first order arithmetical proof to a sequence of computational reductions by which we can extract the computational content of low complexity statements in some bounded k theories of arithmetic including I∆0, Tn , I∆0(exp) and PRA. Then, in the last section, by generalizing term-length flows to ordinal-length flows, we will extend our investigations from bounded theories to strong unbounded systems such as PA and PA+TI(α) to capture their total NP search problems. Keywords: Provability Interpretation, BHK Interpretation, Proof Mining, Bounded Arithmetic References [1] K. Gödel, Eine Interpretation des Intuitionistichen Aussagenkalküls, Ergebnisse Math Colloq. Vol. 4 (1933), pp. 39-40. 2
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce Seyedamirhossein Akbartabatabai, Ph.D. 1.24 MB
Stáhnout Abstrakt v českém jazyce Seyedamirhossein Akbartabatabai, Ph.D. 58 kB
Stáhnout Abstrakt anglicky Seyedamirhossein Akbartabatabai, Ph.D. 58 kB
Stáhnout Posudek vedoucího prof. RNDr. Pavel Pudlák, DrSc. 86 kB
Stáhnout Posudek oponenta Arnold Beckmann 292 kB
Stáhnout Posudek oponenta Rosalie Iemhoff, Ph.D. 61 kB
Stáhnout Záznam o průběhu obhajoby prof. RNDr. Jan Krajíček, DrSc. 69 kB