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 2023/24

Dec 21th, 2023
A consequence of the above theorem is that the collection of Δ1 sets is closed under Boolean operations and bounded quantification. Also, all projections of Δ1 sets are RE. Both Dom(f) and Rng(f) of a partial recursive f are RE. In fact, a set is RE if and only if it is the domain of some partial recursive function. This claim is known as the projection theorem. The graph of a recursive f must be Δ1. For each pair A and B of RE sets there exist RE sets X and Y such that XY = AB, XY = ∅, ABX and BAY. Two sets A and B are recursively separable if there exists a recursive set D such that AD and DB = ∅. Any two disjoint Π1 sets are recursively separable. This is an easy consequence of the just mentioned theorem. However, there exist RE sets A and B that are disjoint and recursively inseparable. This fact will be useful in the proof of (a variant of) the incompleteness theorem.
Dec 19th, 2023
Further official definition: a set is Δ1, i.e. recursive, if it is both Σ1 and  Π1. A function f of q variables is partial recursive if Graph(f), i.e. f taken as a set of (q + 1)-tuples, is RE. A function f of q variables is recursive if it is partial recursive and total (its domain Dom(f) equals Nq). The collection of Σ1 sets is closed under ∃, &, ∨ and bounded quantification. The collection of Π1 sets is closed under ∀, &, ∨ and bounded quantification.
Dec 14th, 2023
A theory T is recursively axiomatizable if it is equivalent to a theory S such that S is a recursive set. If T is recursively axiomatizable, then Thm(T), i.e. the set of all sentences φ such that Tφ, is recursively enumerable. Indeed, Tφ is equivalent to ∃dProofT(φ,d) where ProofT(φ,d) is the condition "d is a proof of φ in T", and we expect that (once we state a definition) this condition is recursive. A theory T is decidable if Thm(T) is recursive. Post's theorem is also one of the expected facts since if both A and NqA are RE, then we can specify an informal but obviously correct algorithm that decides the membership to A. Now finally the definition: a set is RE if it is the projection of some Δ0 relation, i.e. if it is definable in ℕ by a formula of the form ∃(v,x) where φ ∈ Δ0. A set is Π1 if it is definable in ℕ by a formula of the form ∀(v,x) where φ ∈ Δ0.
Dec 12th, 2023
A subset of a domain whose elements can be written as strings (finite sequences of symbols) is a decision problem. A decision problem is in fact a set of questions called instances. It may or may not be algorithmically decidable (recursive). By definition, something is an algorithm if it can be formalized in a fixed computational model. A string can be coded by a natural number. A natural way of coding is to consider individual symbols digits in B-ary notation where B is a sufficiently big number (B = 128 certainly suffices). Thanks to coding we can postulate that a decision problem is a subset of the set Nq for some q. When speaking about decision problems, we alternate between set theoretic terminology where we have intersections, complements etc., and logical terminology where we have conjunctions, negations etc. A set-theoretic name for existential quantification is projection. A set is recursively enumerable (RE) if it is the projection of a recursive sets. An example of an RE set is the set of all sentences provable in Q.
Dec 7th, 2023
The Σ-completeness theorem: a Σ-sentence (both assumptions are crucial) valid in ℕ is provable in Q. The claim that a Δ0-sentence is never independent of Q is an easy consequence of this theorem, but it actually acted as one step in its proof.
Dec 5th, 2023
Quantifier elimination can be used to characterize sets definable in a structure (that admits quantifier elimination). Bounded formulas, i.e. Δ0-formulas, of the arithmetic language. Many useful properties of natural numbers (concerning divisibility, primes, powers of two) can be expressed via Δ0-formulas. The collection of sets and relations definable in ℕ by Δ0-formulas is denoted by Δ0. Or by Δ0 with ℕ in the superscript.
Nov 30th, 2023
Examples of axiomatizable classes and classes that are not axiomatizable. The complement of a finitely axiomatizable class C, i.e. the class of all structures for the given language that are not in C, is again finitely axiomatizable. Definable sets and definable elements of a structure.
Homework. Exercises 10–13 are not so difficult and they are partly already solved. 14 and 17 are hopefully illustrative but also not very difficult. 15 and 16 are more tricky. Please pick some of these and send a solution or questions concerning them.
Nov 28th, 2023
General Łoś-Vaught test: if T is consistent, has no finite models and is κ-categorical for some uncountable κ, then it is complete. SUCC is an example of a theory to which this theorem is applicable. Axiomatizable and finitely axiomatizable classes of structures. Example: if L is an arbitrary language, then the class of all finite structures for L is not axiomatizable. This is an almost immediate consequence of the theorem saying that if T has unboundedly large finite models, then it also as infinite models.
Nov 23rd, 2023
Review of semantic results and their consequences: Weak Löwenheim-Skolem theorem, Weak Łoś-Vaught test (we already discussed it on Tuesday), the compactness theorem. If T has unboundedly large finite models, then it also has infinite models. It T has infinite models, then it has models of any cardinality κ ≥ |L| + ℵ0. A consequence is that Th(〈N,+,0,s〉) has models of any infinite cardinality. It is clear that the order type of an uncountable model of this theory is  ω + (ω* + ω) · λ where λ is a dense linear order. It remains to prove the existence of countable nonstandard models of this theory.
Nov 21st, 2023
Vaught (Łoś-Vaught) test: if T is consistent, its language is at most countable and every two at most countable models of T are isomorphic, then T is complete. There are not so many theories to which this test is applicable. One example is DNO, the theory of dense linear order with no endpoints.
Nov 16th, 2023
Quantifier elimination for the theory DOS. Other classroom examples of structures that admit quantifier elimination (i.e., from which a theory admitting quantifier elimination can be spotted out) are 〈R,<〉 and 〈R,+,0,1〉. More difficult examples, important in the history of logic, are as follows. In 1929 Presburger showed that 〈N,+,0,s〉 admits quantifier elimination. The theory of this structure is called Presburger arithmetic. Later Tarski showed the same about the structure ℝ of the reals (with both addition and multiplication). For more about the history (of quantifier elimination) see the paper Doner-Hodges and Tarski's bibliography by Givant. They cite Tarski's book published in 1948 but they also seem to suggest that Tarski obtained this result already in 1930. Probably not: the same Wilfred Hodges speaks here about the year 1949.
Homework. Exercise 19.
Nov 14th, 2023
DO, the theory of discrete linear order. The theory DOS is a conservative extension of DO. In fact, it is an extension by definitions. It is also a conservative extension of SUCC. Some notation for types of linear order: ω and η are shorthands for the types of 〈N,<〉 and 〈Q,<〉 respectively. Examples of models of DO are ω, ω + ω* + ω, and also ω + (ω* + ω) · λ where λ is any linear order.
Nov 9th, 2023
The remaining part of the proof of quantifier elimination for the theory SUCC. This theory is complete. It is clear that any two models of a complete theory are elementarily equivalent. That is, they do not differ in the validity of any sentence. In particular, 〈N,0,s〉 and 〈N,0,s〉 + 〈Z,s〉 are elementarily equivalent. There is no formula in the language {0,S} saying that “the number x is reachable from zero by finitely many steps of the successor function”. Contrary to what was said today, the book does not contain a brief proof of the quantifier elimination for SUCC, my apologies. It discusses a closely related theory DOS. This is a plan for the next talk.
Nov 7th, 2023
Three lemmas concerning the theory Q where the third of them says that every open sentence in the arithmetic language is either provable or refutable in Q. The same three lemmas clearly hold also for the theory SUCC. The theory SUCC admits quantifier elimination: every formula φ in the language {0,S} is SUCC-equivalent to a quantifier-free formula containing no other free variables than those occurring free in φ. To show this, it is sufficient to treat formulas of the form ∃ where ψ is a clause (a conjunction of literals).
Nov 2nd, 2023
The axioms Q1–Q9 of Robinson arithmetic Q. Facts about ≤ and < provable and unprovable in Q. A simple model with two nonstandard elements shows that the properties of operations (like the commutativity and distributivity) and of order (like the transitivity) are usually unprovable in Q. Robinson arithmetic is not a conservative extension of Q1–Q5.
Oct 31st, 2023
Extensions and conservative extensions of a theory. Q1–Q5 is a conservative extension of Q1–Q3. The axioms Q8 and Q9 concerning the unstrict and strict order. Example sentences provable and unprovable in Q1–Q5,Q8,Q9. A special case of conservative extension is extension by definitions. Q8 and Q9 are definitions in this sense, and Q1–Q5,Q8,Q9 is thus a conservative extension of Q1–Q5 (and of Q1–Q3).
Oct 26th, 2023
Aspects of the completeness theorem: the strong completeness theorem is in fact a conjunction of two claims, the completeness theorem (no adjective) and the compactness theorem. The fact that the Zermelo-Fraenkel set theory, if it is consistent, also has countable models is called Skolem's paradox. However, there is nothing paradoxical about it. The axioms Q4 and Q5. Example sentences provable from Q1–Q5.
Homework. Show that every model of Q1–Q3 has an expansion that is a model of Q1–Q5.
Hint. We know how each model of Q1–Q3 looks like: the standard part, which is isomorphic to 〈N,0,s〉, plus any number of finite loops of arbitrary sizes, plus any number of chains isomorphic to 〈Z,s〉.
Oct 24th, 2023
Many different models for various theories, some notation for them (like 〈N,0,s〉 + 〈Z,s〉 + 〈Z,s〉). The theory SUCC. The strong completeness theorem and the Löwenheim-Skolem theorem.
Oct 19th, 2023
Standard and nonstandard elements of structures in which at least Q1 and Q2 are valid. Standard and nonstandard models. Logically valid formulas. The consequence relation. Contradictory and consistent theories.
Homework. No homework is officially assigned. However, all exercises 1–11 are solvable now. Anyone who can solve Exercise 4 obviously mastered the definition of the consequence relation.
Oct 17th, 2023
Tarski's definition. Lines concerning connectives imply that all tautologies are valid in every structure. The soundness of the generalization rules. The strong soundness theorem as a tool for proving unprovability.
Homework. Exercise 9.
Oct 12th, 2023
The deduction theorem. A review of semantic notions: valuation of variables in a structure, formula satisfied by a valuation in a structure, formula valid in a structure. The soundness theorem.
Oct 10th, 2023
A survey of Hilbert-style calculus HKe. A formal proof of x(P(x) → ∀yP(y)) in the theory with no axioms and of xy(S(y) ≠ x) in the theory having Q1 and Q2 as axioms.
Homework. show that also x(∃yP(y) → P(x)) has a formal proof.
Oct 5th, 2023
More examples of informal and formal proofs. The generalization rules. Numerals.
Homework. Construct formal proofs of some (not necessarily all) formulas in Exercise 1.
Oct 3rd, 2023
A review of logical syntax: from terms to sentences and axiomatic theories. Terms, formulas, axiomatic theories. A sample theory having Q1 and Q2 as axioms.
Homework. Think about an informal proof of the sentence numbered (iii).

