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

Ke zkoušce si prosím připravte seznam šesti cvičení ze seznamu cvModL.pdf, která dovedete řešit. Na poslední přednášce si tento požadavek upřesníme.

Course contents in Fall 2022/23 (Czech)

5. ledna 2023: Podrámce a disjunktní sjednocení rámců jako speciální případy bisimulace mezi rámci. Charakteristická třída libovolné logiky je uzavřena na podrámce, disjunktní sjednocení a p-morfní obrazy.
22. prosince 2022: Cresswellův model. Logika K + H je slabší než GL.
15. prosince 2022: Charakteristická třída logiky GL je třída všech tranzitivních obráceně fundovaných rámců. Táž třída je i charakteristickou třídou pro schéma H.
8. prosince 2022: Logika S5 a její charakteristická třída. Schéma 4 je dokazatelné v S5. V logice S4 platí, že z dvojice sousedících a stejných modalit lze jednu ekvivalentně vypustit. V S5 platí, že ze dvou sousedících libovolných modalit lze první ekvivalentně vypustit. Logika GL. Schéma 4 je dokazatelné v GL.
1. prosince 2022: Schémata 4, T, B a 5 a jejich charakteristické třídy. Logika S4.
24. listopadu 2022: Logika K4, příklad důkazu v ní, její gentzenovský kalkulus. Charakteristické třídy logik.
Domácí cvičení. 1. Dokažte, že hilbertovský a gentzenovský kalkulus se navzájem simulují. Takže jsou spolu ekvivalentní.
2. Nalezněte charakteristickou třídu logiky, která vznikne přidáním schématu A → □◇A k logice K.
3. Nalezněte charakteristickou třídu logiky, která vznikne přidáním formule ¬□⊥ → ¬□¬□⊥ ke K.
10. listopadu 2022: Logika K je rozhodnutelná. Pro oba její kalkuly platí věta o úplnosti. Pro gentzenovský kalkulus platí i věta o eliminovatelnosti řezů. Vlastnost konečných modelů: každá nedokazatelná formule má kripkovský protipříklad, který je konečným antireflexivním stromem.
3. listopadu 2022: Gentzenovský kalkulus pro logiku K. Vzájemná simulovatelnost gentzenovského a hilbertovského kalkulu. Podmodel kripkovského modelu generovaný prvkem.
27. října 2022: Zbývající pravidla kalkulu GK. Subformula property. Pro kalkulus GK platí věta o korektnosti, věta o úplnosti a věta o eliminovatelnosti řezů.
Domácí cvičení. Navrhněte vhodná pravidla pro spojku ≡.
20. října 2022: Dokazatelnost a nedokazatelnost v logice K. Gentzenovský kalkulus GK pro klasickou výrokovou logiku.
13. října 2022: Splněnost formule ve vrcholu kripkovského modelu, platnost formule v modelu. Schéma □A → □□A platí v každém modelu, jehož rámec je tranzitivní (ale i v některých jiných modelech). Logika K a její hilbertovský kalkulus.
Domácí cvičení. S užitím faktu, že všechny tautologie jsou dokazatelné, zdůvodněte, že □A&□B → □(A&B) je v K dokazatelná pro každou volbu formule A.
6. října 2022: Opakování klasické výrokové logiky: logické spojky, tautologie, tautologický důsledek, věta o kompaktnosti. Modality nutnosti a možnosti. Modální výrokové formule. Různé modální principy. Například □A → A se tradičně nazývá princip T. Dále □(□A → A) → □A je Löbův axiom, kdežto □A → A / A je Löbovo pravidlo.
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?

Properties of axiomatic theories

SIS ALG119006, Zoom.

Exercises

Please pay attention to the list of exercises. Here are the same exercises in English.

Exams

For the exam please prepare a list of twenty-one exercises that you can solve. Exercise 22 (provability in Q) can be counted three times.

Course contents in Fall 2022/23 (Czech)

