Introduction

About me

Associate professor at the Department of Logic, College of Arts ("Faculty of Arts"), Charles University in PragueFilozofická fakulta UK, Palachovo nám. 2, 11638 Praha 1. Courses Computability (an introduction to recursive functions), Classical Logic II (with an emphasis on incompleteness and undecidability), and some others related to metamathematics or to algorithms.

Research interests

Interpretability of axiomatic theories, arithmetization, related modal logics, algorithmic aspects of non-classical logics.

Experience and education

During 1982-90 worked as a software developer for an industrial company ČKD Polovodiče. Participation in writing a control system for PDP-11 computers. The system was designed by Jan Pavelka*⁾Accidentally the same Jan Pavelka who, a few years before turning into a respected software developer, wrote innovative papers about fuzzy logics., and was successfully applied in several branches of industry like steel rolling or international transport of natural gas.

Ph.D. in mathematical logic, Ph.D. study in the Institute of Mathematics of the Academy of Sciences of the Czech Republic. Dissertation Self-Reference and Modal Logic, 1982, supervisor Petr Hájek. Graduated in mathematics from Charles University, 1978, master's thesis Degrees of Interpretability.

Office info, events, miscellaneous updates

Office hours Thu 15:00, or by appointment. For more info please see the image above, or the web of the department.

Nabídka témat bakalářských a diplomových prací: TemataPraci13.pdf

Publications

BibTeX file

BibTeX entries can be taken from sv.bib. Note that the file contains a preamble with some strings and macros.

Book

Logika: neúplnost, složitost a nutnost (Logic: Incompleteness, Complexity, and Necessity), Academia Praha, 2002. 464 pages, section 5.2 about Gödel-Dummett fuzzy logic was written by Petr Hájek. See the "Book" tab above.

Some workshop or conference presentations

Logika, Gödel, neúplnost (Logic, Gödel, Incompleteness). A talk at Friday meetings of Sysifos, February 23th, 2018. A videorecord created by Ludvík Hájek is available on YouTube.
Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and Incompleteness). A talk at Hvězdárna and planetárium Brno (Brno Observatory and Planetarium), March 9th, 2017. A videorecord created by Josef Forman is available on YouTube.
Rosser Sentences and Rosser Logics. A talk at the Prague gathering of logicians, Jan 2017.
On Purely implicational Fragments of Intuitionistic Propositional Logic. A talk at the Logica '11 International Conference, Hejnice, Czech Republic, June 2011. [pdf4]

Papers

