V.Š. V.Š.

Introduction

About me

Associate professor at the Department of Logic, College of Arts ("Faculty of Arts"), Charles University in PragueFilozofická fakulta UK, Palachovo nám. 2, 11638 Praha 1. Courses Computability (an introduction to recursive functions), Classical Logic II (with an emphasis on incompleteness and undecidability), and some others related to metamathematics or to algorithms.

Research interests

Interpretability of axiomatic theories, arithmetization, related modal logics, algorithmic aspects of non-classical logics.

Experience and education

During 1982-90 worked as a software developer for an industrial company ČKD Polovodiče. Participation in writing a control system for PDP-11 computers. The system was designed by Jan Pavelka*)Accidentally the same Jan Pavelka who, a few years before turning into a respected software developer, wrote innovative papers about fuzzy logics., and was successfully applied in several branches of industry like steel rolling or international transport of natural gas.

Ph.D. in mathematical logic, Ph.D. study in the Institute of Mathematics of the Academy of Sciences of the Czech Republic. Dissertation Self-Reference and Modal Logic, 1982, supervisor Petr Hájek. Graduated in mathematics from Charles University, 1978, master's thesis Degrees of Interpretability.

Office info, events, miscellaneous updates

Office hours Thu 15:00, or by appointment. For more info please see the image above, or the web of the department.

Nabídka témat bakalářských a diplomových prací: TemataPraci13.pdf

Publications

BibTeX file

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

Book

Some workshop or conference presentations

Papers

Logic: Incompleteness, Complexity, and Necessity (Academia, 2002)

I do not think logic is a field where people are taught how to think logically. Instead, I consider it a theory about deductive thinking for people who already are able to think logically, usually because they have some experience with academic mathematics.

My ambition was to have more than a list of definitions, theorems, and proofs; I am trying to include comments and explanations, and I believe that the reader should be led from some questions to some solutions.

I am grateful to Petr Hájek, who was my teacher and who gave one of the initial impulses for writing this book. He actually wrote only a small part of the text, but much larger part and perhaps everything was inspired by him.

As a result of an agreement with the Academia publishing company, a pdf version of the book is now available (full text!) for study purposes (only!). When downloading the file, it is recommended to download also Errata and save both files to the same folder on local computer. That will activate the links in the text marked by big red 'E'. Redistribution and modifications of the file are not allowed! Printing of (any part of) the document is not allowed!

Po domluvě s nakladatelstvím Academia je nyní plný text knihy ve formátu pdf přístupný pro studium (pouze!). Při kopírování souboru na lokální počítač je doporučeno stáhnout také Errata a umístit oba soubory do téže složky. Soubor nesmí být dále šířen ani nesmí být modifikován! Žádná jeho část nesmí být tištěna!

Click on the blue word 'Academia' on the first page of the book to obtain further information about their bookstores and other books they publish.

Comments and additions to Errata are welcome.

Modal and non-classical logics

SIS ALG119008, Zoom cuni-cz.zoom.us/j/99702828164.

Course contents in Fall 2022/23 (Czech)

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.

Exercises

Please pay attention to the list of exercises.

Course contents in Fall 2022/23 (Czech)

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.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení třinácti cvičení (i s vysvětlením matematického či algoritmického pozadí). Zkouška pak pokračuje prodiskutováním některého důkazu. Letos lze průběh zkoušky domluvit i individuálně, ale na prodiskutování některého důkazu, třeba i předem domluveného, by dojít mělo. Termín zkoušky lze domluvit mailem, preferuji Út celkem kdykoliv, Po a St navečer a Pá ráno.

Course contents in Spring 2021/22 (Czech)

