|
| |
|
|
Arithmetical completeness of the logic R
Holík, Lukáš ; Švejdar, Vítězslav (advisor) ; Bílková, Marta (referee)
The aim of this work is to use contemporary notation to build theory of Rosser logic, explain in detail its relation to Peano arithmetic, show its Kripke semantics and finally using plural self-reference show the proof of arithmetical completeness. In the last chapter we show some of the properties of Rosser sentences. Powered by TCPDF (www.tcpdf.org)
|
|
|
Aspects of the Cut-Elimination Theorem
Rýdl, Jiří ; Švejdar, Vítězslav (advisor) ; Bílková, Marta (referee)
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].
|
|
|
The undecidability of the field of rationals
Jurenka, David ; Švejdar, Vítězslav (advisor) ; Krajíček, Jan (referee)
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...
|
|
|
Some semantic methods in intuitionistic logic
Bergmannová, Pavla ; Švejdar, Vítězslav (advisor)
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.
|
|
|
Machine-Free Characterization of Polynomially Computable Functions
Profeld, Michal ; Švejdar, Vítězslav (advisor) ; Verner, Jonathan (referee)
This thesis focuses on machine-free definition of polynomial functions. The main goal is to not only make the readers familiar with this de- finition, but also to introduce them to the other pivotal terms of this thesis. The other pivotal terms are: basic functions, function composi- tion, recursive schemes a polynomial conditions. Throughout the thesis the readers will be introduced, among other things, to derivation of the most used polynomially bounded functions, like multiplication, addi- tion, or other arithmetic functions. 1
|
|
|
Machine-Free Characterization of Polynomially Computable Functions
Profeld, Michal ; Švejdar, Vítězslav (advisor) ; Verner, Jonathan (referee)
This work is focused into constructing mathematical structure. This structure is closed under it's operations. Structure was developed to contain all functions of certain growth rate. To be More specific functi- ons with polynomial growth rate. We can say that our structure con- tains all functions that have growth rate slower or equal to polynomial growth rate and no other function. Development of our structure was influenced mostly by work of Samuel R. Buss [1] 1
|
|
|
Arithmetical completeness of the logic R
Holík, Lukáš ; Švejdar, Vítězslav (advisor) ; Bílková, Marta (referee)
The aim of this work is to use contemporary notation to build theory of Rosser logic, explain in detail its relation to Peano arithmetic, show its Kripke semantics and finally using plural self-reference show the proof of arithmetical completeness. In the last chapter we show some of the properties of Rosser sentences. Powered by TCPDF (www.tcpdf.org)
|
|
|
Probabilistic algorithms for testing primality
Tejkalová, Natálie ; Švejdar, Vítězslav (advisor) ; Glivický, Petr (referee)
Attention has been paid mostly to the new deterministic algorithm for primality testing AKS recently. However, probabilistic algorithms remain an efficient tool for primality testing. Our thesis focuses mostly on two most well-known probabilistic algorithms for primality testing. It describes the main idea and gives proofs of correctness of Solovay-Strassen and Rabin-Miller algorithms. Apart from that, it also tries to look at the subject of probabilistic algorithms from a wider perspective. It presents a definition of a probabilistic algorithm and various complexity classes that correspond to Monte Carlo or Las Vegas algorithms. Besides pure mathematical theory, we mention also some philosophical aspects that need to be considered when we decide to use the probabilistic method. Powered by TCPDF (www.tcpdf.org)
|
|
|
Implicational fragments of intuitionistic propositional logic
Blicha, Martin ; Švejdar, Vítězslav (advisor) ; Chvalovský, Karel (referee)
In this thesis we study implicational fragments of intuitionistic propositional logic with finite number of atoms. The first part is dedicated to the fragment with only two atoms, which is simple enough to analyze the relations between it's formulas, but is not that trivial. In the next part, we introduce the terms prime node and prime model, which allow us to examine other fragments. In the last part, we find out how the results change when we add the constant into out language.
|
guest ::
