|
|
Intuicionistická logika jako užitečný nástroj
Vachková, Eva ; Švejdar, Vítězslav (vedoucí práce) ; Bílková, Marta (oponent)
V této práci se zabýváme intuicionistickou logikou a úplností gentzenovského kalkulu vůči její sémantice. V důkazu úplnosti jsou využity saturované sekventy. Jazyk, který bereme v úvahu, je nejvýše spočetný. Dále se práce zaměřuje na jedno z rozšíření intuicionistické logiky, a sice intuicionistickou logiku s konstantním univerzem, někdy nazývanou Grzegorczykovou. Zabýváme se Markovovým principem, díky němuž dokážeme, že gentzenovský kalkulus upravený pro tuto logiku nemá bezřezovou úplnost vůči Grzegorczykově sémantice. Značná pozornost je věnována Heytingovým algebrám, jedné z možných sémantik intuicionistické výrokové logiky. Ukážeme, že Rieger-Nishimurův svaz je také Heytingova algebra. Na Heytingových algebrách definujeme filtry a ultrafiltry a s jejich pomocí pak dostaneme kripkovské rámce. Dokážeme, že v těchto rámcích platí tytéž formule jako v Heytingových algebrách.
|
|
|
Intuitionistic logic and axiomatic theories
Brablec, Vladimír ; Švejdar, Vítězslav (vedoucí práce) ; Jeřábek, Emil (oponent)
Pr ace zkoum a vlastnosti n ekter ych element arn ch intuicionistick ych teori . Vybr any jsou n asleduj c teorie: teorie rovnosti, line arn ho uspo r ad an , hust eho line arn ho uspo r ad an , teorie n asledn ka, Robinsonova aritmetika a teorie s c t an racion aln ch c sel; nav c t em e r ka zdou z t echto teori formulujeme dv ema r uzn ymi zp usoby. Z vlastnost teori n as zaj maj p redev s m n asleduj c cty ri: spl yv an s klasickou verz teorie, saturovanost, platnost De Jonghovy v ety a rozhodnutelnost. Diplomov a pr ace vych az zejm ena z v ysledk u C. Smorynsk eho a D. de Jongha a sna z se je rozvinout. N ekter e v ysledky zn am e pro Heytingovu aritmetiku dokazuje i pro jin e teorie. D ale se pokou s odpov ed et nap r klad na to, jak y vliv m a z am ena axiomu teorie za jin y (klasicky ekvivalentn ) axiom nebo jak e vlastnosti by m ela m t dobr a intuicionistick a teorie.
|
|
| |
|
|
Logika dokazatelnosti a její filozofická reflexe
Filippi, Jan ; Švejdar, Vítězslav (oponent) ; Jirků, Petr (vedoucí práce)
V matematické části je zpracováno téma autoreference v aritmetice. Při úvahách i důkazech je užit vyšší programovací jazyk, což umožňuje dospět ke známým výsledkům Gödela, Rossera a Löba přirozeným způsobem. V závěru je formulován další podobný problém a návrhy jeho řešení. Ve filozofické části jsou diskutovány paralely výsledků logiky dokazatelnosti v humanitních vědách. Je zkoumán rozpor mezi determinismem a existencí svobodné vůle a co k tomuto rozporu může říci teorie algoritmů.
|
|
|
Interpolation in modal logics
Bílková, Marta ; Pudlák, Pavel (vedoucí práce) ; Švejdar, Vítězslav (oponent) ; Iemhoff, Rosalie (oponent)
Since Craig's landmark result on interpolation for classical predicate logic, proved as the main technical lemma in [14], interpolation is considered one of the centra! concepts in pure logic. Various interpolation properties find their applications in computer science and have many deep purely logical consequences. We focus on two propositional versions of Craig interpolation property: Craig Interpolation Property: for every provable implication (A -+ B) there is an interpolant I containing only only common variables of A and B such that both implications (A -+ I) and (I-+ B) are provable. Craig interpolation, although it seems rather technical, is a deep logical property. It is dosely related to expressive power of a logic - as such it entails Beth's definability property, or forces functional completeness. It is also related to Robinson's joint consistency of two theories that agree on the common language. Craig interpolation has an important algebraic counterpart - it entails amalgamation or superamalgamation property of appropriate algebraic structures. In case of modal provability logics, Craig interpolation entails fixed point theorem. There are other interpolation properties, defined w.r.t. a consequence relation rather then w.r.t. a provable implication. In presence of deduction theorem the two...
|
|
|
Explicitní pevné body v logice dokazatelnosti
Chvalovský, Karel ; Bílková, Marta (oponent) ; Švejdar, Vítězslav (vedoucí práce)
Smyslem této diplomové práce je prozkoumat explicitní výpoty pevn ých bod v logice dokazatelnosti GL. Vta o pevných bodech zní: Pro kadou modální formuli A(p) v ní kadý výskyt atomu p je vázán modálním operátorem ¤, existuje formule D obsahující pouze výrokové atomy obsaené v A(p), neobsahující výrokový atom p, a taková, e v GL je dokazatelné D ' A(D). Formule D je navíc ur- ena a na dokazatelnou ekvivalenci jednoznan. Nejprve vyslovíme nkolik speciálních pípad vty o pevných bodech a poté podrobnji prozkoumáme vtu v plném znní. Dále ukáeme jednu sémantickou a dv syntaktické konstrukce pevných bod a dokáeme jejich korektnost. V práci se zabýváme také nkterými sloitostními aspekty konstrukce, pedevím uvádíme jednoduché horní odhady délky a modální sloitosti získaných pevných bod.
|
|
|
Relace bisimulace
Arazim, Pavel ; Švejdar, Vítězslav (oponent) ; Bílková, Marta (vedoucí práce)
Tato práce se zabývá relací bisimulace v modální logice a také v intuicionistické logice bez kontrakce. Bisimulace je relace mezi sémantickými modely, která je slabí neo isomor smus, ale přitom pořád zaruuje ekvivalenci v dané logice. Jejím typickým pouoitím jsou d·kazy nerozliitelnosti uritých typ· struktur jazykem dané logiky. Příkladem takové vlastnosti je kardinalita modálních model·, jejío nerozliitelnost ukazuje konstrukce disjunktního sjednocen í. Pro modální logiku má relace bisimulace velký význam jet také proto, oe objas ňuje její vztah ke klasické prvořádové logice. Krom bisimulace je zkoumán také souvisej ící pojem vázaného mor smu, který umooňuje převést výsledky o nede novatelnosti i na úroveň rámc·. ást o modální logice je předevím shrnutím obecn známých výsledk·, přiemo se snaoí objasnit jejich souvislosti, případn rozvést nkteré d·kazy, které se obvykle přecházejí jako zřejmé. U mén prozkoumané intuicionistické logiky bez kontrace spoívá znaná ást práce uo v samotné de nici její sémantiky a zajitní její funknosti. Také zde je ovem zavedena bisimulace i vázaný mor smus a na jejich konkrétních příkladech je naznaeno mooné vyuoití.
|
|
|
Některé sémantické metody v intuicionistické logice
Bergmannová, Pavla ; Švejdar, Vítězslav (vedoucí práce)
V práci se podíváme do světa intuicionistické logiky. Zjistíme že v intuicionistické logice nelze definovat logické spojky pomocí jiných logických spojek. Podíváme se, jak je to v intuicionistické logice s jednoatomovými formulemi, ukážeme, že je můžeme vyčerpávajícím způsobem zorganizovat. Také se budeme věnovat kripkovským modelům a uvidíme, že v některých případech lze vydatně zredukovat nosnou množinu kripkovského modelu. Předložíme nástroje, pomocí kterých poznáme, které prvky jsou v modelu jaksi "navíc" a tudíž je můžeme z modelu "vyškrtnout". Na závěr se soustředíme na jednoatomové modely a na to, jak to vypadá s jejich složitostí, když je maximálně redukujeme. V práci je využito toho, že lze písmem rozlišit dvě implikace ---+ a ~- První z nich je používána jako implikace v rámci diskutovaných formulí, druhá jako prvek metajazyka, kterým si povídáme o této problematice. Při důkazech tvrzení o intuicionistické logice se řídíme pravidly klasické logiky. Písmena A, B, C, ... a z, cp, lf/, . . . představují formule, písmena p, q představují atomy.
|
|
|
Nerozhodnutelnost struktury racionálních čísel
Jurenka, David ; Krajíček, Jan (oponent) ; Švejdar, Vítězslav (vedoucí práce)
Otázka rozhodnutelnosti, tj. otázka, zda existuje algoritmus, který by byl schopen rozhodnout o platnosti každé prvořádové predikátové formule, se dostala na výsluní pozornosti matematiků ve dvacátých letech minulého století. Spolu s ní byla zkoumána i rozhodnutelnost druhořádových formulí a obecně jakéhokoli matematického tvrzení. Souhrnně byly tyto otázky označovány jako Hilbertův Entscheidungsproblem a ještě roku 1930 Hilbert věřil v jejich kladné řešení. Roku 1936 však Alonzo Church ukázal, že samotná predikátová logika prvního řádu je nerozhodnutelná, a téhož roku pak Alan Turing představil dnes již klasický nerozhodnutelný problém, problém zastavení. Oba při tom ve svých pracech využili myšlenek, které formuloval Kurt Godel ve svém důkazu neúplnosti aritmetiky. V otázce rozhodnutelnosti základních aritmetických struktur přinesl první významný výsledek Mojzesz Presburger, který roku 1929 dokázal rozhodnutelnost přirozených čísel s operací sčítání a konstantami O a 1. Nicméně hned následujícího roku vyplynulo z Godelových výsledků, že tatáž struktura včetně operace násobení již rozhodnutelná být nemůže. Tím byla zároveň vyřešena i otázka rozhodnutelnosti čísel celých, neboť pojem přirozeného čísla je v této struktuře definovatelný (viz kapitolu 4.2), a tak je možno v celých číslech reformulovat každou...
|
|
|
Nerozhodnutelnost struktury racionálních čísel
Jurenka, David ; Švejdar, Vítězslav (vedoucí práce) ; Krajíček, Jan (oponent)
Otázka rozhodnutelnosti, tj. otázka, zda existuje algoritmus, který by byl schopen rozhodnout o platnosti každé prvořádové predikátové formule, se dostala na výsluní pozornosti matematiků ve dvacátých letech minulého století. Spolu s ní byla zkoumána i rozhodnutelnost druhořádových formulí a obecně jakéhokoli matematického tvrzení. Souhrnně byly tyto otázky označovány jako Hilbertův Entscheidungsproblem a ještě roku 1930 Hilbert věřil v jejich kladné řešení. Roku 1936 však Alonzo Church ukázal, že samotná predikátová logika prvního řádu je nerozhodnutelná, a téhož roku pak Alan Turing představil dnes již klasický nerozhodnutelný problém, problém zastavení. Oba při tom ve svých pracech využili myšlenek, které formuloval Kurt Godel ve svém důkazu neúplnosti aritmetiky. V otázce rozhodnutelnosti základních aritmetických struktur přinesl první významný výsledek Mojzesz Presburger, který roku 1929 dokázal rozhodnutelnost přirozených čísel s operací sčítání a konstantami O a 1. Nicméně hned následujícího roku vyplynulo z Godelových výsledků, že tatáž struktura včetně operace násobení již rozhodnutelná být nemůže. Tím byla zároveň vyřešena i otázka rozhodnutelnosti čísel celých, neboť pojem přirozeného čísla je v této struktuře definovatelný (viz kapitolu 4.2), a tak je možno v celých číslech reformulovat každou...
|
host ::
RSS.