17. května 2022
Číslo 261 - 1 je prvočíslo. Postup lze zobecnit na zdůvodnění, že Primes je úloha ve třídě NP.
10. května 2022
Úlohy ve třídě NP. Mersennova čísla a Mersennova prvočísla. Řády prvků v grupách obecně a v Eulerových grupách zvláště.
3. května 2022
Výpočet hodnoty Eulerovy funkce: stačí vědět pouze seznam prvočísel v rozkladu daného čísla, bez jejich exponentů se lze obejít. Příklady na užití modulárních reprezentací a Eulerovy věty. Jeden reálný příklad: kryptografická metoda RSA.
26. dubna 2022
Eulerova (Fermatova) věta: v každé konečné komutativní grupě s n prvky platí x(xn = 1).
19. dubna 2022
Ekvivalentní podmínka pro nesoudělnost: nenulová čísla a a b jsou nesoudělná, právě když z(abzaz). Modulární reprezentace a Čínská zbytková věta. Užití modulárních reprezentací k důkazu, že číslo 341 je pseudoprvočíslo.
12. dubna 2022
Teoreticko-informatický důsledek čtyřsloupcového algoritmu: o invertibilitě v ℤm lze rozhodnout a inverzní prvek invertibilního prvku lze nalézt v polynomiálním čase. K tomu patří dodatek, že pro  x∈ℤm a přirozené číslo k lze mocninu xk také nalézt v polynomiálním čase. Matematický důsledek Bézoutovy věty: v ℤ platí, že každé ireducibilní číslo je prvočíslo.
5. dubna 2022
Zobecněný (čtyřsloupcový) Eukleidův algoritmus.
29. března 2022
Ještě tělesa a obory integrity. A ještě jednou základní pojmy dělitelnosti: nesoudělnost, ireducibilní prvky, prvočísla.
Cvičení. Dokažte, že každé prvočíslo je ireducibilní.
22. března 2022
Opakování: modulární aritmetika, inverzní a opačné prvky v okruzích. Tělesa a obory integrity. Rozdíl mezi logickými principy a axiomy teorie.
15. března 2022
Vlastnosti opačných prvků v okruzích. Modulární aritmetika. Invertibilní prvky v různých okruzích (podrobně byla z tohoto hlediska prozkoumána struktura ℤm). Tělesa. Obor integrity jako struktura vhodná pro zkoumání dělitelnosti. Základní pojmy teorie dělitelnosti: asociované prvky, nesoudělnost, největší společný dělitel, ireducibilní prvky, prvočísla. Například x a y jsou podle definice nesoudělná, jestliže každý jejich společný dělitel je invertibilní (čili je dělitelem jedničky).
8. března 2022
Eukleidův algoritmus pracuje v polynomiálním čase. Definice komutativního okruhu a bezprostřední důsledky axiomů. Opačné a inverzní prvky.
1. března 2022
Úlohy PrimesFactoring. Pojem polynomiálního algoritmu. Eukleidův algoritmus a jeho matematický důsledek: pro každá dvě přirozená čísla existuje jejich společný dělitel, který je dělitelný všemi jejich společnými děliteli.
22. února 2022
Úlohy a algoritmy. Školní algoritmus pro úlohu Násobení neboli Mult. Jeho časové nároky. Dva algoritmy pro určování, zda dané číslo je prvočíslo. Oba bohužel, a to na rozdíl od školního algoritmu pro násobení, pracují v exponenciálním čase.

Huge number calculator

The calculator BNCalc.pdf is implemented as a (set of scripts behind a) pdf document and can be used for operating with really huge integers. Note that there are some undocumented key combinations that make it easier to repeat the given operation. The "result" text field in the "Factoring" page, marked by an arrow in this image, accepts Shift‑M (or Shift‑B with the same meaning). Also, the result text field on the preceding page accepts Shift‑M and Shift‑B.

Incompleteness and Gödel Theorems

Here is an (updated May 24th) list of exercises.

SIS ALG119007, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení čtrnácti cvičení. Termín zkoušky nebo konzultace lze domluvit individuálně mailem, preferuji Út celkem kdykoliv, Po a St navečer a Pá ráno.

Course contents in Spring 2021/22