Do We Need Recursion? In I. Sedlár and M. Blicha, eds., The Logica Yearbook 2019, pp. 193–204. College Publications, London, 2020. [pdf][talk]
Modern Czech Logic: Vopěnka and Hájek, History and Background. Journal of Applied Logics — IfCoLoG Journal of Logics and their Applications, 5(6):1261–1271, 2018. [pdf]
Předmluva: o logice 20. století (Preface: On the 20th Century Logic). In L. Dostálová, ed., Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and Incompleteness), pp. 13–53. OPS in collaboration with University of West Bohemia Publishing, Plzeň, 2015. ISBN 978-80-87269-39-8. In Czech. [pdf]
On Strong Fragments of Peano Arithmetic. In P. Arazim and M. Dančák, eds., The Logica Yearbook 2014, pp. 281–291. College Publications, London, 2015. [pdf][talk]
Výuka logiky bez logických pojmů (Teaching logic without the use of logical notions). In L. Dostálová and K. Šebela, eds., Organon VII — Nihil novi, pp. 49–57. University of West Bohemia Publishing, Plzeň, 2011. ISBN 978-80-261-0035-5. In Czech. [pdf][pdf2]
Infinite natural numbers: an unwanted phenomenon, or a useful concept? In M. Peliš and V. Punčochář, eds., The Logica Yearbook 2010, pp. 283–294. College Publications, London, 2011. [pdf][pdf2][talk]
Decision Problems of Some Intermediate Logics and Their Fragments. In M. Peliš, ed., The Logica Yearbook 2009, pp. 297–307. College Publications, London, 2010. [pdf][pdf2][talk]
Relatives of Robinson Arithmetic. In M. Peliš, ed., The Logica Yearbook 2008, pp. 253–263. College Publications, London, 2009. [pdf][pdf2][talk]
On Interpretability in the Theory of Concatenation. Notre Dame Journal of Formal Logic, 50(1):87–95, 2009. [pdf][pdf2]
Weak Theories and Essential Incompleteness. In M. Peliš, ed., The Logica Yearbook 2007, pp. 213–224. Filosofia, Praha, 2008. [pdf][pdf2][talk]
An Interpretation of Robinson Arithmetic in its Grzegorczyk's Weaker Variant. Fundamenta Informaticae, 81(1–3):347–354, 2007. [pdf][pdf2]
Gödel-Dummett Predicate Logics and Axioms of Prenexability. In O. Tomala and R. Honzík, eds., The Logica Yearbook 2006, pp. 251–260. Filosofia, Praha, 2007. [pdf][pdf2][talk]
On Modal Systems with Rosser Modalities. In M. Bílková and O. Tomala, eds., The Logica Yearbook 2005, pp. 203–214. Filosofia, Praha, 2006. [pdf][pdf2][talk]
On Sequent Calculi for Intuitionistic Propositional Logic. Comm. Math. Univ. Carolinae, 47(1):159–173, 2006. [pdf][pdf2]
With Blanka Kozlíkova, On Interplay of Quantifiers in Gödel-Dummett Fuzzy Logics. Archive for Math. Logic, 45(5):569–580, 2006. [pdf][pdf2]
Note on Inter-Expressibility of Logical Connectives in Finitely-Valued Gödel-Dummett Logics. Soft Computing, 10(7):629–630, 2006. [pdf][pdf2]
Gödlov prvi izrek o nepolnosti. Obzornik za matematiko in fyziko, 51(4):113–121, 2004.
The limit lemma in fragments of arithmetic. Comm. Math. Univ. Carolinae, 44(3):565–568, 2003. [pdf][pdf2]
A note on arithmetical completeness of theories with Rosser modalities. In K. Bendová and P. Jirků, eds., Miscellanea logica V, pp. 123–132. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
On structural proofs of Gödel First Incompleteness Theorem. In K. Bendová and P. Jirků, eds., Miscellanea logica V, pp. 115–122. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
The decision problem of provability logic with only one atom. Archive for Math. Logic, 42(8):763–768, 2003. Errata: The final paragraph, just before the list of references, contains an unpleasant misprint: 'added in January 2002', should be 'added in January 2003'. My apologies! [pdf][pdf2]
On the polynomial-space completeness of intuitionistic propositional logic. Archive for Math. Logic, 42(7):711–716, 2003. [pdf][pdf2]
With K. Bendová, On Inter-Expressibility of Logical Connectives in Gödel Fuzzy Logic. Soft Computing, 4(2):103–105, 2000. [pdf][pdf2]
On Provability Logic. Nordic Journal of Philosophical Logic, 4(2):95–116, 2000. [pdf][pdf2]
Arithmetical Classification of the Set of All Provably Recursive Functions. Comm. Math. Univ. Carolinae, 40(4):631–634, 1999. [pdf][pdf2]
Poznamka o vztahu vyplyvani v klasicke predikatove logice (A Note on the Consequence Relation in Classical Predicate Logic). In P. Jirků and V. Švejdar, eds., Miscellanea Logica II. Karolinum, Praha, 1999. In Czech.
Logika v aritmetice. In P. Jirků and V. Švejdar, eds., Miscellanea Logica I. Karolinum, Praha, 1998. In Czech.
With P. Hájek, Matematicka logika (Mathematical Logic). Praha, November 1994. Lecture notes, electronic version only, in Czech.
Some Independence Results in Interpretability Logic. Studia Logica, 50(1):29–38, 1991.
With P. Hájek, A Note on the Normal Form of Closed Formulas of Interpretability Logic. Studia Logica, 50(1):25–28, 1991.
Modal Analysis of Generalized Rosser Sentences. J. Symb. Logic, 48(4):986–999, 1983. [JSTOR]
A Sentence that is Difficult to Interpret. Comm. Math. Univ. Carolinae, 22(4):661–666, 1981.
Degrees of Interpretability. Comm. Math. Univ. Carolinae, 19(4):789–813, 1978.

Logic: Incompleteness, Complexity, and Necessity (Academia, 2002)

I do not think logic is a field where people are taught how to think logically. Instead, I consider it a theory about deductive thinking for people who already are able to think logically, usually because they have some experience with academic mathematics.

My ambition was to have more than a list of definitions, theorems, and proofs; I am trying to include comments and explanations, and I believe that the reader should be led from some questions to some solutions.

I am grateful to Petr Hájek, who was my teacher and who gave one of the initial impulses for writing this book. He actually wrote only a small part of the text, but much larger part and perhaps everything was inspired by him.

As a result of an agreement with the Academia publishing company, a pdf version of the book is now available (full text!) for study purposes (only!). When downloading the file, it is recommended to download also Errata and save both files to the same folder on local computer. That will activate the links in the text marked by big red 'E'. Redistribution and modifications of the file are not allowed! Printing of (any part of) the document is not allowed!

Po domluvě s nakladatelstvím Academia je nyní plný text knihy ve formátu pdf přístupný pro studium (pouze!). Při kopírování souboru na lokální počítač je doporučeno stáhnout také Errata a umístit oba soubory do téže složky. Soubor nesmí být dále šířen ani nesmí být modifikován! Žádná jeho část nesmí být tištěna!

Click on the blue word 'Academia' on the first page of the book to obtain further information about their bookstores and other books they publish.

Comments and additions to Errata are welcome.

Modal and non-classical logics

SIS ALG119008, Zoom cuni-cz.zoom.us/j/99702828164.

Exams

Please prepare answers/explanations to the following list of topics.

Course contents in Fall 2020/21 (Czech)