Jan 5th, 2023: Σ-completeness theorem. Gödel's 1st incompleteness theorem.
Jan 3rd, 2023: Schemas provable in Robinson arithmetic.
Dec 22th, 2022: A simple nonstandard model of Robinson arithmetic Q. Basic properties of operations (like the commutativity and associativity) and properties of the ordering (transitivity) are usually unprovable in Q.
Dec 20th, 2022: A set is RE if and only if it is the domain of some partial recursive function. Adding finitely many axioms to a decidable theory yields a decidable theory. A consequence of this fact and the undecidability of Q (to be proved later) is that the set of all arithmetic formulas that are logically valid is nonrecursive. From the fact (also waiting for a proof) that RE sets that are not recursive exist it follows that ℕ is an undecidable structure.
Dec 15th, 2022: Official definitions of partial recursive functions, RE sets and Δ₁ sets. Interdefinability of these notions. Characteristic function of a set. The graph of a recursive function is Δ₁. Any partial recursive function, i.e. a function with an RE graph, is algorithmically computable in the intuitive sense.
Dec 8th, 2022: Recursively axiomatizable theories. If T is recursively axiomatizable, then the sets Thm(T) and Ref(T) are RE. If T is also complete, then it is decidable.
Dec 8th, 2022: Connections between recursive and RE sets. The projection of a recursive set is RE. Two disjoint sets whose complements are RE can be recursively separated in the sense that there exists a recursive set D containing one of the two sets and disjoint with the other.
Dec 6th, 2022: Partial recursive functions, recursive sets and RE sets, preliminary considerations and summary of the expectations. Recursive conditions are closed under Boolean operations and bounded quantification.
Dec 1st, 2022: Arithmetical sets. Δ₀, Σ_n and Π_n formulas. Δ₀, Σ_n and Π_n sets (relations), closure under operations. This system of sets (relations) is called arithmetical hierarhy.
Nov 29th, 2022: Quantifier elimination can be used to characterize sets definable in some structures.
Nov 24th, 2022: Quantifier elimination for the theory DOS. Further theories that admit quantifier elimination (no proofs). Sets definable in a structure.
Nov 22th, 2022: Provability in the theory DOS. DOS is a conservative extension of SUCC, and also of DO.
Nov 15th, 2022: Quantifier elimination for the theory SUCC, finalization. Conservative extension of a theory. The theory DOS.
Nov 10th, 2022: The theory SUCC admits quantifier elimination.
Nov 8th, 2022: The theory DNO as an attempt to axiomatize the structure η. Vaught's test, κ-categorical theories. DNO is complete because it is one of the (not so many) theories to which Vaught's test is applicable.
Nov 3rd, 2022: The Löwenheim-Skolem theorems. Complete axiomatic theories. The theory LO. The theory DO as an attempt to axiomatize the structure ω. The theory SUCC.
Nov 1st, 2022: Non-axiomatizability of the class of all well-ordered sets. Reduct and expansion of a structure. Types of linearly ordered sets, and operations with them. The order type of the reduct of a nonstandard model of Th(ℕ) to the language {<} is ω + (ω* + ω) ⋅ λ where λ is a densely ordered set.
Oct 27th, 2022: Using the compactness theorem to prove non-axiomatizability of some classes of structures. The existence of a countable nonstandard model of Th(ℕ).
Homework. Exercises 14-16. When writing down the solution, avoid using syntactic notions (like consistency).
Oct 25th, 2022: Axiomatizable and finitely axiomatizable classes of structures.
Oct 20th, 2022: Theory of a structure. Elementarily equivalent structures. The completeness and compactness theorems, the Löwenheim-Skolem theorem.
Oct 18th, 2022: The class of all models of a theory. Isomorphic structures do not differ in the validity of any sentence.
Oct 13th, 2022: More semantic notions: the consequence relation, logically valid formulas, model of a theory. Proving unprovability, for example in the theory {Q1,Q2}, using the soundness theorem.
Homework. Pick three exercises among 1-9 (however, 6-8 might be somewhat difficult, and 5 may be found boring) and solve them. Do not rely on symbolic expression, write (also) sentences in Czech (English). In the case of Exercise 1, it is not necessary to deal with all sentences.
Oct 11th, 2022: The deduction theorem. Consistent and contradictory theories. Characterization of provability using contradictoriness. The sets Thm(T) and Ref(T). Tarski's definition. Formulas valid in a structure.
Oct 6th, 2022: Informal proofs, their translation to the calculus HK. Tautologies in predicate logic with equality.
Oct 4th, 2022: Terms, formulas, axiomatic theories. A classroom example: a theory having Q1 and Q2 as axioms.

Arithmetics and algorithms

Please pay attention to the list of exercises.

SIS ALG110008, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení patná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. V SISu budou vypsány nějaké termíny na pokud možno všechny úterky do konce června s výjimkou týdne od 20.6. Později pokud možno i v září, ale počítejte prosím s určitou improvizací a ne s úplně každým týdnem. Všechny termíny lze využívat i jako konzultace a mailem se lze domluvit i na jiné dny než ty vypsané v SISu, většinou na Po a St navečer nebo Út celkem kdykoliv.

Course contents in Spring 2022/23 (Czech)

