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 Tue, Zoom Thu.

Excercises

Please pay attention to the list of excercises (minor corrections Jan 30 and Feb 4).

Exams

Ke zkoušce si prosím připravte seznam dvaceti cvičení, která dovedete řešit.

Course contents in Fall 2020/21 (Czech)

7. ledna 2021: První Gödelova věta: každé korektní rekurzívně axiomatizovatelné rozšíření T Robinsonovy aritmetiky, které je formulované v aritmetickém jazyce, je neúplné a nerozhodnutelné.
Cvičení. Zdůvodněte, že předpoklad o rekurzívní axiomatizovatelnosti nehraje roli pro tvrzení o nerozhodnutelnosti.
5. ledna 2021: Věta o Σ-úplnosti Robinsonovy aritmetiky: každá Σ-sentence platná v ℕ je v Q dokazatelná.
22. prosince 2020: Ještě Δ₀-definovatelnost mocniny. Důležitá (avšak nedokázaná) ingredience budoucího důkazu První Gödelovy věty o neúplnosti: každá RE relace je Σ₁-definovatelná. Věta o dokazatelnosti v Robinsonově aritmetice.
17. prosince 2020: Δ₀-formule a Σ₁-formule. Každá Δ₀-definovatelná množina je rekurzívní. Takže každá Σ₁-definovatelná je RE. Množina { [n,k,m] ; m=n^k } je Δ₀-definovatelná.
15. prosince 2020: Užití eliminace kvantifikátorů k charakterizaci definovatelných množin v určité struktuře. Například, každá množina přirozených čísel definovatelná ve struktuře 〈N,0,s,<〉 je buď konečná, nebo má konečný komplement. Omezené formule (Δ₀-formule).
Cvičení. Najděte Δ₀-formuli, která ve struktuře ℕ definuje množinu všech mocnin dvojky.
10. prosince 2020: Sjednocení a průnik RE množin je opět RE množina. Definovatelné podmnožiny a prvky struktur.
Cvičení. Dokažte, že sentence ∀x(x≤m → x=0 ∨ x=1 ∨ . . ∨ x=m) a ∀x(x≤m ∨ m≤x) jsou v Robinsonově aritmetice dokazatelné pro každé m.
Cvičení. Projekce RE množiny je opět RE množina.
8. prosince 2020: Postova věta, věta o projekci. Aplikace Postovy věty v logice: každá úplná rekurzívně axiomatizovatelná teorie je rozhodnutelná.
Cvičení 1. Když X a Y jsou RE úlohy takové, že X ∩ Y = ∅ a X ∪ Y je rekurzívní, pak X i Y je rekurzívní.
Cvičení 2. Nechť teorie T v jazyce L má pouze n navzájem neekvivalentních úplných rozšíření T₁, . . ,T_n formulovaných v tomtéž jazyce L. Pak Thm(T) = ⋂_iThm(T_i). Takže když všechny T_i jsou rozhodnutelné, i T je rozhodnutelná.
3. prosince 2020: Rekurzívní množiny jsou uzavřeny na booleovské operace. Rekurzívně spočetné (RE) množiny. Každá rekurzívní množina je RE. Projekcí rekurzívní množiny vznikne množina, která je RE.
1. prosince 2020: Kódování syntaktických objektů pomocí přirozených čísel. Rekurzívně axiomatizovatelné teorie. Robinsonova aritmetika Q.
Cvičení. Zdůvodněte, že sentence 5+2=7 a 5·2=10 jsou dokazatelné v Q. Také sentence ∀x∀y(x+y=0 → x=0 & y=0) je dokazatelná. Avšak sentence ∀x(0+x=x) a ∀x(0·x=0) dokazatelné nejsou.
26. listopadu 2020: Algoritmy, úlohy, rozhodnutelné teorie.
24. listopadu 2020: Axiomatizaze struktury 〈R,+,0,1〉.
Cvičení. Zůstalo nevyjasněné, jestli je nutné přidat k axiomům ještě schéma ∀x∀y(nx=ny → x=y).
19. listopadu 2020: Eliminace kvantifikátorů pro teorii DOS. Z toho plyne úplnost obou teorií DOS a DO.
Cvičení (nepovinné). Podobně lze dokázat úplnost pro teorii DNO (za předpokladu, že mezi logickými symboly jsou symboly pro pravdu a nepravdu) a pro teorii SUCC. Obtížnější ale pořád pravděpodobně zvládnutelný je projekt axiomatizovat strukturu 〈R,<,+,0,1〉.
12. listopadu 2020: Modelová podmínka pro konzervativní rozšíření. Teorie DOS jako konzervativní rozšíření jak teorie SUCC, tak teorie DO. První kroky v důkazu její úplnosti.
10. listopadu 2020: Varianty Löwenheimovy-Skolemovy věty. Neaxiomatizovatelnost třídy všech silně souvislých orientovaných grafů. Rozšíření a konzervativní rozšíření teorie.
Cvičení nezadáno, ale prohlédněte si prosím ty varianty Löwenheimovy-Skolemovy věty, zvlášť přehledně to dnes řečeno nebylo.
5. listopadu 2020: Axiomatizovatelné (tj. elementární) a konečně axiomatizovatelné třídy struktur.
Cvičení. Dokažte s užitím věty o kompaktnosti, že je-li třída struktur axiomatizovatelná a její komplement také, pak jsou obě konečně axiomatizovatelné.
3. listopadu 2020: Vaughtův test, κ-kategorické teorie. Úplnost teorií SUCC a DNO. Charakterizace modelů teorie DO: všechny struktury tvaru ω + (ω*+ω)·λ, kde λ je libovolný model teorie LO.
Cvičení. Formulujte bezespornou teorii v prázdném jazyce, která nemá žádné konečné modely. Pomocí Vaugtova testu dokažte její úplnost. Je teorie s prázdným jazykem a jediným axiomem ∀x∀y(x=y) úplná?
29. října 2020: Izomorfní a elementárně ekvivalentní struktury. Charakterizace modelů teorie SUCC: všechny struktury tvaru 〈N,0,s〉 + 〈Z,s〉·λ, kde λ je libovolný kardinál.
Cvičení: tentokrát nezadáno.
27. října 2020: Úplné teorie. Důkaz Löwenheimovy-Skolemovy věty s použitím věty o kompaktnosti. Teorie SUCC jako kandidát na úplnou teorii.
Cvičení. Pro strukturu 〈N,<〉 nebo pro strukturu 〈Q,<〉 vytipujte teorii, která ji axiomatizuje.
22. října 2020: Věta o silné úplnosti, věta o kompaktnosti a dvě verze Löwenheimovy-Skolemovy věty. Souvislosti mezi nimi.
Cvičení. Pro každou ze struktur 〈N,<〉, 〈Z,<〉 〈Q,<〉 (přirozená, celá resp. racionální čísla s ostrým uspořádáním) nalezněte sentenci, která v ní platí, ale neplatí v ostatních dvou.
20. října 2020: Souvislosti mezi větou o korektnosti (jejím důkazem), definicí vyplývání a logicky platnými formulemi. Sporné a bezesporné teorie.
Cvičení. Uvažujte teorii s prázdným jazykem a prázdnou množinou axiomů. Popište všechny její modely. Najděte příklady sentencí, které platí jen v některých z nich.
15. října 2020: Teorie struktury, logicky platné formule, model teorie.
Cvičení. Fragment teorie množin z minulé hodiny (to cvičení 21) je pořád aktuální. Dále cvičení 2 na straně 156, ale většinu jsme již vyřešili. Je některá z formulí ∀x(P(x) → ∀yP(y)) a ∃x(P(x) → ∀yP(y)) logicky platná?
13. října 2020: Tarského definice, platnost formule ve struktuře, logicky platné formule. Věta o korektnosti: každá formule dokazatelná z množiny předpokladů platí v každé struktuře, v níž platí všechny předpoklady.
Cvičení. Domácí úkol se sentencemi (iv) a (v) z minulého týdne je pořád aktuální. Řešitelné je také cvičení 21 na straně 182 knihy [Šv02].
8. října 2020: Hilbertovský kalkulus. Syntaktické pojmy: důkaz, modus ponens, pravidla generalizace, výrokové axiomy, axiomy specifikace, axiomy rovnosti, věta o dedukci.
Domácí cvičení. Připomeňte si větu o korektnosti a pokuste se ji použít ke zdůvodnění, že sentence (iv) ∀x(S(x)≠x) a (v) ∀x(x=0 ∨ ∃y(x=S(y))) nejsou dokazatelné v teorii s axiomy Q1 a Q2.
6. října 2020: Formální a neformální důkazy (tří sentencí z minulé hodiny). Užití (výrokových) tautologií a tautologického důsledku při konstrukci důkazů v hilbertovském kalkulu pro klasickou predikátovou logiku s rovností. Ručně psanými poznámkami se moc chlubit nemohu (prosím nešířit), ale třeba trochu pomohou.
Domácí cvičení. (a) Podejte příklad termu, který je substituovatelný za nějakou proměnnou v nějaké formuli, a jiného termu, který substituovatelný není (třeba za tutéž proměnnou v téže formuli). (b) Nalezněte důkaz (neformální nebo i formální) sentence ∃x(P(F(x)) ∨ ¬P(x)) v teorii, která má prázdnou množinu axiomů, unární predikát P a unární funkční symbol F.
1. října 2020: Formule klasické predikátové logiky s rovností.
Domácí cvičení. Uvažujte teorii s jazykem {0,S} a s axiomy ∀x∀y(S(x)=S(y) → x=y) a ∀x(S(x)≠0). Nalezněte neformální důkazy následujících sentencí: (i) S(0)≠0, (ii) S(S(0))≠S(0), (iii) ∀x∃y(S(y)≠x).