7. ledna 2021: Standardní překlad modální logiky do klasické predikátové logiky. Věta o úplnosti a rozhodovací procedura pro logiku GL.
Cvičení. Standardní překlad prosím konfrontujte s (opravte dle) toho, co píše van Benthem v úvodní kapitole ke knize Handbook of Modal Logics.
17. prosince 2020: Věta o úplnosti a rozhodovací procedura pro logiku K. Věta o eliminovatelnosti řezů, finite model property. Odvozená pravidla □A / A a □A→A / A (Löbovo pravidlo LR).
Cvičení. Je-li A libovolná formula a označíme-li B formuli □(□A→A)→□A, pak v logice K4 lze dokázat formuli □B→B. Takže logiku GL lze také axiomatizovat přidáním pravidla LR k logice K4.
10. prosince 2020: Gentzenovský kalkulus pro logiku K a důkaz jeho úplnosti.
3. prosince 2020: Varianty axiomatizace logiky GL: z L lze dokázat schéma 4, z H a 4 lze dokázat L. Gentzenovský kalkulus pro klasickou výrokovou logiku. Varianty pravidel.
26. listopadu 2020: Bisimulační kontrakce modelu. Cresswellův model demonstrující, že schémata H a L nejsou ekvivalentní.
19. listopadu 2020: Bisimulace, podmodely a disjunktní sjednocení modelů (rámců). Příklady tříd rámců, které nejsou charakterizovatelné: nereflexivní rámce, antireflexivní rámce, rámce 〈W,R〉, kde R = W², a antisymetrické rámce.
Cvičení. Uvažujte modely M a N z přednášky (v M je cyklus z r do s a zpět a navíc r vidí t a s vidí u, kdežto v N je obdobný cyklus z c do d a zpět a dvě další šipky do e a do f, ale obě začínají v d). Najděte formuli neobsahující atomy, která platí jen v jednom z těchto modelů.
12. listopadu 2020: Přehled charakteristických tříd různých logik. Modely a rámce generované prvkem.
Cvičení. Domyslete důkaz tvrzení, že "schéma 5", čili schéma ◇A→□◇A, charakterizuje eukleidovskost.
5. listopadu 2020: Charakteristické třídy logik K4, T, B, H a L.
Cvičení. Nalezněte logiku, která charakterizuje eukleidovskost. Domyslete úvahu týkající se charakterizace lokálně silně souvislé relace.
29. října 2020: Logiky T a K4. Charakteristické třídy logik.
Cvičení (formulace upravena 31.10.). Domyslete tvrzení, že logika K + ◇A→◇◇A charakterizuje hustotu (relace dosažitelnosti). Najděte logiku, která charakterizuje symetrii.
22. října 2020: Schéma K a hilbertovský kalkulus pro logiku K. Věta o korektnosti této logiky vůči kripkovské sémantice.
Cvičení. S využitím tautologií a tautologických důsledků zdůvodněte, že všechny instance schématu □A & □B → □(A & B) jsou v hilbertovském kalkulu pro logiku K dokazatelné. Formule □p → □□p ale dokazatelná není.
15. října 2020: Ještě kripkovská sémantika.
Cvičení. Uvažujte rámec 〈W,R〉, kde W = {a,b,c} a R = {[a,b],[b,c],[c,c]}. Takže a vidí pouze b, kdežto b a c vidí c a nic jiného. Atom p je splněn v b a v c, ale ne v a, ostatní atomy jsou všude nesplněny. Dokažte, že b a c nelze odlišit žádnou modální formulí, tj. že každá modální formule, která je splněna v b, je splněna i v c.
8. října 2020: Věta o kompaktnosti v klasické výrokové logice. Kripkovské rámce a kripkovské modely pro modální výrokovou logiku.
Domácí cvičení. Uvažujte rámec se čtyřmi vrcholy 1, 2, 3 a 4, v němž z 1 jsou dosažitelné vrcholy 3 a 4, z 2 je dosažitelný 1, z 4 jsou dosažitelné 4 a 2. Atom p je splněn ve vrcholech 1 a 2. Ve kterých vrcholech je splněna formule ◇□◇p?
1. října 2020: Opakování klasické výrokové logiky: logické spojky, tautologie, ekvivalentní formule, důsledek.
Domácí cvičení. Promyslete následující variantu Příkladu 1.1.7 v knize [Šv02]. Nechť množina Γ výrokových formulí je definována jako { p_i → p_i+1 ; i ∈ N }. Které z formulí tvaru p_i → p_j jsou logickým důsledkem (vyplývají) z množiny Γ? Je pravda, že ta, která vyplývá, vyplývá i z některé konečné podmnožiny množiny Γ? Z které?

Properties of axiomatic theories

SIS ALG119006, Zoom.

Excercises

Please pay attention to the list of excercises.

Exams

Ke zkoušce si prosím připravte seznam dvaceti cvičení, která dovedete řešit. Cvičení 23 (zejména jeho druhá část) zůstalo za obzorem kursu.

Course contents in Fall 2021/22 (Czech)

