velikost textu

Dôkazy bezespornosti aritmetiky

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:
Dôkazy bezespornosti aritmetiky
Název v angličtině:
Cut Elimination and Consistency Proofs
Typ:
Disertační práce
Autor:
Mgr. Anna Horská
Školitel:
prof. RNDr. Pavel Pudlák, DrSc.
Oponenti:
Mgr. Pavel Hrubeš, Ph.D.
prof. Samuel Buss
Id práce:
147143
Fakulta:
Filozofická fakulta (FF)
Pracoviště:
Katedra logiky (21-KLOG)
Program studia:
Logika (P6142)
Obor studia:
Logika (XLG)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
1. 11. 2017
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Klíčová slova:
eliminácia rezu|bezespornosť Peanovej aritmeitky|Gerhard Gentzen|Veblenova hierarchia|nekonečné kalkuly
Klíčová slova v angličtině:
cut elimination|consistency of Peano arithmetic|Gerhard Gentzen|Veblen hierarchy|infinitary calculus
Abstrakt:
Abstrakt Táto práca pozostáva z dvoch častí. Prvá čast sa zaoberá Gentze- novým dôkazom bezespornosti Peanovej aritmetiky (PA), ktorý pochádza z roku 1935. Skúmame hlavne Gentzenovu stratégiu eliminácie rezu, ktorá eliminuje rezy, ktorých premisy majú bezrezové odvodenia. Neberie sa pritom ohĺ ad na zložitosť eliminovaného rezu. Naša analýza Gentzenovej stratégie ukázala, že Gentzen vo svojom dôkaze implicitne využíva transfinitnú induk- ciu po Φω(0), kde Φω je Veblenova funkcia s poradovým číslom ω. Jedná sa o horný odhad a hodnota Φω(0) je horný odhad na výšku nekonečných bezrezových odvodení, ktoré Gentzen konštruuje pre sekventy dokazateĺ né v PA. V súčasnosti nemáme výsledky o spodnom odhade. Prvá časť d’alej obsahuje formalizáciu tohto Gentzenovho dôkazu. Na základe nej vidíme, že hore spomínaná transfinitná indukcia je jediný princíp použitý v dôkaze, ktorý nejde formalizovať v PA. Druhá časť porovnáva Gentzenovu a Taitovu stratégiu eliminácie rezu v kla- sickej výrokovej logike. Taitova stratégia znižuje tzv. cut-rank odvodenia. Ked’že výroková logika nepoužíva odvodzovacie pravidlá s vlastnými pre- mennými, s tzv. eigenvariables, podarilo sa nám nadefinovať elimináciu rezu tak, že obe stratégie dávajú v klasickej výrokovej logike identické bezrezové odvodenia.
Abstract v angličtině:
Abstract 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.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce Mgr. Anna Horská 671 kB
Stáhnout Abstrakt v českém jazyce Mgr. Anna Horská 43 kB
Stáhnout Abstrakt anglicky Mgr. Anna Horská 43 kB
Stáhnout Autoreferát / teze disertační práce Mgr. Anna Horská 189 kB
Stáhnout Posudek vedoucího prof. RNDr. Pavel Pudlák, DrSc. 48 kB
Stáhnout Posudek oponenta Mgr. Pavel Hrubeš, Ph.D. 100 kB
Stáhnout Posudek oponenta prof. Samuel Buss 1.34 MB
Stáhnout Záznam o průběhu obhajoby 22 kB