V.Š. V.Š.


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


BibTeX file

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


Some workshop or conference presentations


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.


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 AA se tradičně nazývá princip T. Dále □(□AA) → □A je Löbův axiom, kdežto AA / 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.


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


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 Δ1 sets. Interdefinability of these notions. Characteristic function of a set. The graph of a recursive function is Δ1. 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. Δ0, Σn and Πn formulas. Δ0, Σ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. It (may extend and) will be used during the exam.

SIS ALG110008, Zoom.

Course contents in Spring 2022/23 (Czech)

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 FactoringPrimes. 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 MultPrimes, 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 24th) list of exercises.

SIS ALG119007, Zoom.

Course contents in Spring 2022/23

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 Δ0 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 Δ0(PA)) and the number of primes less than x (its graph is certainly Σ1(PA), but it is not known to be Δ0(PA)).
Mar 2nd, 2023
Exponentiation can be formalized in PA. The formula y = zx is Δ0(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


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.

Course contents in 2022/23 (Czech)

Kombinatorické principy nezávislé na PA (D. Roubínek, od 9.3.23)
Kayova teorie PA-. Ramseyova věta.
Hyperprosté množiny a nezávislá axiomatizovatelnost (J. Urbánek, 5 týdnů od 22.12.22)
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 in) 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.22)
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, tři 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


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, ...


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 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