11. května 2023: Když p je prvočíslo a k je dělitel čísla p - 1, pak v grupě Φ(p) je přesně φ(k) prvků řádu k. Z toho mimo jiné plyne, že ve Φ(p) existují prvky maximálního možného řádu p - 1, neboli že Φ(p) je cyklická grupa.
4. května 2023: Řády prvků v grupách. Řád libovolného a ∈ Φ(n) musí být dělitelem čísla φ(n). Známé tvrzení, že polynom stupně k, který není identicky nulový, má nejvýše k různých kořenů, platí ve všech oborech integrity.
27. dubna 2023: Kryptografická metoda RSA. Mersennova čísla a Mersennova prvočísla.
20. dubna 2023: Počítání s modulárními reprezentacemi. Čínská zbytková věta.
13. dubna 2023: Umocňování x^y v ℤ_m, chápané jako funkce tří proměnných, je polynomiálně počitatelné. Pseudoprvočísla.
30. března 2023: Bézoutova věta jako důsledek korektnosti čtyřsloupcového Eukleidova algoritmu. Některé její důsledky: ekvivalentní podmínka pro nesoudělnost nenulových čísel a a b (tj. podmínka ∀z(a ∣ bz → a ∣ z)) a fakt, že když prvočíslo je dělitelem součinu xy, musí být dělitelem některého z čísel x a y (toto ponecháno jako cvičení).
23. března 2023: Úloha určit (z a a m), zda a je v ℤ_m invertibilní, a také úloha nalézt inverzní prvek k invertibilnímu a jsou polynomiálně počitatelné. Nesoudělnost, prvočísla (v oborech integrity). Čtyřsloupcové rozšíření Eukleidova algoritmu.
Domácí úkol: cvičení 5 (cvičení 1-4 jsou také řešitelná nebo již vyřešená).
16. března 2023: Definice největšího společného dělitele, úloha GCD. Eukleidův algoritmus a jeho časové nároky.
9. března 2023: Eulerova grupa (nějakého přirozeného čísla). Tělesa a obory integrity. Dělitelnost v oborech integrity.
Cvičení. Dokažte, že relace asociativnosti je ekvivalence.
2. března 2023: Komutativní monoidy a komutativní (čili Abelovy) grupy. Invertibilní prvky monoidu tvoří grupu. Věta (možná Eulerova) o umocňování v konečných komutativních grupách. Okruhy a počítání s opačnými prvky v nich. Struktury ℤ, ℚ, ℤ_m a ℚ[x] jako příklady okruhů.
23. února 2023: Pojem polynomiálního algoritmu. Rozdíl mezi úlohami Factoring a Primes. Monoidy a invertibilní prvky v nich.
Cvičení. Je-li na množině {0,. .,14} operace ∗ definována předpisem x∗y = Mod(xy,15), které prvky jsou invertibilní?
16. února 2023: Několik všeobecně matematických pojmů: přirozená, celá a racionální čísla, dělení se zbytkem, relace a některé jejich vlastnosti (reflexivita, tranzitivita). Logické symboly (spojky a kvantifikátory). Úlohy a algoritmy. Úlohy Mult a Primes, a algoritmy, které je počítají. Časové nároky algoritmů. Například školní algoritmus pro úlohu Mult počítá v kvadratické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 19th, 2023) list of exercises.

SIS ALG119007, Zoom.

Exams (Czech)

Please bring a list of 14 exercises whose solution you are able to present.

Course contents in Spring 2022/23

May 11th, 2023: Completeness of the propositional calculus GJ. Two by-products of the proof: the cut-elimination theorem and the finite model property. Kripke semantics of intuitionistic predicate logic.
May 9th, 2023: The relationship between classical and intuitionistic logic: Glivenko's theorem. The disjunction property. The calculus GJ.
May 4th, 2023: Constructing Kripke counterexamples. Every intuitionistic tautology is a (classical) tautology.
May 2nd, 2023: Kripke semantics for intuitionistic propositional logic.
Apr 27th, 2023: Essentially undecidable and essentially incomplete theories. Motivating considerations concerning intuitionistic logic.
Apr 25th, 2023: Rosser's theorem. Craig's trick.
Apr 20th, 2023: Some connections of Gödel's 2nd theorem: Hilbert's program, uniqueness of fixed points, the variety of formulas τ(z) defining the same theory.
Apr 18th, 2023: Gödel's second incompleteness theorem. Its formalization in PA.
Apr 13th, 2023: The self-reference theorem. Th(ℕ) is a non-arithmetical set. Gödel's self-referential sentence.
Apr 11th, 2023: Löb's derivability conditions. An ad hoc semantics showing that some consistency statements are provable in PA.
Apr 4th, 2023: Facts about provability (the deduction theorem etc.) that are provable in PA. The formalized completeness theorem.
Mar 30th, 2023: Formalization of provability and consistency in PA.
Mar 28th, 2023: Using balanced strings in some cases, the basic syntactic notions (variables, terms, formulas, substitutability, the substitution function etc.) can be formalized in PA.
Mar 23rd, 2023: String functions, balanced strings.
Mar 21st, 2023: Partial recursive functions are closed under primitive recursion and course-of-values recursion. An infinite subset of N is RE if and only if it is the range of some one-to-one function.
Mar 16th, 2023: Partial recursive functions are closed under composition and minimization.
Mar 14th, 2023: Some connections between RE sets and partial recursive functions: a set is a projection of a Δ₀ relation (or a projection of a recursive relation) if and only if it is the domain of some partial recursive functions, and a nonempty subset of N is RE if and only if it is the range of some recursive function.
Mar 9th, 2023: Recursively enumerable sets, partially recursive and recursive functions. The collection schema (with some additions) can be used to construct an alternative axiomatization of PA.
Mar 7th, 2023: Further functions formalizable in PA: the number of bits in the binary expansion of x (its graph is Δ₀(PA)) and the number of primes less than x (its graph is certainly Σ₁(PA), but it is not known to be Δ₀(PA)).
Mar 2nd, 2023: Exponentiation can be formalized in PA. The formula y = z^x is Δ₀(PA).
Feb 28th, 2023: The fact that irreducible numbers are the same as prime numbers is provable in PA. Properties of powers of two are provable in PA as well. For example, the product of any two powers of two is again a power of two.
Feb 23th, 2023: The infinitude of irreducible numbers, and also Bézout's theorem are provable in PA.
Feb 21th, 2023: The least number principle (LNP) is provable in PA. More exactly, over (Q + ∀x(x<S(x))) it is equivalent to the induction schema. However, these two schemas are not equivalent over Q itself.
Feb 16th, 2023: Peano arithmetic PA. Using the schema Ind to prove the expected properties of operations and the two order relations.
Feb 14th, 2023: Robinson arithmetic and its properties.

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) in the academic year 2022-23. 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í přednáška se do počtu 13 počítá trojnásobně.