Arithmetics and algorithms

Exercises (updated May 19, 2024).

SIS ALG110008, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení cvičení 8 a dalších libovolně zvolených 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. Kromě termínů vypsaných v SISu se lze domluvit i na jinou dobu, ale ve středu obvykle mohu až tak od 17h, a v pátek pouze ráno a pouze možná. Všechny termíny lze využívat i jako konzultace.

Course contents in Spring 2023/24 (Czech)

14. května 2024
Chybějící část důkazu z minulé přednášky: když m je prvočíslo a a∈Φ(m) má řád k, pak každý prvek b řádu k se rovná některému ai pro i<k. Avšak když i je soudělné s k, pak ai nemá řád k. Takže počet prvků řádu k je nejvýše φ(k).
7. května 2024
Několik poznatků, které se skládají na tvrzení, že když m je prvočíslo a k je dělitel čísla m - 1, pak v grupě Φ(m) je přesně φ(k) prvků řádu k. Toto bylo téměř ale ne zcela dokončeno. Dokončení a vysvětlení, jak na základě těchto úvah definovat certifikát pro prvočíslo, je (kromě konzultace na jakékoliv téma), plánem na Út 14.5.
25. dubna 2024
Mersennova čísla a Mersennova prvočísla. Výsledek Franka Colea z roku 1903, že jedním z dělitelů čísla 267 - 1 je  193 707 721, umožňuje neformálně vysvětlit, co je třída NP. Úloha U je ve třídě NP, jestliže pro ni lze definovat krátká data (certifikát), která když jsou pro daný vstup x předložena, lze z nich a z x polynomiálním algoritmem potvrdit, že xU. Jinými slovy, úlohy ve třídě NP jsou úlohy s efektivní verifikovatelností pozitivních instancí. Certifikát pro složené číslo větší než 2 je přirozené definovat jako (některý) dělitel onoho čísla. Takže množina všech složených čísel větších než 2 je úlohou ve třídě NP. Třída P všech polynomiálně rozhodnutelných úloh je podtřídou třídy NP. Řády prvků v grupách. Řád libovolného prvku grupy Φ(m) musí být dělitelem čísla φ(m). Úvahy o řádech směřují k výsledku, že i množina všech prvočísel je úlohou ve třídě NP. Což je (na rozdíl od celkem nedávného silnějšího výsledku, že množina všech prvočísel je dokonce úlohou ve třídě P) fakt na školní úrovni celkem dosažitelný.
23. dubna 2024
Výpočet čísla φ(m) na základě seznamu prvočísel v prvočíselném rozkladu čísla m. Šifrovací metoda RSA. K jejímu prolomení by stačil polynomiální algoritmus pro nalezení prvočíselného rozkladu. Stačil by i algoritmus pro výpočet funkce φ, ale ani jeden z takovýchto algoritmů není znám (protože pravděpodobně neexistuje).
16. dubna 2024
Důkaz čínské zbytkové věty. Počítání s modulárními reprezentacemi. Pseudoprvočísla.
Cvičení. Ověřte pomocí počítání s modulárními reprezentacemi, že 567 je pseudoprvočíslo. Číslo 641, které pravděpodobně bylo zmíněno v přednášce, pseudoprvočíslem není (protože je to prvočíslo). Ale s užitím faktu, že v ℤ43 platí 214 = 1, by šlo ověřit, že 645 je pseudoprvočíslo.
9. dubna 2024
Nejen určování invertibility v ℤm a výpočet inverzního prvku jsou polynomiálně počitatelné. Také pro umocňování, tj. pro výpočet funkce [m,x,z] ↦ Mod(zx,m) existuje polynomiální algoritmus. Eulerova grupa a Eulerova funkce. Eulerova věta: pro libovolné m a libovolné x∈Φ(m) platí xφ(m) = 1. V tomto tvaru ji budeme potřebovat, ale přehlednější důkaz má trochu obecnější verze: v komutativní grupě s n prvky umocnění libovolného prvku na n-tou dá jedničku čili neutrální prvek té grupy. Modulární reprezentace.
2. dubna 2024
Dva důsledky Bézoutovy věty, tj. dvě tvrzení dokazatelná v teorii, jejímiž axiomy jsou Bézoutova věta a axiomy obory integrity: ekvivalentní podmínka pro nesoudělnost a fakt, že každé ireducibilní číslo je prvočíslem. To druhé je domácí úkol kontrolovaný (až) u zkoušky. Eukleidův algoritmus lze užít k rozhodnování o invertibilitě v ℤm. Jeho čtyřsloupcovou variantu lze užít k výpočtu inverzního prvku. Když m je prvočíslo, pak ℤm je těleso. Není-li m prvočíslo, pak ℤm není ani obor integrity.
26. března 2024
V libovolném oboru integrity platí, že každé prvočíslo je ireducibilní. Rozšířený (čtyřsloupcový) Eukleidův algoritmus. Z něj (z jeho analýzy) plyne Bézoutova věta pro strukturu celých čísel: ke každé dvojici a a b existuje dvojice x a y taková, že ax + by je společným dělitelem (je jasné, že největším společným dělitelem) čísel a a b.
19. března 2024
ℤ a ℚ[x] jako příklady oborů integrity. Také každé těleso je oborem integrity. Nenulovým prvkem lze v oboru integrity krátit. Dělitelnost v oborech integrity: asociované prvky, dělitelé jedničky, nesoudělnost, největší společný dělitel. Prvky x a y jsou spolu asociované, právě když xy a yx.
12. března 2024
Definice okruhu a příklady: ℚ, ℤ, ℤm a ℚ[x]. Invertibilní prvky komutativního monoidu tvoří pod-monoid, který je grupou. V případě (multiplikativní části) okruhu ℤm se tato grupa nazývá Eulerovou grupou čísla m a značí se Φ(m). Například nosná množina grupy Φ(15) je {1,2,4,7,8,11,13,14}.
5. března 2024
Eukleidův algoritmus pracuje v polynomiálním čase. Monoidy a inverzní 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í? Uvažujte (nekomutativní) monoid všech funkcí z tříprvkové množiny {a,b,c} do sebe. Je funkce {[a,a],[b,a],[c,b]} invertibilní? Je {[a,c],[b,a],[c,b]} invertibilní?
27. února 2024
Vlastnosti relací obecně, vlastnosti relace dělitelnosti. Na x(x ∣ 0)xyz(xy → (xy+zxz)) lze založit ověření, že Eukleidův algoritmus správně počítá úlohu GCD, tj. že k libovolným dvěma číslům nalezne jejich největšího společného dělitele. Ale lze uvažovat i opačným směrem a z korektnosti Eukleidova algoritmu odvodit čistě matematický poznatek: ke každým dvěma číslům existuje jejich společný dělitel, který je dělitelný všemi jejich (ostatními) společnými děliteli.
20. února 2024
Úloha a algoritmus jako základní pojmy teoretické informatiky. Časové nároky algoritmů. Školní algoritmus pro úlohu Mult pracuje v kvadratickém čase, školní algoritmus pro sčítání dokonce v lineárním čase. Pro algoritmy, které pracují v linárním, kvadratickém, kubickém atd. čase máme souhrnný název polynomiální algoritmy. Úlohou, pro kterou polynomiální algoritmus neexistuje, je pravděpodobně Factoring, čili úloha nalézt prvočíselný rozklad daného čísla. Ale dokázané to není, nalezení důkazu je otevřeným problémem. Dva algoritmy, který bychom dostali modifikací těch algoritmů pro úlohu Primes, které byly uvedeny v přednášce, pracují v exponenciálním čase, takže polynomiální rozhodně nejsou.

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 2nd, 2024) list of exercises.