6. ledna 2022: Věta o Σ-úplnosti Robinsonovy aritmetiky. První Gödelova věta o neúplnosti a její strukturální důkaz.
4. ledna 2022: Každá Δ₀-sentence je v Q dokazatelná nebo vyvratitelná. Definice Σ-formule.
21. prosince 2021: Věta o dokazatelnosti v Q. Každá otevřená sentence je v Q dokazatelná nebo vyvratitelná, a to nutně v souladu s tím, jestli platí nebo neplatí ve struktuře ℕ.
16. prosince 2021: Robinsonova aritmetika Q. Její jednoduchý model se dvěma nestandardními prvky, který ukazuje, že běžná tvrzení o vlastnostech operací a uspořádání v Q dokazatelná většinou nejsou.
14. prosince 2021: Σ₁-formule a Π₁-formule. Všechny množiny definovatelné Σ₁-formulí jsou RE. Všechny množiny, které jsou definovatelné Σ₁-formulí a současně (jinou) Π₁-formulí, jsou rekurzívní. Libovolná RE úloha (v čemž jsou i některé nerekurzívní) je převeditelná na množinu Th(ℕ). Z toho plyne, že Th(ℕ) není rekurzívní. Varianta První Gödelovy věty o neúplnosti: když T je rekurzívně axiomatizovatelná teorie v aritmetickém jazyce taková, že struktura ℕ je jejím modelem, pak T je neúplná.
9. prosince 2021: Užití eliminace kvantifikátorů k charakterizaci množin definovatelných v některých strukturách. Omezené aritmetické formule (Δ₀-formule). Příklady množin a relací definovatelných Δ₀-formulemi: množina všech prvočísel, relace m = Mod(n,k) a m = Div(n,k), množina všech mocnin dvojky. Náznak důkazu, že i relace m = n^k je Δ₀-definovatelná.
Domácí úkol: cvičení 24 teď definitivně.
7. prosince 2021: Halting Problem je RE množina, jejíž komplement není RE (dokončení důkazu). Je to tedy nerekurzívní RE množina. Je také jasné, že RE množiny nejsou uzavřeny na komplement. Definovatelné množiny a definovatelné prvky struktur. Příklady.
Domácí úkol: cvičení 24.
2. prosince 2021: Úplná rekurzívně axiomatizovatelná teorie je rozhodnutelná. Konečná struktura pro konečný jazyk je rozhodnutelná. Konečné rozšíření rozhodnutelné teorie je rozhodnutelné. Komplement úlohy Halting Problem není RE (jen část důkazu).
30. listopadu 2021: Rekurzívní a RE úlohy (množiny). Rozhodnutelné, konečně axiomatizovatelné a rekurzívně axiomatizovatelné teorie. Důležité příklady RE množin: množina Thm(T), pokud je T rekurzívně axiomatizovatelná, nebo Problém zastavení.
25. listopadu 2021: Algoritmy a úlohy. Výpočtové modely. Churchova teze. Příklady rekurzívních úloh.
23. listopadu 2021: Eliminace kvantifikátorů pro teorii DOS, dokončení. Historické příklady na eliminaci kvantifikátorů: Presburgerův výsledek týkající se struktury přirozených čísel bez násobení, Tarského výsledek týkající se struktury ℝ (struktury reálných čísel).
18. listopadu 2021: Postačující podmínka pro konzervativnost rozšíření. Eliminace kvantifikátorů pro teorii DOS (skoro všechny kroky).
16. listopadu 2021: Eliminace kvantifikátorů pro teorii SUCC, dokončení. Teorie DOS. Rozšíření a konzervativní rozšíření teorie.
Domácí úkol: oficiálně nezadán (snad jen připomínám poslední část cvičení 14: teorie SUCC není konečně axiomatizovatelná). Relevantní by také mohlo být toto: navrhněte axiomatizaci pro strukturu <R,+,0,1>.
11. listopadu 2021: Eliminace kvantifikátorů pro teorii SUCC.
9. listopadu 2021: Teorie LO, DO, DNO a SUCC. Jejich modely. Teorie DNO je ℵ₀-kategorická. Vaughtův test: bezesporná teorie s nejvýše spočetným jazykem, která nemá konečné modely a je ℵ₀-kategorická, je úplná.
Domácí úkol: k problematice Vaughtova testu se vztahují cvičení 13 a 14.
4. listopadu 2021: Třída všech silně souvislých orientovaných grafů není axiomatizovatelná. Silnější verze Löwenheimovy-Skolemovy věty: každá teorie T s jazykem L, která má nekonečné modely, má i modely všech mohutností κ ≥ ∣L∣ + ℵ₀. Pokusy axiomatizovat konkrétní struktury. Teorie DO.
Domácí úkol: Cvičení 15 a 16 teď už definitivně.
2. listopadu 2021: Třída všech konečných struktur pro (libovolný) jazyk L není axiomatizovatelná. Třída všech dobře uspořádaných množin také ne. Třída všech struktur pro prázdný jazyk, které jsou nekonečné, axiomatizovatelná je, ale není konečně axiomatizovatelná.
Domácí úkol: Cvičení 15 a 16 (přičemž 16 bude aktuální až po čtvrtku). Tentokrát prosím o písemné řešení (zaslané mailem do 8.11.) jednoho z těchto cvičení. V řešení respektujte to, že věta o kompaktnosti je sématnické tvrzení, a vyhněte se syntaktickým pojmům (dokazatelnost, bezespornost).
26. října 2021: Rozdíl mezi úplností a silnou úplností, věta o kompaktnosti, slabá verze Löwenheimovy-Skolemovy věty. Axiomatizovatelné (neboli elementární) a konečně axiomatizovatelné třídy struktur pro daný jazyk.
Domácí úkol oficiálně nezadán, ale ten minulý (cvičení 10 a 11) je stále aktuální.
19. a 21. října 2021: Logicky platné formule. Prominentní struktury: ℝ, ℚ, ℤ a ℕ. Věta o silné úplnosti a některé její souvislosti.
Domácí úkol: cvičení 10 a 11.
14. října 2021: Ohodnocení proměnných, Tarského definice. Korektnost pravidel generalizace. Definice vyplývání.
Domácí úkol: cvičení 4 (řešitelná jsou 1 až 10).
12. října 2021: Věta o korektnosti. Struktury, platnost formule ve struktuře.
Domácí úkol: cvičení 9 v seznamu nahoře.
7. října 2021: Množiny Thm() a Ref() nějaké axiomatické teorie. Sporné a bezesporné teorie. Věta o dedukci.
5. října 2021: Hilbertovské logické kalkuly. Volné a vázané výskyty proměnných, generalizace, substituovatelné termy, axiomy specifikace. Tautologie v predikátové logice s rovností. Neformální důkazy.

