|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (vedoucí práce) ; Hrubeš, Pavel (oponent) ; Buss, Samuel (oponent)
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 ohl'ad na zložitost' 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 dokazatel'né v PA. V súčasnosti nemáme výsledky o spodnom odhade. Prvá čast' 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 formalizovat' v PA. Druhá čast' 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 nadefinovat' elimináciu rezu tak, že obe stratégie dávajú v...
|
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (vedoucí práce) ; Hrubeš, Pavel (oponent) ; Buss, Samuel (oponent)
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 ohl'ad na zložitost' 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 dokazatel'né v PA. V súčasnosti nemáme výsledky o spodnom odhade. Prvá čast' 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 formalizovat' v PA. Druhá čast' 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 nadefinovat' elimináciu rezu tak, že obe stratégie dávajú v...
|
|
|
Gentzen's Consistency Proof
Horská, Anna ; Švejdar, Vítězslav (vedoucí práce) ; Velebil, Jiří (oponent)
Práca podáva podrobne vysvetlené dva dôkazy bezespornosti Peanovej aritmetiky, ktoré v rokoch 1936 a 1938 uverejnil nemecký matematik Gerhard Gentzen. Dôkazy boli naštudované z pôvodných zdrojov, a to z článkov "Die Widerspruchsfreiheit der reinen Zahlentheorie" a "Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie". Prvý z uvedených dôkazov je zaujímavý z historického hľadiska, Gentzen pri ňom využíva kalkul prirodzenej dedukcie a ordinálne čísla, ktoré kvôli dôkazu sám vymyslel. Druhý dôkaz je viac-menej dnes bežne známy ako dôkaz bezespornosti Peanovej aritmetiky.
|
host ::
RSS.