velikost textu

Undecidability of Some Substructural Logics

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:
Undecidability of Some Substructural Logics
Název v češtině:
Nerozhodnutelnost některých substrukturálních logik
Typ:
Disertační práce
Autor:
Mgr. Karel Chvalovský
Školitel:
Mgr. Marta Bílková, Ph.D.
Oponenti:
prof. Vojciech Buszkowski
prof. Nick Galatos
Id práce:
101527
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:
10. 6. 2015
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Klíčová slova:
substrukturální logiky, nerozhodnutelnost, dokazatelnost, sekventové kalkuly
Klíčová slova v angličtině:
substructural logics, undecidability, provability, sequent calculi
Abstrakt:
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ě.
Abstract v angličtině:
This thesis deals with the algorithmic undecidability (unsolvability) of provability in some non-classical logics. In fact, there are two natural variants of this problem. Fix a logic, we can study its set of theorems or its consequence relation, which is a more general problem. It is well-known that both these problems can be undecidable already for propositional logics and we provide further examples of such logics in this thesis. In particular, we study propositional substructural logics which are obtained from the sequent calculus LJ for intuitionistic logic by dropping structural rules. Our main results are the following. First, (finite) consequence relations in some basic non-associative substructural logics are shown to be undecidable. Second, we prove that a basic associative substructural logic with the contraction rule, which is notorious for being hard to handle, has an undecidable set of theorems. Since the studied logics have natural algebraic semantics, we also obtain corresponding algebraic results which are interesting in their own right.
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce Mgr. Karel Chvalovský 900 kB
Stáhnout Abstrakt v českém jazyce Mgr. Karel Chvalovský 29 kB
Stáhnout Abstrakt anglicky Mgr. Karel Chvalovský 25 kB
Stáhnout Autoreferát / teze disertační práce Mgr. Karel Chvalovský 359 kB
Stáhnout Posudek vedoucího Mgr. Marta Bílková, Ph.D. 136 kB
Stáhnout Posudek oponenta prof. Vojciech Buszkowski 87 kB
Stáhnout Posudek oponenta prof. Nick Galatos 101 kB
Stáhnout Záznam o průběhu obhajoby 98 kB