V.Š. V.Š.

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

Some workshop or conference presentations

Papers

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 / AAA / A (Löbovo pravidlo LR).
Cvičení. Je-li A libovolná formula a označíme-li B formuli □(□AA)→□A, pak v logice K4 lze dokázat formuli □BB. 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 = W2, 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 { pipi+1 ; i ∈ N }. Které z formulí tvaru pipj 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á Δ0-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
Σ1-formule a Π1-formule. Všechny množiny definovatelné Σ1-formulí jsou RE. Všechny množiny, které jsou definovatelné Σ1-formulí a současně (jinou) Π1-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 (Δ0-formule). Příklady množin a relací definovatelných Δ0-formulemi: množina všech prvočísel, relace m = Mod(n,k)m = Div(n,k), množina všech mocnin dvojky. Náznak důkazu, že i relace m = nk je Δ0-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 ℵ0-kategorická. Vaughtův test: bezesporná teorie s nejvýše spočetným jazykem, která nemá konečné modely a je ℵ0-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∣ + ℵ0. 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 261 - 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(xn = 1).
19. dubna 2022
Ekvivalentní podmínka pro nesoudělnost: nenulová čísla a a b jsou nesoudělná, právě když z(abzaz). 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 xk 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 PrimesFactoring. 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] ↦ zxx"počet jedniček v binární expanzi čísla x" mají dokonce Δ0-definovatelný graf. Jejich vlastnosti, například zx+y = zx·zy, 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