Course contents in 2022/23 (Czech)

Nezávislost Paris-Harringtonova principu na PA (D. Roubínek, 2. a 9.5.): Poslední kapitola v knize Handbook of Mathematical Logic.
Intuicionistická predikátová logika (B. Heřmanová, 3.5 týdne od 4.4.): Sémantika intuicionistické predikátové logiky. Tři prenexní implikace, které nejsou intuicionisticky logicky platné. Schéma DNS. Chování rovnosti, mimolehlost, axiomy stability.
Kombinatorické principy nezávislé na PA (D. Roubínek, 4 týdny od 7.3.23): Kayova teorie PA^-. Ramseyova věta. Důkaz nekonečné Ramseyovy věty převedením na Königovo lemma.
Hyperprosté množiny a nezávislá axiomatizovatelnost (J. Urbánek, 5 týdnů od 22.12.): Ekvivalentní definice hyperprosté množiny. Rekurzívně axiomatizovatelná teorie je nezávisle axiomatizovatelná, právě když má axiomatizaci { α_i ; i ∈ N }, jejíž markant (tj. množina všech n takových, že α_n+1 je dokazatelná z konjunkce všech α_i pro i ≤ n) není hypersimple. To je právě tehdy, když každá axiomatizace má tuto vlastnost.
Aritmetická úplnost logiky dokazatelnosti (V. Švejdar, 5 týdnů od 15.11.): Varianty axiomatizace logiky GL. Logika GLS, která není normální, je kandidátem na logiku, která axiomatizuje množinu všech ℕ-tautologií. GLS-modely. Kripkovská úplnost logiky GLS. Solovayův důkaz aritmetické úplnosti obou logik.
Metamatematika teorií množin (M. Blahynka, 3 týdny od 25.10.22): Gödelova-Bernaysova teorie množin GB a její konečná axiomatizovatelnost. Pravdivostní relace a obsaditelná přirozená čísla. V GB není dokazatelná indukce pro všechny její formule, a je nad ZF konzervativní vůči množinovým sentencím.
Autoreference (V. Švejdar, 3 týdny): Aritmetizace dokazatelnosti. Löbovy podmínky. Gödelova, Henkinova a Löbova autoreferenční rovnice. Přinejmenším první dvě mají jednoznačně určené řešení.

Interpretation of Gödel incompleteness theorems

About

A seminar based on students' presentations, devoted to reading papers mainly by Smorynski and Detlefsen. Here is a course announcement. SIS: ALGV19006.

Course contents in 2023/24

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 2022/23 (Czech)

Properties of axiomatic theories

SIS ALG119006, Zoom.

Exercises

Exams

Course contents in Fall 2022/23 (Czech)

Arithmetics and algorithms

SIS ALG110008, Zoom.

Exams (Czech)

Course contents in Spring 2022/23 (Czech)

Huge number calculator

Incompleteness and Gödel Theorems

SIS ALG119007, Zoom.

Exams (Czech)

Course contents in Spring 2022/23

Chapters in Classical Logic

About

Exams (Czech)

Course contents in 2022/23 (Czech)

Interpretation of Gödel incompleteness theorems

About

Course contents in 2023/24

Other activities

FBUsersSetup

DBUSubst