SIS ALG119007, Zoom.

Exams (Czech)

Please be ready to discuss any of the 14 exercises. However, the exam requirements end with the proof of Löb's theorem. Further consultation and exam days (other than given in SIS) are possible.

Course contents in Spring 2023/24

May 16th, 2024
Solovay's completeness theorem for GL: a modal formula A is provable in GL if and only if it is a PA-tautology. We did not discuss the completeness of another logic, sometimes denoted by GLS. It is complete with respect to ℕ-tautologies, and the proof is very similar and is also contained in Solovay's paper.
May 14th, 2024
Soundness of GL w.r.t. Kripke semantics (finished). The proofs of completeness and of finite model property are skipped. However, they have a clear consequence: GL is decidable. A plan for the next talk is Solovay's arithmetic completeness proof: a finite Kripke counterexample for a modal formula A can be converted to an arithmetic counterexample, i.e. to an arithmetic valuation ∗ such that PA ⊬ A.
May 7th, 2024
Two variants of the substitution theorem are provable in K4. An application of GL in metamathematics: a solution of a Gödelian self-reference equation (like Gödel's, Henkin's or Löb's sentence) is uniquely determined. A sentence is obtained by Gödelian self-reference if the claim it says about itself can be expressed using the formula Prπ(x), which can be nested, parameters, and nothing else. However, a general unique solvability theorem is not true. This is clear from some exercises. Kripke semantics for GL: it is sound w.r.t. the class of all transitive and reversely well-founded frames (to be finished). Some connections of reverse well-foundedness and irreflexivity: a well-founded frame is irreflexive, and a finite transitive and irreflexive frame is reversely well-founded.
May 5th, 2024
Logic GL can be defined by two equivalent ways, as the extension of K4 by Löb's rule, or the extension of K4 by Löb's axiom scheme. The latter is preferable in the literature.
May 2nd, 2024
An alternative proof of Löb's theorem. Modal formulas, PA-tautologies and ℕ-tautologies. Modal logics K and K4. Löb's rule and Löb's axiom scheme.
Apr 25th, 2024
As we know, if T and τ(z) are as usual, then (T+Con(τ)) can prove the unprovability of the sentence Con(τ). However, (T+Con(τ)) cannot prove the independence of the sentence Con(τ). This is an example on the situation where Gödel's second theorem works as a technical tool used in some proof. Henkin's question concerning a self-referential sentence asserting its own provability. Löb's solution: all such sentences are provable.
Apr 23rd, 2024
Some connections to Gödel's second theorem. First, Paris and Harrington and some other authors exhibited sentences that are independent of PA and speak about numbers, not about formalized logic. There is a link from these results to Gentzen who considered the question what arithmetic axioms, if added to PA, make it possible to prove the consistency of PA. Second, reasoning about self-referential sentences can be simulated in modal logic, and modal logic even has some applications in that reasoning. And third, most philosophers agree that Gödel's result in fact refutes Hilbert's program, but the opposite opinion and further considerations are still possible. While PA cannot prove its own consistency, some consistency proofs in PA are possible. For example, PA ⊢ Con(∅).
Apr 18th, 2024
Gödel's second incompleteness theorem. It is often cited as follows: no sufficiently strong recursively axiomatized theory can prove its own consistency. More exactly, if τ(z) is Σ and defines T (in which case T must be recursively axiomatizable), and T is consistent, then T ⊬ Con(τ). In particular, PA ⊬ Con(π) where π is the natural definition of PA in ℕ.
Apr 16th, 2024
The self-reference theorem. Formalized Σ-completeness theorem. Gödel's self-referential sentence asserting its own unprovability.
Apr 11th, 2024
The formulas Prτ(x) and Con(τ). Facts about formalized provability and formalized consistency provable in PA. Löb's derivability conditions.
Apr 9th, 2024
Formulas describing further syntactic notions. They can be used to write down a formula Proofτ(x,w) containing a formula τ(z) as a subformula. If τ(z) is Σ or Δ0, then Proofτ(x,w) is PA-equivalent to a Σ1-formula (that is, is Σ1(PA)), or is Δ0 respectively. If τ(z) defines T, then Proofτ(x,w) defines the set of all pairs [φ,m] such that m is a proof of φ in T.
Apr 4th, 2024
String functions in PA. Formulas Var(v) and Term(t). They express the property "the number v is a variable" and "the number t is a term", respectively, in the arithmetic language. Writing down the former is straightforward (using Euclidean division and the exponential function), but defining terms involves speaking about balanced strings and quasiterms. Both formulas are Δ0.
Apr 2nd, 2024
Formalization in arithmetic (arithmetization) of a notion involves finding a formula that defines the notion in ℕ and proving in PA that the notion, if described by that formula, has the expected properties. Notions formalizable in PA include primes (irreducibles), powers of two, Euclidean division and the function NPB. Most of these notion are formalizable already in IΔ0. The exponential function is formalizable, but the sentence ∀xy(y=2x) is not provable in IΔ0. It is not known whether the fact that there are infinitely many primes is provable in IΔ0. If two formulas define the same set in ℕ, then they are (of course) Th(ℕ)-equivalent, but they may be PA-inequivalent.
Mar 26th, 2024
Euclidean division in PA. The claim that there are infinitely many irreducible numbers (before we prove that being irreducible is the same as being prime, we distinguish between the two notions) is expressible in the arithmetic language. In fact the classical (Euclid's) proof is formalizable in PA, but is seems adequate to avoid speaking about the factorial function and about the prime factorization of a number. The fact that every nonzero number is the product of some irreducible numbers is objectionable since it is an infinite disjunction and thus it is problematic to consider it a sentence.
Mar 21st, 2024
The relationship between the schemas LNP and Ind. A model showing that they are not equivalent over Q.
Mar 19th, 2024
Peano arithmetic PA and provability in it: both operations are commutative and associative, · is distributive over +, both cancellation rules hold, the strict order is transitive, irreflexive and linear, the unstrict order relates to the strict order as expected, and also the interaction of the order relations and the operations is as expected.
Homework. Using the fact that a consistent decidable theory has a complete decidable extension show that a theory T is essentially undecidable (in the sense that every consistent extension of T is undecidable) if and only if T is essentially incomplete (in the sense that every recursively axiomatizable extension of T is incomplete).
Mar 14th, 2024
A finally finished full proof of Rosser's theorem: if T is any consistent recursively axiomatizable extension of Q, then T is incomplete (if fact, already some Σ1-sentences are independent) and undecidable (more than that, Thm(T) and Ref(T) are recursively inseparable RE sets).
Mar 12th, 2024
An addendum to Gödel's 1st theorem: if T satisfies the assumptions, then Thm(T) is Σ1-complete (in the sense that every RE set is m-reducible to it). So it is one of the algorithmically most complicated RE sets. A finite extension of a decidable theory must again be decidable. From this it follows that the set of all logically valid arithmetic formulas is not decidable. Thus predicate logic is not decidable in general. However, there are some special cases that are decidable. For example, if the language consists of only finitely many unary predicate symbols. Rosser's theorem (to be finished or repeated): the claim of Gödel's 1st theorem remains true if Σ1-soundness is replaced by mere consistency.
Mar 7th, 2024
Since every RE set is m-reducible to Th(ℕ) and sets in REΠ1 exist, Th(ℕ) is not Π1. Since the arithmetic hierarchy does not collapse (sets in ΣnΠn exist for every nonzero n), this argument can be repeated at every level n≠0: Th(ℕ) is not Πn. The whole fact is cited as Tarski's theorem on the undefinability of truth: arithmetic truth (the set of all formulas valid in ℕ) is not arithmetical (is not in the union of all Πn, which equals the union of all Σn; or put otherwise, no formula defines it in ℕ). Gödel's 1st incompleteness theorem: if T is a Σ1-sound extension of Q, then T is undecidable (and thus) incomplete. There exist independent sentences that are as simple as Σ1 (or Π1).
Mar 5th, 2024
We know that if T is recursively axiomatizable, then Thm(T) is RE. Craig's theorem (known as Craig's trick) says that the opposite is also true: if Thm(T) is RE, then there exists a recursive is S equivalent to T. If is T is recursively axiomatizable and complete, then it is decidable. Therefore, SUCC, DNO and other theories from the Fall semester are decidable. All their models (like ω + (ω* + ω) · ω) are decidable structures. Any finite structure for a finite language is decidable. If AREΔ1 and φ(x) is a Σ1-formula that defines it, then the equivalence n(nAφ(\bar{n})∈Th(ℕ)) shows that Am Th(ℕ). Thus ℕ is an undecidable structure.
Feb 29th, 2024
Course-of-values recursion and some examples on its use. (i) Hofstadter's function is recursive. (ii) For every recursive function g of one variable such that Rng(g) is infinite there exists a one-to-one recursive function f having the same range. This fact is a key step in proving a characterization of RE subsets of N: a set A ⊆ N is RE if and only if it is finite or it is the range of some one-to-one recursive function. (iii) The set of all terms (in the arithmetic language) is recursive. From this it is possible to continue to other syntactic notions (formulas, free and bound variables etc.) and conclude that if T is recursive or RE, then the binary relation "d is a proof of φ in T" is recursive or RE respectively.
Feb 27th, 2024
A set A ⊆ N is m-reducible to a set B ⊆ N, which we denote by Am B, if there exists a recursive function f such that n(nAf(n)∈B). If Am B and B is Σ1 (or Π1, or Δ1), then A is Σ1 (or Π1, or Δ1 respectively). The function computing the number of primes less than n is clearly recursive, but it is not known whether its graph is Δ0.
Feb 22th, 2024
The graphs of the functions [x,z] ↦ zx and [x] ↦ NPB(x) are Δ0-definable. A function derived from a (partial) recursive function via primitive recursion must again be (partial) recursive.
Feb 20th, 2024
The graph of the functions Div and Mod are Δ0-definable. Also the graph of the function [x,z] ↦ zx is Δ0-definable (to be finished).

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


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

Smorynského článek Hilbert's Programme (Adam Fürstenzeller, od 14.12., 2 přednášky)
Abstrakt (poskytnutý přednášejícím): Smoryńského článek popisuje situaci, ve které se matematika jako vědecká disciplína ocitla na začátku dvacátého století. Mezi matematiky se vedly diskuse týkající se formulování samotných základů této vědní disciplíny. Jednou z teorií byl intuicionismus, za jehož zakladatele se považuje L. E. J. Brouwer, který ve své disertaci (1907) zformuloval základní myšlenky tohoto směru. Intuicionisté odmítali aktuální nekonečno a využívání aristotelské logiky, zejména zákonu vyloučení třetího, pro nekonečné objekty. Dalším rozšířeným směrem byl formalismus v čele s Davidem Hilbertem. Hlavní myšlenkou formalismu je budování bezesporných axiomatických teorií — sad axiomů, které úplně popisují danou matematickou teorii (věty a axiomy jsou pravdivé, když nejsou ve sporu se svými důsledky — nemusí se nutně jednat o “evidentní” pravdy).
Názorová rozepře mezi Hilbertem a Brouwerem je ústředním tématem celého článku. Smoryński důkladně popisuje jak osobní vztah hlavních dvou protagonistů, tak i ohlasy, které jejich práce vyvolaly. Počátkem dvacátých let získává Brouwer nové stoupence. Jedním z nich byl také H. Weyl, jehož přednáška z roku 1920 přiměla Hilberta znovu se plně věnovat práci v oblasti základů matematiky. Společně se svými stoupenci se snaží dokázat bezespornost aritmetiky (v širším smyslu, zahrnujícím i analýzu a teorii množin) — tzv. Hilbertův program. Ideový spor mezi Hilbertem a Brouwerem se postupně přesouvá i do osobní roviny. Jeho vrcholem je vyloučení Brouwera z Matematische Annalen, které inicioval Hilbert.
V průběhu dvacátých let 20. století předkládá Hilbert rozpracované důkazy Ackermanna a Von Neumanna a zdá se, že důkaz bezespornosti aritmetiky a s ním i dokončení Hilbertova programu je na dosah ruky. Zvrat však přináší rok 1931 a Gödelovy věty o neúplnosti. V první z nich Gödel dokázal, že každá bezesporná rekurzivně axiomatizovatelná teorie obsahující aritmetiku je neúplná (existuje v ní nezávislé tvrzení) a tím prokázal neuskutečnitelnost Hilbertova programu.
Eckart Menzler-Trott: Logic's Lost Genius — The Life of Gerhard Gentzen (Timea Cochová, od 30.11., 2 přednášky)
Zaoberali sme sa životným príbehom matematika a logika Dr. habil. Gerharda Gentzena. Od detstva, cez štúdium a prácu až po jeho tragickú smrť v Prahe. Nahliadli sme k jeho práci a komunikácii s matematikmi vtedajšej doby, ako boli napríklad Hilbert a Bernays. Z oficiálnych dokumentov, spovedí blízkych, pracovných a osobných listov sa dozvedáme o jeho charaktere a sledovali sme rozvoj jeho nápadov a práce. Taktiež sme si priblížili ako vyzerala veda a hlavne matematika a logika v nacistickom Nemecku a v zvyšku sveta.
Ukážky niektorých listov a dokumentov: PDF1, PDF2.
L. E. J. Brouwer: Life, Art and Mysticism (Šimon Pošta, 23.11., 1 přednáška)
Brouwerův výchozí bod Smutného světa, role člověka jako individua a jako člena kolektivu, zásadnost karmického řádu a jeho prohlédnutí skrze přivrácení se k sobě, druhy řečí, pravd a jejich vztah k vědám, speciálně k logice a matematice. K tomu podrobnější shrnutí.
Detlefsenův článek z roku 79 (Timotej Šujan, od 2.11, 1.5 přednášky)
Abstrakt (poskytnutý přednášejícím): Detlefsen v první části článku kritizuje takovou skeptickou interpretaci (SI) Gödelovy druhé věty (G2), která by se snažila dojít ke skeptickému závěru, že víru v konzistenci teorie T nelze odůvodnit důkazem sentence Con(T). Tvrdí, že tento závěr z G2 žádným zřejmým způsobem neplyne, a tedy je potřeba dokázat určité pomocné předpoklady SUP1 a SUP2. Následně se snaží ukázat, že platnost SUP1 vyvrací původní SI — v jeho argumentu jsou ústřední pojmy jako reflexivní teorie či (jeho vlastní pojem) epistemicky kompaktní teorie. V druhé části článku se snaží upravit SI tak, aby unikla ze spárů jeho kritiky, avšak následně i takovou upravenou SI odmítá jako nepodloženou. V třetí části krátce odmítá jako nepodloženou Resnikovu interpretaci G2 v kontextu “nejsilnějšího/nejsložitějšího systému, který jsme ještě ochotní vážně zkoumat”, a to i kvůli nejasnému popisu takového systému. V závěrečné části se pak snaží zachránit Hilbertův program tak, že představuje tzv. omezené ω-pravidlo, které je dle něj v souladu s finitními metodami, které Hilbertův program vyžaduje, a tvrdí, že např. Con(PA) je dokazatelné z PA+(ω-pravidlo).
Gödelův článek z roku 1931 (L. Clowez, od 19.10., 2.5 přednášky)
Kódování logické syntaxe, které je založeno na prvočíselných rozkladech přirozených čísel. Definice kalkulu poměrně podobná dnešní definici kalkulu hilbertovského. Gödel pracuje s axiomatickou teorií, která odráží takzvanou teorii typů. Viditelný rozdíl vůči dnešním přístupům je to, že nepracuje s nějakým předem fixovaným jazykem. Pouze trvá na tom, že k dispozici jsou symboly pro nulu a následnickou funkci. Článek pracuje s “rekurzívními” funkcemi, ale definici se shoduje s tím, čemu se dnes říká primitivně rekurzívní funkce (dnes víme, že rekurzívní funkce lze ztotožnit s funkcemi algoritmicky počitatelnými a je jich víc než primitivně rekurzívních). Jako celkem věrohodná tedy vypadá historická hypotéza, že kromě vět o neúplnosti je článek důležitý také tím, že v něm byly zavedeny primitivně rekurzívní funkce.
Dnešní pohled na Gödelovy věty (V. Švejdar, 2 týdny)
Trochu životopisných údajů ke Gödelovi. Ingredience důkazu jeho vět o neúplnosti: kódování syntaxe, numerály, definovatelné množiny, Σ-formule a věta o Σ-úplnosti, predikát dokazatelnosti, věta o autoreferenci.

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