Arithmetics and algorithms

Please pay attention to the list of excercises. It (may extend and) will be used during the exam.

SIS ALG110008, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení třinácti cvičení (i s vysvětlením matematického či algoritmického pozadí). Zkouška pak pokračuje prodiskutováním některého důkazu. Letos lze průběh zkoušky domluvit i individuálně, ale na prodiskutování některého důkazu, třeba i předem domluveného, by dojít mělo. Termín zkoušky lze domluvit mailem, preferuji Út celkem kdykoliv, Po a St navečer a Pá ráno.

Course contents in Spring 2021/22 (Czech)

17. května 2022: Číslo 2⁶¹ - 1 je prvočíslo. Postup lze zobecnit na zdůvodnění, že Primes je úloha ve třídě NP.
10. května 2022: Úlohy ve třídě NP. Mersennova čísla a Mersennova prvočísla. Řády prvků v grupách obecně a v Eulerových grupách zvláště.
3. května 2022: Výpočet hodnoty Eulerovy funkce: stačí vědět pouze seznam prvočísel v rozkladu daného čísla, bez jejich exponentů se lze obejít. Příklady na užití modulárních reprezentací a Eulerovy věty. Jeden reálný příklad: kryptografická metoda RSA.
26. dubna 2022: Eulerova (Fermatova) věta: v každé konečné komutativní grupě s n prvky platí ∀x(xⁿ = 1).
19. dubna 2022: Ekvivalentní podmínka pro nesoudělnost: nenulová čísla a a b jsou nesoudělná, právě když ∀z(a ∣ bz → a ∣ z). Modulární reprezentace a Čínská zbytková věta. Užití modulárních reprezentací k důkazu, že číslo 341 je pseudoprvočíslo.
12. dubna 2022: Teoreticko-informatický důsledek čtyřsloupcového algoritmu: o invertibilitě v ℤ_m lze rozhodnout a inverzní prvek invertibilního prvku lze nalézt v polynomiálním čase. K tomu patří dodatek, že pro x∈ℤ_m a přirozené číslo k lze mocninu x^k také nalézt v polynomiálním čase. Matematický důsledek Bézoutovy věty: v ℤ platí, že každé ireducibilní číslo je prvočíslo.
5. dubna 2022: Zobecněný (čtyřsloupcový) Eukleidův algoritmus.
29. března 2022: Ještě tělesa a obory integrity. A ještě jednou základní pojmy dělitelnosti: nesoudělnost, ireducibilní prvky, prvočísla.
Cvičení. Dokažte, že každé prvočíslo je ireducibilní.
22. března 2022: Opakování: modulární aritmetika, inverzní a opačné prvky v okruzích. Tělesa a obory integrity. Rozdíl mezi logickými principy a axiomy teorie.
15. března 2022: Vlastnosti opačných prvků v okruzích. Modulární aritmetika. Invertibilní prvky v různých okruzích (podrobně byla z tohoto hlediska prozkoumána struktura ℤ_m). Tělesa. Obor integrity jako struktura vhodná pro zkoumání dělitelnosti. Základní pojmy teorie dělitelnosti: asociované prvky, nesoudělnost, největší společný dělitel, ireducibilní prvky, prvočísla. Například x a y jsou podle definice nesoudělná, jestliže každý jejich společný dělitel je invertibilní (čili je dělitelem jedničky).
8. března 2022: Eukleidův algoritmus pracuje v polynomiálním čase. Definice komutativního okruhu a bezprostřední důsledky axiomů. Opačné a inverzní prvky.
1. března 2022: Úlohy Primes a Factoring. Pojem polynomiálního algoritmu. Eukleidův algoritmus a jeho matematický důsledek: pro každá dvě přirozená čísla existuje jejich společný dělitel, který je dělitelný všemi jejich společnými děliteli.
22. února 2022: Úlohy a algoritmy. Školní algoritmus pro úlohu Násobení neboli Mult. Jeho časové nároky. Dva algoritmy pro určování, zda dané číslo je prvočíslo. Oba bohužel, a to na rozdíl od školního algoritmu pro násobení, pracují v exponenciálním čase.

Huge number calculator