Arithmetics and algorithms

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

SIS ALG110008, Zoom.

Exams (Czech)

Zkouška může proběhnout pokud možno co nejdříve v termínu dle domluvy (preferuji Po a Út dle celkem kdykoliv, St navečer a Pá ráno). Mám pro tento účel rezervované termíny 25.5., 8.6. a 29.6. vždy od 15h v Hlavní budově, ale není nutné se omezovat na tyto doby. Ke zkoušce si prosím připravte (přineste) řešení jedenácti cvičení vybraných z množiny 1 až 14 (i s vysvětlením matematického či algoritmického pozadí). Zkouška by v každém případě měla zahrnout i prodiskutování některého důkazu. Zkoušku přes Zoom nevylučuji.

Course contents in Spring 2020/21 (Czech)

13. května 2021: Kryptografická metoda RSA. Důkaz její korektnosti pomocí modulárních reprezentací. Mersennova prvočísla a Coleův výsledek z roku 1903 týkající se čísla 2⁶⁷ - 1. Neformální vysvětlení, co je třída NP (úloh rozhodnutelných v tzv. nedeterministickém polynomiálním čase).
6. května 2021: Čínská zbytková věta: když m je součin navzájem nesoudělných čísel p₁,..,p_n a [r₁,..,r_n] je n-tice čísel takových, že 0 ≤ r_i < p_i, pak [r₁,..,r_n] je modulární reprezentací nějakého (ale jediného) a ∈ ℤ_m. Užití modulárních reprezentací k důkazu, že 341 je pseudoprvočíslo.
29. dubna 2021: Umocňování v okruhu ℤ_m. Pseudoprvočísla. Modulární reprezentace.
22. dubna 2021: Eulerova grupa a Eulerova funkce. Eulerova (Malá Fermatova) věta.
Cvičení. Užijte Eulerovu větu a případně i Bezoutovu větu a spočítejte 7¹⁰⁷ v ℤ₂₇. Určete číslo φ(100).
15. dubna 2021: Komutativní monoidy, Abelovy grupy a komutativní okruhy. Eulerova grupa okruhu ℤ_m.
Cvičení. Kolik prvků má Eulerova grupa okruhu ℤ_m, když m je prvočíslo? Kolik má prvků, když m je součin dvou různých prvočísel?
8. dubna 2021: Přehled důsledků Bézoutovy věty pro prvočíselnost, nesoudělnost, společný násobek a určování inverzních a invertibilních prvků v ℤ_m.
Cvičení nezadáno, avšak nahlédněte prosím nahoře do pdf souboru s cvičeními.
1. dubna 2021: Opakování a zpřesnění ireducibilních čísel a prvočísel. Inverzní a invertibilní prvky ve struktuře ℤ_m.
Záznam přednášky: těm, kteří se nemohli zúčastnit, možná pomohou poznámky nebo videozáznam celé přednášky. Ale moc dobré studijní materiály to nejsou, takže zájemcům nabízím individuální konzultaci. Videozáznam z mého počítače spustit šel, ale kdyby z Vašeho nešel, ozvěte se, mám od Zoomu ještě heslo.
Cvičení. Dokažte (užitím Bezoutovy věty na a a b), že když a a b jsou nesoudělná, pak splňují podmínku ∀z(a ∣ bz → a ∣ z). Vysvětlete, že pokud a a b tuto podmínku splňují, nemusí být nesoudělná.
25. března 2021: Užití Bézoutovy věty k důkazu, že každé ireducibilní číslo je prvočíslo. Definice komutativního okruhu.
Cvičení. Jak je třeba opravit definice, aby vyšlo, že každé prvočíslo je ireducibilní?
17. března 2021: Bézoutova věta. Zobecněný (čtyřsloupcový) Eukleidův algoritmus pro nalezení řešení Bézoutovy rovnice.
Cvičení. Pro která čísla c je rovnice 78x + 21y = c řešitelná?
11. března 2021: Když n není prvočíslo, pak ani 2ⁿ - 1 není prvočíslo. Teoretický důsledek Eukleidova algoritmu: každá dvě celá čísla mají společného dělitele, který je dělitelný všemi jejich společnými děliteli. Obecné definice pojmů týkajících se dělitelnosti (největší společný dělitel, nesoudělná čísla, ireducibilní čísla). Oprava (doplnění) k číslu 0: dvě čísla definujeme jako soudělná, jestliže nejsou nesoudělná, čili jestliže mají společného dělitele, který není dělitelem jedničky. Pak vyjde, že nula je nesoudělná s děliteli jedničky, soudělná se všemi ostatními čísly.
Cvičení. Zdůvodněte, že rovnice 4495x + 2356y = 160 nemá v oboru celých čísel řešení.
4. března 2021: Eukleidův algoritmus pro úlohu GCD. Jeho časové nároky.
Cvičení. Nalezněte největšího společného dělitele čísel 829 931 a 715 997.
25. února 2021: Časové nároky algoritmů. Algoritmy pracující v polynomiálním čase, tj. polynomiální algoritmy. Polynomiálně počitatelné úlohy. Dělitelnost v oboru celých čísel. Vlastnosti relace dělitelnosti.
18. února 2021: Úlohy a algoritmy. Úlohy Mult, Factoring, GCD a Primes, a algoritmy, které je počítají.

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 (incomplete) list of excercises.

