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
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 = 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 { pi → pi+1 ; i ∈ N }. Které z formulí
tvaru pi → pj
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
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)
a 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.
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(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 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 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.
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] ↦ zx
a x ↦ "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
- the selection
of a db server

On the local computer, TIGER, there are two parallel instances of Firebird.
One communicates through the standard port 3050, the other through port fb25 that translates
to 3060 in the services
file. The user can click on one of them in the listbox,
or say something else. Assume that, since he wants to modify users on the computer JUPITER where
Firebird communicates through port 3060, he deleted the text "TIGER" in the upper text field
and typed "JUPITER/3060" instead. In the two bottom text fields he has to specify the admin login.
In most cases, the admin would be SYSDBA. However, in Firebird 2.0 and later any user can
change his own password.
, and then
- a user action
The version of Firebird addressed as JUPITER/3060 is 2.5.2. Besides SYSDBA, there
are three other database users on that server. Since database user's first and last names are hardly ever needed,
FBUsersSetup somewhat misuses these data and codes the current time into them: JOSEPH and VIOLA
were inserted on Apr 14th, 2013. JASMIN was not inserted using FBUsersSetup and so her
first and last names are unknown. A new database user ADAM is now about to be inserted.
on that server.
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
- the database connection

Our database zoodata.fdb resides on a computer orel where
(the relevant instance of) Firebird communicates thru port 3060;
orel can be a computer in the local network or a
computer visible on internet. Of course, if it is not the local computer
on which DBUSubst is run, the browse button cannot be used; the path to zoodata.fdb
has to be typed.
When developing the database, we accessed it as a user LION.
This user is an owner of the database.
We also have another user VISITOR who is designed to have some restricted
access. Now when the database is about to be
deployed, it appears that the name LION was not wisely selected and that the
owner name should be ZOODBA. So we are about to substitute ZOODBA for LION.
ZOODBA already exists on the server in question, i.e. orel/3060.
with the NEW user's login, and then
- the login of
the dead
user

Since we were allowed to proceed to this dialog window, the login of
ZOODBA was verified against Firebird on orel/3060. It was also detected
that the version of this Firebird server is 2.5.1 and that the owner
of the database is LION, see the blue text labels in the bottom.
We are now selecting LION as the user who will be substituted by ZOODBA,
and we have to specify his password. The password of VISITOR is immaterial
for the current substitution process since VISITOR is not
a grantor of anything. However, if there were other users who
granted something to LION, further dialog windows asking about their
passwords would follow.
, i.e. the user who is to disappear.