The calculator BNCalc.pdf is implemented as a (set of scripts behind a) pdf document and can be used for operating with really huge integers. Note that there are some undocumented key combinations that make it easier to repeat the given operation. The "result" text field in the "Factoring" page, marked by an arrow in this image, accepts Shift‑M (or Shift‑B with the same meaning). Also, the result text field on the preceding page accepts Shift‑M and Shift‑B.

Incompleteness and Gödel Theorems

Here is an (updated May 24th) list of excercises.

SIS ALG119007, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení čtrnácti cvičení. Termín zkoušky nebo konzultace lze domluvit individuálně mailem, preferuji Út celkem kdykoliv, Po a St navečer a Pá ráno.

Course contents in Spring 2021/22

19. května 2022: Tři prenexní implikace, které nejsou intuicionisticky logicky platné. Jedna z nich, týkající se disjunkce a univerzálního kvantifikátoru, ale platí ve všech strukturách s konstantním univerzem. Schéma DNS ukazuje, že finite model property pro intuicionistickou predikátovou logiku neplatí. Predikátová varianta kalkulu GJ.
17. května 2022: Korektnost kvantifikátorových pravidel kalkulu GK, dokončení. Kripkovská sémantika intuicionistické predikátové logiky.
12. května 2022: Příklady důkazů v predikátové verzi kalkulu GK. Korektnost kvantifikátorových pravidel.
10. května 2022: Glivenkova věta. Kvantifikátorová pravidla kalkulu GK.
5. května 2022: Úplnost kalkulu GJ vůči kripkovské výrokové sémantice. Dva důležité vedlejší produkty důkazu: pro výrokovou variantu kalkulu GJ platí věta o eliminovatelnosti řezů, a výroková kripkovská sémantika má finite model property: každá formule, která má jakýkoliv kripkovský protipříklad, má i konečný protipříklad.
3. května 2022: Kalkulus GJ pro intuicionistickou výrokovou logiku. Příklady důkazů. Bezřezové důkazy. Vlastnost podformulí (subformula property): každá formule v bezřezovém důkazu je podformulí některé formule ve finálním sekventu.
28. dubna 2022: Intuicionistické tautologie, protipříklady. Inkluze IntTaut ⊆ Taut. Dvě modelové konstrukce: podmodel generovaný prvkem a amalgamace. Disjunction property.
26. dubna 2022: Kripkovská sémantika intuicionistické logiky.
21. dubna 2022: Korektnost a úplnost gentzenovského kalkulu GK vůči sémantice klasické výrokové logiky. Vlastnost podformulí (subformula property), věta o eliminovatelnosti řezů.
19. dubna 2022: Příklad definice τ(z) množiny axiomů Peanovy aritmetiky takové, že z ní vytvořená sentence Con(τ) je v PA dokazatelná. Pravidla gentzenovského výrokového kalkulu.
14. dubna 2022: Rosserova věta. Craigův trik. Podstatná neúplnost neboli podstatná nerozhodnutelnost Robinsonovy aritmetiky.
12. dubna 2022: Některé souvislosti Druhé Gödelovy věty. Hilbertův program.
7. dubna 2022: Klasický důkaz První Gödelovy věty (založený na větě o autoreferenci). Druhá Gödelova věta.
Cvičení. Dokažte, že Gödelova sentence ν sestrojená k teorii T a její Σ-definici τ je T-ekvivalentní se sentencí Con(τ).
5. dubna 2022: Věta o autoreferenci.
31. března 2022: Vlastnosti formalizované dokazatelnosti dokazatelné v PA. Formalizace konečně axiomatizovatelných teorií, například Robinsonovy aritmetiky. Formule π(z) formalizující v PA axiomatiku PA. Podmínky pro dokazatelnost (Löb's derivability conditions).
29. března 2022: Formalizace syntaktických pojmů v PA: od proměnných a termů k dokazatelnosti a bezespornosti. Aritmetizace logické syntaxe. Textové řetězce, operace s nimi, vyvážené řetězce, proměnné, termy.
24. března 2022: Aritmetizace logické syntaxe. Textové řetězce, operace s nimi, vyvážené řetězce, proměnné, termy.
22. března 2022: Množina všech rekurzívních funkcí je uzavřena na operaci primitivní rekurze: dokončení a shrnutí. Dvě důležité funkce, totiž [x,z] ↦ z^x a x ↦ "počet jedniček v binární expanzi čísla x" mají dokonce Δ₀-definovatelný graf. Jejich vlastnosti, například z^x+y = z^x·z^y, jsou dokazatelné v PA.
15. března 2022: Bezestrojová (čistě logická) definice RE množin, rekurzívních množin a rekurzívních funkcí.
10. března 2022: Struktura nestandardního modelu PA. Aritmetická hierarchie. Množiny Σ_m(PA) a Π_m(PA) jsou uzavřeny na konjunkci, disjunkci a omezenou kvantifikaci. Navíc Σ_m(PA) je uzavřena na ∃, Π_m(PA) je uzavřena na ∀. Každá aritmetická formule je ekvivalentní s nějakou Σ_m-formulí (tím ovšem i s nějakou Π_m-formulí).
8. března 2022: V PA lze dokázat, že prvočísla jsou přesně ta čísla, která jsou ireducibilní. Dále lze dokázat vlastnosti mocnin dvojky: dělitel mocniny dvojky je opět mocnina dvojky, součin dvou mocnin dvojky je mocnina dvojky, pro každé dvě mocniny dvojky platí, že některá z nich je dělitelem druhé, a když s je mocnina dvojky, pak mezi s a 2s není žádná jiná mocnina dvojky.
3. března 2022: V PA lze dokázat, že ireducibilních čísel je nekonečně mnoho. Dále lze dokázat větu o dělení se zbytkem a Bezoutovu větu.
1. března 2022: Existuje model demonstrující, že nad samotnou Robinsonovou aritmetikou schémata Ind a LNP ekvivalentní nejsou.
24. února 2022: Schémata Ind a LNP jsou nad teorií (Q + ∀x(x<S(x))) ekvivalentní.
22. února 2022: Peanova aritmetika PA. Užití schématu Ind k dokazování očekávaných vlastností operací a uspořádání.

Chapters in Classical Logic

About

A seminar partly based on students' presentations, devoted to various topics in metamathematics, non-classical logics, and proof theory. The topics usually include: Provability Logic, independence of the Paris-Harrington combinatorial principle over Peano arithmetic, relations between ZF, GB and the Kelly-Morse set theories, upper and lower bounds for cut-elimination in classical predicate logic, decision procedures for intuitionistic propositional logic. Here is the list of topics (in Czech). SIS: ALG500003.

Exams (Czech)

Ke zkoušce je třeba zvládnout témata dle vlastního výběru, která pokrývají 13 dvouhodinovek. Vlastní referát se do počtu 13 počítá trojnásobně.

Course contents in 2019/20 (Czech)

Konce semestru (18. května): Na posledním setkání 5.5. domluveno, že během nadcházejícího víkendu (10.5.) dá pan Štefanišin vědět, jestli má smysl se ještě jednou setkat. V tom případě by připadalo v úvahu Po 18.5. odpoledne (nebo v Út 19.5. v 9:10). 12.5. se nescházíme.
Gentzenův důkaz bezespornosti Peanovy aritmetiky (J. Štefanišin, 14. až 5. května, 3): Přednášeno dle diplomové práce Anny Horské.
Pudlákův spodní odhad pro eliminovatelnost řezů (J. Urbánek, 7. a 13. dubna, 2): Pudlákova exponenciální aritmetika PEX, superexponenciální spodní odhad.
Eliminovatelnost řezů pro klasickou predikátovou logiku (J. Rýdl, 24. března, 2): Z více důkazů je do mé knihy převzat ten, který vychází ze Schwichtenbergovy kapitoly v Handbooku (Barwise), ale je upraven pro kalkulus se všemi logickými symboly a se sekventy jako množinami.
Rozhodnutelnost a kripkovská úplnost logiky dokazatelnosti (V. Švejdar, 17. března, 1): Zpětným užitím pravidel gentzenovského kalkulu lze získat buď bezřezový důkaz, nebo kripkovský protipříklad. Téma malinko navazuje na předchozí, protože argument, že algoritmus konverguje (termination argument) není zcela triviální.
Dobrá uspořádání v teoretické informatice (J. Štefanišin, 3. března, 2): U složitějšího algoritmu může vzniknout problém jak dokázat, že se na každém vstupu dopočítá a že je korektní. To lze řešit pomocí nějaké vhodně vymyšlené terminační funkce, ale lze i definovat vtipné multimnožiny a využít obecnou větu, která se týká jejich dobrého uspořádání.
Turingovy stroje (Š. Laichter, 2): Původní článek obsahující definici Turingova stroje (ne úplně shodnou s dnes používanými). K Busy Beaver Competition pan Laichter dává k dispozici články [Rado62] a [ShenLinRado65].
Logika dokazatelnosti (V. Švejdar, 5): PA-tautologie a ℕ-tautologie. Logiky K a K4. Charakteristické třídy logik. Kalkuly pro logiku dokazatelnosti.
Autoreference (J. Urbánek, 2): Je známo (a v přednášce bylo trochu naznačeno) Gödelova-Bernaysova teorie množin GB (nověji bývá označována NBG) je konzervativní nad ZF vůči množinovým sentencím a je konečně axiomatizovatelná. V jazyce teorie GB lze napsat formuli (vlastnost přirozených čísel) J(x), která je vlastním řezem: sentence J(0) a ∀x(J(x) → J(S(x))) v GB dokázat lze, ale ∀x(J(x)) dokázat nelze. Toto je pravděpodobně Vopěnkův výsledek: plná indukce (pro všechny formule) v GB neplatí. Konstrukce řezu také ukazuje, jaký problém by vznikl, kdybychom chtěli zobecnit logickou sémantiku (rozšířit Tarského definici) tak, aby se jako struktury a modely teorií připouštěly i vlastní třídy.
Autoreference (V. Švejdar, 5): Větu o autoreferenci lze chápat jako větu o řešitelnosti rovnice pro neznámou sentenci. Löbovo řešení Henkinova problému vlastně ukazuje, že Henkinova rovnice má jednoznačně určené řešení (každá dvě řešení jsou dokazatelně ekvivalentní). Také Gödelova rovnice má jednoznačně určené řešení. Existují ale rovnice, pro které to neplatí. Rozdíl mezi Gödelovou a Rosserovou sentencí: v případě Gödelovy sentence lze v PA formalizovat důkaz její nedokazatelnosti, ale důkaz její nevyvratitelnosti formalizovat nelze, kdežto v případě Rosserovy sentence lze v PA formalizovat jak důkaz nedokazatelnosti, tak důkaz nevyvratitelnosti.

Interpretation of Gödel incompleteness theorems

About

A seminar based on students' presentations, devoted to reading papers mainly by Smorynski and Detlefsen. Here is the course announcement (in Czech). SIS: ALGV19006, Zoom.

Course contents in 2021/22 (Czech)

Detlefsenův článek z roku 1979. (J. Štefanišin, 16. prosince): Skeptická interpretace Druhé Gödelovy věty. Údajný destruktivní vliv Druhé Gödelovy věty na Hilbertův program.
Detlefsenův článek z roku 1990. (J. Rýdl, 3 lekce od 25. listopadu): První, a pak druhá prezentace.
Smorynského článek Hilbert's Programme v CWI Quarterly. (J. Urbánek, 3 lekce od 4. listopadu): Hilbert jako autor metody matematické práce, která se dá popsat jako axiomatizace. Hilbertův plán prokazovat bezespornost teorií takzvaně finitně, čili v podstatě počítáním symbolů v syntaktických zápisech a případně použitím indukce. Brouwer jako výrazná osobnost jak ve filosofii matematiky, tak v matematice samé. Na znění a interpretaci Hilbertova programu lze usuzovat ze tří Hilbertových přednášek (třetí v Lipsku v roce 1922). Gödelovo oznámení jeho věty o neúplnosti na konferenci v Königsbergu. Handout, který Jan Urbánek poskytl k přibližně druhé půlce přednášky.
Gödelův článek z roku 31 (D. Roubínek, 3 lekce od 7. října): Gödelův popis systému P odvozeného z Principia Mathematica. Čtyřicet pět primitivně rekurzívních a jedna rekurzívně spočetná podmínka v Gödelově článku: od dělení se zbytkem k dokazatelnosti. Oddíly od VII výše se pravděpodobně týkají formalizace dokazatelnosti v systému P. Je zde definována Gödelova beta funkce. Dále je explicitně formulována Druhá věta o neúplnosti, což je odpověď na dříve kladenou otázku, zda o Druhé větě neměl být článek s římskou II v titulu. V závěru je diskuse o předpokladu týkajícím se ω-konzistence. Pro platnost Druhé věty opravdu potřebný není, ale pro Gödelův důkaz První věty o neúplnosti potřebný je.

Other activities

TeX/LaTeX, pdf, ...

FBUsersSetup

The Firebird SQL server comes with a command line utility gsec for manipulating database users. Using it, one can add, delete, or modify server's users, where a modification practically means a password change.

FBUsersSetup.exe is written as an Inno Setup Windows installer*⁾Unlike normal installers, it does not write anything to the registry and does not leave any trace on your computer. So no deinstallation is provided/needed. and it basically is a gui wrapper for the gsec utility. As such, it has little additional functionality in comparison to gsec. However, it is easy to use, it can modify users on any computer in or outside the local network, it never gets confused if there are parallel instances of Firebird running on the local computer, and it can detect the properties of the local Firebird(s).

The utility is rather self-explanatory, the essential dialog pages being

DBUSubst

The utility DBUSubst.exe can substitute one Firebird database user for another. A substitution of user M for existing user D in a database means that M becomes an owner of all database objects that user D owned, he inherits all privileges that were granted to D, and he becomes a grantor of all privileges that D granted. After being substituted out, user D grants and is granted nothing, and owns no database object. If D was an owner of a database then M becomes a new database owner. Thus user substitution is a more general operation than database ownership change.

Similarly as FBUsersSetup, DBUSubst.exe is written as a (harmless for your computer) Inno Setup Windows installer. It basically is a wrapper for the isql command line utility and some sql scripts. The scripts are available in DBUSubst.zip. They are documented and thus contain a detailed information about the substitution process. The document DBUSubst.pdf contains some introductory information about the user privileges and some Firebird internals. Two essential dialog pages of DBUSubst.exe are

Vítězslav Švejdar

Introduction

About me

Research interests

Experience and education

Office info, events, miscellaneous updates

Publications

BibTeX file

Book

Some workshop or conference presentations

Papers

Logic: Incompleteness, Complexity, and Necessity (Academia, 2002)

Modal and non-classical logics

SIS ALG119008, Zoom cuni-cz.zoom.us/j/99702828164.

Exams

Course contents in Fall 2020/21 (Czech)

Properties of axiomatic theories

SIS ALG119006, Zoom.

Excercises

Exams

Course contents in Fall 2021/22 (Czech)

Arithmetics and algorithms

SIS ALG110008, Zoom.

Exams (Czech)

Course contents in Spring 2021/22 (Czech)

Huge number calculator

Incompleteness and Gödel Theorems

SIS ALG119007, Zoom.

Exams (Czech)

Course contents in Spring 2021/22

Chapters in Classical Logic

About

Exams (Czech)

Course contents in 2019/20 (Czech)

Interpretation of Gödel incompleteness theorems

About

Course contents in 2021/22 (Czech)

Other activities

FBUsersSetup

DBUSubst