SIS ALG119007, Zoom.

Course contents in Fall 2020/21

18. května 2021: Disjunction property. Harropovské formule.
13. května 2021: Kripkovské modely pro intuicionistickou výrokovou logiku. Persistence, vzájemná nevyjádřitelnost logických spojek. Ostatní sémantické pojmy (vyplývání...).
11. května 2021: Interpretovatelnost sentencí Con(τ) a ¬Con(τ).
6. května 2021: Souvislost formalizované konzistence s interpretovatelností: teorie T je interpretovatelná v každé teorii S, která je rozšířením PA a je v ní dokazatelná bezespornost T.
4. května 2021: Podstatná neúplnost a podstatná nerozhodnutelnost. Každá bezesporná rozhodnutelná teorie má rozšíření (se stejným jazykem), které je rozhodnutelné a úplné.
29. dubna 2021: Rosserova věta a její formalizace v PA. Aplikovatelnost modální logiky v metamatematice.
27. dubna 2021: Důkaz Löbovy věty převedením na Gödelovu větu. Rosserova sentence.
22. dubna 2021: Souvislost Druhé Gödelovy věty s modální logikou. Löbova věta. Löbova rovnice také má jednoznačně určené a explicitně vyjádřitelné řešení.
20. dubna 2021: Druhá Gödelova věta. Některé souvislosti, Hilbertův program.
15. dubna 2021: Druhá Gödelova věta. Její formalizace v PA. Gödelova autoreferenční rovnice má jednoznačně určené a navíc explicitně vyjádřivelné řešení, totiž sentenci vyjadřující konzistenci.
13. dubna 2021: Slabá reprezentovatelnost funkcí v Q. Různé autoreferenční sentence: Gödelova, Henkinova plus dva dodatečné (školní) příklady, které demonstrují, že autoreferenční sentence může tvrdit něco nejen přímo o sobě, ale i o výsledku zpracování sebe sama nějakou Δ₀-definovatelnou funkcí, a druhý navíc ukazuje, že řešení autoreferenční rovnice nemusí být určené jednoznačně.
8. dubna 2021: Věta o autoreferenci. Gödelova sentence a Henkinova sentence.
6. dubna 2021: Podmínky pro dokazatelnost (Löbovy podmínky). Některé jejich důsledky.
1. dubna 2021: Formalizovaná bezespornost. Formalizované numerály a formalizovaná věta o Σ-úplnosti.
30. března 2021: Podmínka D1. Dokazatelnost bezespornosti teorie, která má prázdnou množinu axiomů (jazyk libovolný). Existence definice π*(z) Peanovy aritmetiky, pro kterou platí PA ⊢ Con(π*).
25. března 2021: Vlastnosti formalizované dokazatelnosti. Přirozené definice teorií Q a PA. Formalizovaná věta o dedukci. Podmínka D2 (Löb's second derivability condition).
23. března 2021: Princip kolekce. Σ_m(PA)- a Π_m(PA)-formule.
18. března 2021: Formalizace syntaktických pojmů, včetně pojmů důkaz, dokazatelnost a bezespornost.
16. března 2021: Formalizace termů, kvazitermů a formulí v Peanově aritmetice.
11. března 2021: Počítání jedniček v binární expanzi čísla. Z toho plyne možnost počítat znaky v textových řetězcích. Formalizace některých syntaktických pojmů (proměnné, numerály).
Cvičení. Nechť slovo u je vyvážený podřetězec slova w vymezený čísly i₁ a j₁ (v tom smyslu, že nejlevější znak slova u je na pozici i₁, kdežto j₁ určuje první pozici za u, takže u má délku j₁ - i₁). Nechť v je jiný vyvážený podřetězec slova w vymezený čísly i₂ a j₂ a platí i₁ ≤ i₂ < j₁. Pak j₂ ≤ j₁.
9. března 2021: Formalizace pojmů v PA: prvočísla, mocniny dvojky, exponenciální funkce. Existují modely PA obsahující nestandardní Δ₀-definovatelné prvky.
4. března 2021: V PA lze dokázat Bezoutovu větu. Dále, ireducibilní čísla jsou přesně ta čísla, která jsou prvočísly, a je jich nekonečně mnoho.
2. března 2021: Ekvivalennce schémat Ind a LNP nad Robinsonovou aritmetikou s jedním dodatečným axiomem. Vlastnosti operací a uspořádání dokazatelné v PA. Dělení se zbytkem.
25. února 2021: Schémata Ind a LNP. Teorie R. Nestandardní model Robinsonovy aritmetiky, v němž leccos neplatí, avšak schéma LNP platí. Užití schématu Ind k důkazům vlastností operací.
23. února 2021: Hierarchie aritmetických formulí. Axiomy Robinsonovy aritmetiky Q. Q není konzervativním rozšířením teorie s axiomy Q1-Q5, ta ale je konzervativním rozšířením teorie s axiomy Q1-Q3.
18. února 2021: Struktura nestandardního modelu teorie Th(ℕ). Δ₀-formule, jejich důležité příklady.
16. února 2021: Opakování: kalkuly, struktury, uspořádané množiny, struktura přirozených čísel; izomorfismus a elementární ekvivalence.

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.

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 Tue, Zoom Thu.

Excercises

Exams

Course contents in Fall 2020/21 (Czech)

Arithmetics and algorithms

SIS ALG110008, Zoom.

Exams (Czech)

Course contents in Spring 2020/21 (Czech)

Huge number calculator

Incompleteness and Gödel Theorems

SIS ALG119007, Zoom.

Course contents in Fall 2020/21

Chapters in Classical Logic

About

Exams (Czech)

Course contents in 2019/20 (Czech)

Other activities

FBUsersSetup

DBUSubst