|
|
Aspects of the Cut-Elimination Theorem
Rýdl, Jiří ; Švejdar, Vítězslav (vedoucí práce) ; Bílková, Marta (oponent)
I give a proof of the cut-elimination theorem (Gentzen's Hauptsatz) for an intuitionistic multi-succedent calculus. The proof follows the strategy of eliminating topmost maximal-rank cuts that allows for a straightforward way to measure the upper bound of the increase of derivations during the procedure. The elimination of all cut inferences generates a superexponential increase. I follow the structure of the proof for classical logic given in Švejdar's [18], modifying only the critical cases related to two restricted rules. Motivated by the diversity found in the early literature on this topic, I survey selected aspects of various formulations of sequent calculi. These are reflected in the proof of the Hauptsatz and its preliminaries. In the end I give one corollary of cut elimination, the Midsequent theorem, which is one of the three applications to be found already in Gentzen's [10]. Powered by TCPDF (www.tcpdf.org)
|
|
|
Usuzování s nekonzistentními informacemi
Přenosil, Adam ; Bílková, Marta (vedoucí práce) ; Noguera, Carles (oponent) ; Jansana, Ramon (oponent)
Tato dizertační práce studuje extenze čtyřhodnotové Belnapovy-Dunnovy logiky, tzv. superbelnapovské logiky, z pohledu abstraktní algebraické logiky. Popisujeme v ní globální strukturu svazu superbelnapovských logik a ukazu- jeme, že tento svaz lze zcela popsat pomocí tříd konečných grafů splňujících jisté uzávěrové podmínky. Také zde zavádíme teorii tzv. explozivních extenzí a používáme ji k důkazu nových vět o úplnosti pro superbelnapovské logiky. Poté rozvíjeme gentzenovskou teorii důkazů pro tyto logiky a použijeme ji k důkazu věty o interpolaci pro mnoho z těchto logik. Nakonec také studujeme rozšíření Belnapovy-Dunnovy logiky o operátor pravdivosti ∆. Klíčová slova: abstraktní algebraická logika, Belnapova-Dunnova logika, parakonzistentní logika, superbelnapovské logiky
|
|
|
Fragmenty intuicionistické logiky, intermediárích logik a substrukturálních logik (vybrané otázky).
Truhlář, Pavel ; Bílková, Marta (vedoucí práce) ; Sedlár, Igor (oponent)
diplomové práce Pozitivní formule v některých substrukturálních logikách, autor Pavel Truhlář V této diplomové práci budeme zkoumat, které distributivní substrukturální logiky, tak jak jsou definovány v Resstalově knize "An Introduction to Substructural Logics" mají stejný positivní fragment s axiomem slabého vyloučeného třetího a bez něj. Hlavní výsledek této diplomové práce je, že některé substrukturální logiky tuto vlastnost mají. Zopakujeme základní pojmy, tak jak jsou popsány v Resstalově knize, zvláště pak konsekuce, přirozená dedukce, rámcové semantika, Hilbertův systém. Budeme používat věty o korektnosti a úplnosti. Také budeme potřebovat větu o ekvivalenci přirozené dedukce a Hilbertova důkazového systému. Všechny tyto důležité věty jsou ve výše uvedené Resstalově knize. V další části dokážeme náš hlavní výsledek. Budeme používat sémantiku rámců podobně jako de Jongh and Zhao v článku "Positive Formulas in Intuitionistic and Minimal Logic". Definujeme, co to je top model. Poté ukážeme, jak z daného modelu vytvoříme top model. Pro každou formuli definujeme její pozitivní část, to jest formuli, která se na top modelech chová stejně jako původní formule. Pro formulaci naší hlavní věty použijeme Hilbertův kalkulus. Dokážeme ji pomocí věty o dedukci, která platí pro některé typy Hilbertova...
|
|
|
Hypotetické soudy, pravdivost a tvrditelnost
Punčochář, Vít ; Kolman, Vojtěch (vedoucí práce) ; Sedlár, Igor (oponent) ; Bílková, Marta (oponent)
Vít Punčochář Disertační práce na téma: Hypotetické soudy, pravdivost a tvrditelnost Abstrakt: Základním tématem této disertační práce je logika indikativních kondicionálních vět, tj. vět, které mají obvykle tvar Pokud A, tak B. V klasické logice jsou tyto věty analyzovány pomocí tzv. materiální implikace, avšak tato analýza je v mnoha ohledech problematická. Část této práce je věnována rozboru problémů, se kterými se musíme potýkat, když chceme modelovat indikativní kondicionální věty pomocí standardní sémantiky klasické logiky. Je přitom kladen důraz na zdánlivě paradoxní situaci, v níž se přitom ocitáme. Některé obecné principy klasické logiky (jako třeba ten, podle něhož můžeme z věty Platí A nebo B odvodit větu Pokud A neplatí, tak platí B) vypadají na první pohled zcela nezpochybnitelně, avšak přitom mají velmi kontroverzní důsledky. V práci jsou představeny jak pokusy o obhajobu klasické logiky, tak i pokusy o její revizi. Přístupy k logické analýze kondicionálních vět jsou v předkládané práci rozděleny na dva základní druhy: ontický a epistemický. Ontický přístup vymezuje všechny klíčové sémantické pojmy pomocí pojmu pravdivosti, která se v logice chápe jako vztah mezi větami daného jazyka a stavy světa. Oproti tomu epistemický přístup se neopírá o pojem pravdivosti, nýbrž o pojem tvrditelnosti....
|
|
|
Aritmetická úplnost logiky R
Holík, Lukáš ; Švejdar, Vítězslav (vedoucí práce) ; Bílková, Marta (oponent)
Cílem práce bylo s použitím novodobé notace vystavět teorii Rosserovy logiky, vysvětlit do detailu její vztah s Peanovou aritmetikou, ukázat kripkovskou sémantiku a nakonec pomocí autoreference v množném čísle zpracovat důkaz aritmetické úplnosti. V poslední kapitole se pak ukazují některé z vlastností rosserovských sentencí. Powered by TCPDF (www.tcpdf.org)
|
|
|
Undecidability of Some Substructural Logics
Chvalovský, Karel ; Bílková, Marta (vedoucí práce) ; Buszkowski, Vojciech (oponent) ; Galatos, Nick (oponent)
Tato disertační práce se zabývá algoritmickou nerozhodnutelností (neřešitel- ností) dokazatelnosti v některých neklasických logikách. Ve skutečnosti existují dvě přirozené varianty toho problému. Mějme dánu logiku, pak můžeme studovat její množinu teorémů nebo její relaci důsledku, což je obecnější problém. Je známo, že oba tyto problémy mohou být nerozhod- nutelné již pro výrokové logiky a tato disertační práce poskytuje další pří- klady takových logik. Konkrétně se věnujeme výrokovým substrukturálním logikám, které lze získat ze sekventového kalkulu LJ pro intuicionistickou logiku odebráním strukturálních pravidel. Naše hlavní výsledky jsou násle- dující. Ukazujeme nerozhodnutelnost (konečné) relace důsledku pro některé základní neasociativní substrukturální logiky. Dále dokazujeme, že množina teorémů v základní substrukturální logice s pravidlem kontrakce, které ob- vykle způsobuje řadu komplikací, je nerozhodnutelná. Neboť studované logiky mají přirozené algebraické sémantiky, dostáváme také odpovídající algebraické výsledky, které jsou zajímavé samy o sobě.
|
|
|
A Four-Valued Kripke Semantics for Classical and Intuitionistic Logic
Přenosil, Adam ; Bílková, Marta (vedoucí práce) ; Cintula, Petr (oponent)
Práce zavádí logiku, která kombinuje intuicionistickou implikaci s de Morganovskou negací způsobem, který konzervativně rozšiřuje jak klasickou tak intuicionistickou logiku. Tato logika je intuicionistickým protějškem čtyřhodnotové Belnap-Dunnovy logiky. V souvislosti s touto logikou studujeme de Morganovské algebry a jejich rozšíření, zejména jejich rozšíření o konstantu reprezentující nekonzistenci. Dokazujeme dualitu pro takovéto algebry rozšiřující Priestleyovskou dualitu. Také zavádíme pojem slabé modální algebry a dokazujeme pro takovéto algebry dualitu. Nakonec definujeme analytické sekventové kalkuly pro různé logiky de Morganovské negace. Powered by TCPDF (www.tcpdf.org)
|
|
|
Algebraic and Kripke semantics of substructural logics
Arazim, Pavel ; Bílková, Marta (vedoucí práce) ; Běhounek, Libor (oponent)
Tato práce se zabývá distributivním Lambekovým kalkulem, tedy intuicionistickou logikou bez pravidel záměny, kontrakce a oslabení, a především dvěma různými sé- mantikami této logiky, totiž sémantikou algebraickou a kripkovskou. Tyto dvě séman- tiky jsou nejdříve pojednávány ve zvláštních kapitolách a jsou prezentovány některé výsledky, které se jich týkají, např. se ukáže vlastnostnost disjunkce pomocí sloučení dvou Kripkovských modelů. Jádrem práce je nicméně především vztah těchto dvou sémantik, protože je zajímavé porovnávat, co mají společného, a čím se vůbec mohou lišit, když jsou obě sémantikami téže logiky. Bude ukázán překlad kripkovských rámců na algebry a algeber na rámce a dále bude tento překlad rožšířen i na morfismy, čímž budou zkonstruovány dva funktory mezi oběma kategoriemi. Klíčová slova:distributivní logika FL, distributivní Lambekův kalkul, strukturální pravidla, distributivní residuované svazy, kripkovské rámce, morfismy mezi rámci, kategorie, funktor 3
|
|
|
Dynamické epistemické logiky
Pivoňková, Martina ; Bílková, Marta (vedoucí práce) ; Sedlár, Igor (oponent)
V této práci se budeme zabývat logikou veřejného prohlášení, která je dynamickým rozšířením epistemické logiky. Nejprve vyložíme logiku pravdivého veřejného prohlášení pro multiagentní systém S5, a poté budeme zkoumat, jak by mělo vypadat veřejné prohlášení v systémech slabších než je S5. Zaměříme se konkrétně na systémy, v nichž neplatí axiom T a epistemický operátor nutnosti se v nich interpretuje nikoli jako "znalost , nýbrž jako "přesvědčení . Vytvoříme tak novou sé- mantiku veřejného prohlášení, které už nemusí být pravdivé, je ovšem jako pravdivé přijímáno. Systémy rozšířené o takovéto veřejné prohlá- šení se rovněž pokusíme axiomatizovat. Klíčová slova: logika veřejného prohlášení, logika přesvědčení
|
|
| |
host ::
RSS.