19. května 2022
Tři prenexní implikace, které nejsou intuicionisticky logicky platné. Jedna z nich, týkající se disjunkce a univerzálního kvantifikátoru, ale platí ve všech strukturách s konstantním univerzem. Schéma DNS ukazuje, že finite model property pro intuicionistickou predikátovou logiku neplatí. Predikátová varianta kalkulu GJ.
17. května 2022
Korektnost kvantifikátorových pravidel kalkulu GK, dokončení. Kripkovská sémantika intuicionistické predikátové logiky.
12. května 2022
Příklady důkazů v predikátové verzi kalkulu GK. Korektnost kvantifikátorových pravidel.
10. května 2022
Glivenkova věta. Kvantifikátorová pravidla kalkulu GK.
5. května 2022
Úplnost kalkulu GJ vůči kripkovské výrokové sémantice. Dva důležité vedlejší produkty důkazu: pro výrokovou variantu kalkulu GJ platí věta o eliminovatelnosti řezů, a výroková kripkovská sémantika má finite model property: každá formule, která má jakýkoliv kripkovský protipříklad, má i konečný protipříklad.
3. května 2022
Kalkulus GJ pro intuicionistickou výrokovou logiku. Příklady důkazů. Bezřezové důkazy. Vlastnost podformulí (subformula property): každá formule v bezřezovém důkazu je podformulí některé formule ve finálním sekventu.
28. dubna 2022
Intuicionistické tautologie, protipříklady. Inkluze IntTaut ⊆ Taut. Dvě modelové konstrukce: podmodel generovaný prvkem a amalgamace. Disjunction property.
26. dubna 2022
Kripkovská sémantika intuicionistické logiky.
21. dubna 2022
Korektnost a úplnost gentzenovského kalkulu GK vůči sémantice klasické výrokové logiky. Vlastnost podformulí (subformula property), věta o eliminovatelnosti řezů.
19. dubna 2022
Příklad definice τ(z) množiny axiomů Peanovy aritmetiky takové, že z ní vytvořená sentence Con(τ) je v PA dokazatelná. Pravidla gentzenovského výrokového kalkulu.
14. dubna 2022
Rosserova věta. Craigův trik. Podstatná neúplnost neboli podstatná nerozhodnutelnost Robinsonovy aritmetiky.
12. dubna 2022
Některé souvislosti Druhé Gödelovy věty. Hilbertův program.
7. dubna 2022
Klasický důkaz První Gödelovy věty (založený na větě o autoreferenci). Druhá Gödelova věta.
Cvičení. Dokažte, že Gödelova sentence ν sestrojená k teorii T a její Σ-definici τ je T-ekvivalentní se sentencí Con(τ). Aritmetická sémantika modální logiky. ℕ-tautologie a logika GLS.
5. dubna 2022
Věta o autoreferenci.
31. března 2022
Vlastnosti formalizované dokazatelnosti dokazatelné v PA. Formalizace konečně axiomatizovatelných teorií, například Robinsonovy aritmetiky. Formule π(z) formalizující v PA axiomatiku PA. Podmínky pro dokazatelnost (Löb's derivability conditions).
29. března 2022
Formalizace syntaktických pojmů v PA: od proměnných a termů k dokazatelnosti a bezespornosti. Aritmetizace logické syntaxe. Textové řetězce, operace s nimi, vyvážené řetězce, proměnné, termy.
24. března 2022
Aritmetizace logické syntaxe. Textové řetězce, operace s nimi, vyvážené řetězce, proměnné, termy.
22. března 2022
Množina všech rekurzívních funkcí je uzavřena na operaci primitivní rekurze: dokončení a shrnutí. Dvě důležité funkce, totiž [x,z] ↦ zxx"počet jedniček v binární expanzi čísla x" mají dokonce Δ0-definovatelný graf. Jejich vlastnosti, například zx+y = zx·zy, jsou dokazatelné v PA.
15. března 2022
Bezestrojová (čistě logická) definice RE množin, rekurzívních množin a rekurzívních funkcí.
10. března 2022
Struktura nestandardního modelu PA. Aritmetická hierarchie. Množiny Σm(PA) a Πm(PA) jsou uzavřeny na konjunkci, disjunkci a omezenou kvantifikaci. Navíc Σm(PA) je uzavřena na ∃, Πm(PA) je uzavřena na ∀. Každá aritmetická formule je ekvivalentní s nějakou Σm-formulí (tím ovšem i s nějakou Πm-formulí).
8. března 2022
V PA lze dokázat, že prvočísla jsou přesně ta čísla, která jsou ireducibilní. Dále lze dokázat vlastnosti mocnin dvojky: dělitel mocniny dvojky je opět mocnina dvojky, součin dvou mocnin dvojky je mocnina dvojky, pro každé dvě mocniny dvojky platí, že některá z nich je dělitelem druhé, a když s je mocnina dvojky, pak mezi s a 2s není žádná jiná mocnina dvojky.
3. března 2022
V PA lze dokázat, že ireducibilních čísel je nekonečně mnoho. Dále lze dokázat větu o dělení se zbytkem a Bezoutovu větu.
1. března 2022
Existuje model demonstrující, že nad samotnou Robinsonovou aritmetikou schémata Ind a LNP ekvivalentní nejsou.
24. února 2022
Schémata Ind a LNP jsou nad teorií (Q + ∀x(x<S(x))) ekvivalentní.
22. února 2022
Peanova aritmetika PA. Užití schématu Ind k dokazování očekávaných vlastností operací a uspořádání.

Chapters in Classical Logic

About

A seminar partly based on students' presentations, devoted to various topics in metamathematics, non-classical logics, and proof theory. The topics usually include: Provability Logic, independence of the Paris-Harrington combinatorial principle over Peano arithmetic, relations between ZF, GB and the Kelly-Morse set theories, upper and lower bounds for cut-elimination in classical predicate logic, decision procedures for intuitionistic propositional logic. Here is the list of topics (in Czech). SIS: ALG500003.

Course contents in 2022/23 (Czech)

Aritmetická úplnost logiky dokazatelnosti (V. Švejdar, 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.
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

About

A seminar based on students' presentations, devoted to reading papers mainly by Smorynski and Detlefsen. Here is the course announcement (in Czech). SIS: ALGV19006, Zoom.

Course contents in 2021/22 (Czech)

Detlefsenův článek z roku 1979. (J. Štefanišin, 16. prosince)
Skeptická interpretace Druhé Gödelovy věty. Údajný destruktivní vliv Druhé Gödelovy věty na Hilbertův program.
Detlefsenův článek z roku 1990. (J. Rýdl, 3 lekce od 25. listopadu)
První, a pak druhá prezentace.
Smorynského článek Hilbert's Programme v CWI Quarterly. (J. Urbánek, 3 lekce od 4. listopadu)
Hilbert jako autor metody matematické práce, která se dá popsat jako axiomatizace. Hilbertův plán prokazovat bezespornost teorií takzvaně finitně, čili v podstatě počítáním symbolů v syntaktických zápisech a případně použitím indukce. Brouwer jako výrazná osobnost jak ve filosofii matematiky, tak v matematice samé. Na znění a interpretaci Hilbertova programu lze usuzovat ze tří Hilbertových přednášek (třetí v Lipsku v roce 1922). Gödelovo oznámení jeho věty o neúplnosti na konferenci v Königsbergu. Handout, který Jan Urbánek poskytl k přibližně druhé půlce přednášky.
Gödelův článek z roku 31 (D. Roubínek, 3 lekce od 7. října)
Gödelův popis systému P odvozeného z Principia Mathematica. Čtyřicet pět primitivně rekurzívních a jedna rekurzívně spočetná podmínka v Gödelově článku: od dělení se zbytkem k dokazatelnosti. Oddíly od VII výše se pravděpodobně týkají formalizace dokazatelnosti v systému P. Je zde definována Gödelova beta funkce. Dále je explicitně formulována Druhá věta o neúplnosti, což je odpověď na dříve kladenou otázku, zda o Druhé větě neměl být článek s římskou II v titulu. V závěru je diskuse o předpokladu týkajícím se ω-konzistence. Pro platnost Druhé věty opravdu potřebný není, ale pro Gödelův důkaz První věty o neúplnosti potřebný je.

Other activities

TeX/LaTeX, pdf, ...

FBUsersSetup

The Firebird SQL server comes with a command line utility gsec for manipulating database users. Using it, one can add, delete, or modify server's users, where a modification practically means a password change.

FBUsersSetup.exe is written as an Inno Setup Windows installer*)Unlike normal installers, it does not write anything to the registry and does not leave any trace on your computer. So no deinstallation is provided/needed. and it basically is a gui wrapper for the gsec utility. As such, it has little additional functionality in comparison to gsec. However, it is easy to use, it can modify users on any computer in or outside the local network, it never gets confused if there are parallel instances of Firebird running on the local computer, and it can detect the properties of the local Firebird(s).

The utility is rather self-explanatory, the essential dialog pages being

DBUSubst

The utility DBUSubst.exe can substitute one Firebird database user for another. A substitution of user M for existing user D in a database means that M becomes an owner of all database objects that user D owned, he inherits all privileges that were granted to D, and he becomes a grantor of all privileges that D granted. After being substituted out, user D grants and is granted nothing, and owns no database object. If D was an owner of a database then M becomes a new database owner. Thus user substitution is a more general operation than database ownership change.

Similarly as FBUsersSetup, DBUSubst.exe is written as a (harmless for your computer) Inno Setup Windows installer. It basically is a wrapper for the isql command line utility and some sql scripts. The scripts are available in DBUSubst.zip. They are documented and thus contain a detailed information about the substitution process. The document DBUSubst.pdf contains some introductory information about the user privileges and some Firebird internals. Two essential dialog pages of DBUSubst.exe are