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.

KGPreface.pdf je připravovaná předmluva k překladu Gödelových článků z r. 1930 a 1931, který vydá Katedra filosofie ZČU v Plzni. Všechny poznámky jsou vítány. KGPreface_p.pdf je úspornější verze, se dvěma stránkami na jeden list papíru.

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.

Computability

SIS ALG110010

Exams

Please pay attention to the list of excercises. It might extend and will be used during the exam.

Course contents in Fall 2016/17 (Czech)

1. prosince 2016
Množiny NE, Tot, Unb a Rec. Jejich aritmetická klasifikace. Tarského‑Kuratowského algoritmus. Definice a základní vlastnosti m‑převeditelnosti.
29. listopadu 2016
Univerzální Σn‑relace existuje pro každé nenulové n. Důsledkem je, že aritmetická hierarchie nekolabuje.
24. listopadu 2016
Částečně rekurzívní funkce, která nemá žádné rekurzívní prodloužení. Rekurzívně neoddělitelné dvojice rekurzívně spočetných množin.
D. cv. K této problematice se víceméně vztahuje cvičení 11(b): na rozdíl od RE‑množin, disjunktní Π1‑množiny vždy rekurzívně oddělitelné jsou.
22. listopadu 2016
Enumerace částečně rekurzívních funkcí a RE‑množin. Diagonální metoda. Vlastnosti množin K a K0.
D. cv. Na přednášce jsme začali řešit cv. 19. Aktuální jsou i 18 a 20. Řešitelná jsou teď všechna do 20 s výjimkou 13–15 (ta se týkají primitivní rekurze, kterou jsme přeskočili).
15. listopadu 2016
Churchova téze. Pojem univerzální funkce. Množina K.
10. listopadu 2016
Kódování. Turingův predikát.
8. listopadu 2016
Kódování instrukcí, celých vývojových diagramů, jejich konfigurací a výpočtů pomocí slov v pětiprvkové abecedě (začátek).
3. listopadu 2016
Věta o výběrové funkci a její důsledky. Funkce je FPartR, právě když má RE graf. Věta o separaci. Postova věta: jsou-li dvě RE množiny navzájem komplementární, obě musí být rekurzívní.
D. cv. 11(b) a 12 (10 a 11(a) udělána v přednášce, přičemž 11(a) je ona věta o výběrové funkci).
1. listopadu 2016
Věta o projekci: množina k-tic je RE, právě když je definičním oborem nějaké částečně rekurzívní funkce. Neprázdná množina čísel je RE, právě když je oborem hodnot nějaké rekurzívní funkce jedné proměnné.
D. cv. Cvičení 7. Řešitelné je i cvičení 8.
27. října 2016
Dokončení důkazu věty týkající se uzavřenosti tříd Σn a Πn na operace. Každá částečně rekurzívní funkce má RE graf. Z toho plyne, že i definiční obor a obor hodnot. Také z toho plyne, že každá Δ1-množina je RE (a ovšem i Π1).
25. října 2016
Párovací funkce. Aritmetická hierarchie.
20. října 2016
Každá Δ0 množina je rekurzívní. To dohromady s větou o rekurzívnosti grafu funkce dává pohodlný prostředek k dokazování, že nějaká funkce je rekurzívní. Dělení se zbytkem, tj. funkce Mod a Div, jsou rekurzívní.
D. cv. K této problematice se vztahuje cvičení 6.
18. října 2016
Graf funkce. Totální funkce je rekurzívní, právě když její graf je rekurzívní množina. Omezené kvantifikátory a Δ0 množiny, čili omezené množiny (podmínky). Tato problematika je v anglickém textu hned na začátku.
D. cv. Zdůvodněte, že množina všech mocnin dvojky je Δ0.
13. října 2016
Rekurzívní funkce a rekurzívní množiny. Uzavřenost rekurzívních množin na booleovské operace.
D. cv. Relevantní jsou cvičení 1 a 3-5 s tím, že cvičení 4 bylo vyřešeno v přednášce.
11. října 2016
Operace minimalizace, částečně rekurzívní funkce. Čtyři triviální operace s funkcemi.
6. října 2016
Vývojové diagramy: úspornější verze vzniklé vynecháním některých instrukcí. Částečné a totální funkce v oboru přirozených čísel, jejich definiční obor a obor hodnot, jejich skládání.
D. cv. Oficiálně nezadáno, protože relevantní cvičení s čísly 16 a 17 v seznamu nahoře byla na přednášce v podstatě vyřešena. Ale možná by mělo smysl si řešení pečlivě napsat.
4. října 2016
Úvod: funkce algoritmicky počitatelné, a ty ostatní. Vývojové diagramy a funkce, které jsou pomocí vývojových diagramů počitatelné.
D. cv. Dokažte, že instrukce CLR, X=Y? a X:=Y lze simulovat pomocí ostatních tří instrukcí.

Classical Logic II

SIS ALG110014

Excercises

Please pay attention to the list of excercises.

Exams (Czech)

Ke zkoušce si prosím připravte seznam osmadvaceti cvičení, která dovedete řešit.

Course contents in Spring 2015/16 (Czech)

12. května 2016
Úplnost kalkulu GJ vůči kripkovslé sémantice.
10. května 2016
Kalkuly GK a GJ. Korektnost a úplnost obou kalkulů vůči příslušné sémantice, úplnost kalkulu GK.
5. května 2016
Intuicionistická výroková logika: kripkovská sémantika, vztah k logice klasické, disjunction property. Gentzenovské (tj. sekventové) kalkuly: sekvent, antecedent, sukcedent, principální, vstupní a postranní formule.
3. května 2016
Druhá Gödelova věta o neúplnosti. Některé souvislosti: Hilbertův program, modální logika.
28. dubna 2016
Formalizace důkazů a dokazatelnosti v PA. Podmínky pro dokazatelnost (Löb's derivability conditions).
21. dubna 2016
Rosserova věta a její strukturální důkaz, tj. důkaz založený na existenci rekurzívně neoddělitelných RE množin. Podstatná neúplnost a podstatná nerozhodnutelnost.
19. dubna 2016
První Gödelova věta o neúplnosti, její strukturální důkaz.
14. dubna 2016
Věta o Σ‑úplnosti Robinsonovy aritmetiky.
12. dubna 2016
Definovatelnost ve struktuře N, souvislost s aritmetickou hierarchií. Jednoduchá varianta První Gödelovy věty o neúplnosti.
7. dubna 2016
Definovatelné množiny. Eliminace kvantifikátorů je nejen nástrojem pro prokazování úplnosti, ale i pro získání informace o definovatelných množinách v různých strukturách. Definovatelné množiny jsou uzavřeny na booleovské operace a na projekci.
5. dubna 2016
Rozhodnutelné a nerozhodnutelné struktury a teorie. Rekurzívní axiomatizovatelnost, Craigův trik. Rozhodnutelnost všech úplných rekurzívně axiomatizovatelných teorií. Rozhodnutelnost teorie, která je rozšířením rozhodnutelné teorie o jediný axiom.
31. března 2016
Rozšíření teorie, konzervativní rozšíření a rozšíření o definice. Úplnost teorie DO. Další příklady (bez důkazů) teorií umožňujících eliminaci kvantifikátorů.
29. března 2016
Eliminace kvantifikátorů pro teorii SUCC, dokončení. Náznak postupu při eliminaci kvantifikátorů pro teorii DOS.
24. března 2016
Vaughtův test, jeho použití k důkazu úplnosti teorie DNO. První kroky v důkazu úplnosti teorie SUCC pomocí eliminace kvantifikátorů.
22. března 2016
Úplné a neúplné teorie. Teorie LO; teorie SUCC a DNO jako možné úplné teorie.
17. března 2016
S užitím věty o kompaktnosti lze dokázat existenci spočetných nestandardních modelů Peanovy aritmetiky i teorie Th(N). Axiomatizovatelné (elementární) a konečně axiomatizovatelné třídy.
15. března 2016
Ze schématu LNP je naopak možné dokázat schéma indukce, ale kromě axiomů Robinsonovy aritmetiky je k tomu potřeba ještě jeden dodatečný axiom. V PA lze dokázat i mnohé další aritmetické fakty: existence a jednoznačnost dělitelnosti se zbytkem, existence nekonečně mnoha prvočísel. Existence a struktura nestandardního modelu Peanovy aritmetiky.
Cvičení. Ke struktuře nestandardních modelů se vztahují cv. 18 a 19.
10. března 2016
Axiomatika Peanovy aritmetiky PA. S užitím schématu indukce lze v PA dokázat, že sčítání, násobení a uspořádání mají "očekávané" vlastnosti (asociativita, komutativita, distributivita, tranzitivita ...). V PA je dokazatelné schéma LNP (schéma nejmenšího prvku).
8. března 2016
Pět schémat dokazatelných v Robinsonově aritmetice Q.
3. března 2016
Větu o silné úplnosti lze chápat i jako nástroj ke zdůvodnění dokazatelnosti určitých formulí. Z věty o silné úplnosti plyne věta o kompaktnosti. Robinsonova aritmetika Q a její jednoduchý nestandardní model ukazující, že běžná tvrzení o přirozených číslech, jako třeba komutativita sčítání nebo tranzitivita uspořádání, obvykle v Q dokazatelná nejsou.
1. března 2016
Dvě definice logického důsledku. Věta o silné úplnosti. Slabá verze Löwenheimovy-Skolemovy věty.
25. února 2016
Struktura jako nástroj pro prokazování nedokazatelnosti, a struktura jako samostatný předmět výzkumu. Prominentní struktury: N, Z, Q, a R. Pojem logického důsledku (vyplývání).
23. února 2016
Sémantika klasické predikátové logiky: struktura pro určitý jazyk, ohodnocení proměnných, Tarského definice, platnost formule ve struktuře. Logicky platné formule. Věta o korektnosti.
Cvičení. Logicky platných formulí se týkají cvičení 1, 5 a 6 v seznamu cvičení. Dokazatelnosti a použití věty o korektnosti se týká cvičení 8. Řešitelné je i cvičení 7.
18. února 2016
Důkaz v hilbertovském kalkulu, dokazatelnost. Axiomy specifikace (konkretizace), pravidla generalizace, axiomy rovnosti.
16. února 2016
Syntax klasické predikátové logiky s rovností. Logické a mimologické symboly, jazyk teorie. Formule, sentence, axiomatické teorie, axiomy specifikace. Jednoduchá teorie s aximy Q1 a Q2.

Arithmetics and algorithms

Please pay attention to the list of excercises. It will extend and will be used during the exam.

SIS ALG110008

Exams (Czech)

Ke zkoušce si prosím připravte seznam patnácti cvičení, která dovedete řešit. Zkouška začne ukázkovým řešením některého nebo některých z těchto cvičení a neúspěch v této části by znamenal neúspěch celé zkoušky. V úterý 17.5. se v 9:10 v učebně 137 koná poslední přednáška.

Course contents in Spring 2015/16 (Czech)

3. května 2016
Důležitá pomocná tvrzení: nenulový polynom stupně n má v oboru integrity nejvýše n kořenů, a součet čísel φ(k) pro dělitele k čísla n je n.
3. května 2016
Úlohy ve třídě NP. Řády prvků v komutativní grupě.
19. dubna 2016
Kryptografická metoda RSA. Mersennova čísla a Mersennova prvočísla.
12. dubna 2016
Výpočet hodnoty Eulerovy funkce pro libovolný argument. Fermatova (Eulerova) věta: umocnění libovolného prvku Abelovy (tj. komutativní) grupy na počet prvků grupy dá jako výsledek jedničku (té grupy).
Cvičení. K dokončení důkazu na konci přednášky, že 645 je pseudoprvočíslo, chybělo najít dělitele m čísla 644 takového, že 2m - 1 = 1Z43. Řešitelné je i cvičení 7, které na přednášce z části vyřešeno bylo.
5. dubna 2016
Pseudoprvočísla. Eulerova grupa a Eulerova funkce. Výpočet hodnoty Eulerovy funkce pro určité argumenty (mocnina prvočísla nebo součin dvou různých prvočísel).
Cvičení. Dokažte bez užití technických prostředků, že číslo 561 je pseudoprvočíslo.
29. března 2016
Dělitelnost v oborech integrity, v nichž platí Bezoutova věta. Ekvivalentní podmínky pro prvočíselnost a pro nesoudělnost. Čínská zbytková věta.
22. března 2016
Nejen sčítání, násobení a (díky zobecněnému Eukleidovu algoritmu) i invertování, ale i umocňování v Zm je počitatelné v polynomiálním čase. Dělitelnost v oboru integrity. Bezoutova věta jako dodatečný axiom přidaný k axiomům oboru integrity.
15. března 2016
Invertibilní prvky v různých okruzích. Charakterizace invertibilních prvků v okruhu Zm. Díky (zobecněnému) Eukledovu algoritmu lze o invertibilitě v Zm rozhodovat a inverzní prvky určovat v polynomiálním čase. Tělesa a obory integrity.
8. března 2016
Axiomy komutativní pologrupy a a grupy a komutativního okruhu. Jejich bezprostřední důsledky. Důležité příklady okruhů: Zm pro m ≥ 2, struktura celých čísel Z, struktura racionálních čísel Q, struktura Q[x] všech polynomů s racionálními koeficienty. Opačné a inverzní prvky.
Cvičení. Určete, které prvky okruhu Z15 jsou invertibilní.
1. března 2016
Drobný matematický důsledek Eukleidova algoritmu: největší společný dělitel dvou čísel je takový společný dělitel, který je dělitelný všemi společnými děliteli. Korektnost zobecněného Eukleidova algoritmu. Komutativní pologrupa.
23. února 2016
Eukleidův algoritmus pro úlohu GCD. Důkaz jeho korektnosti a faktu, že počítá v polynomiálním čase. Bezoutova rovnice. Zobecněný (čtyřsloupcový) Eukleidův algoritmus pro nalezení řešení Bezoutovy rovnice.
Cvičení. V seznamu cvičení nahoře je řešitelné cv. 1. Přestože jsme ještě nedokázali korektnost zobecněného Eukleidova algoritmu, lze jej použít k řešení cvičení 3.
16. února 2016
Úlohy a algoritmy. Úloha jako nekonečná množina instancí. Algoritmus počítající nebo rozhodující úlohu. Některé důležité úlohy: Násobení, Mod, Div, Primes, Factoring, GCD. Časové nároky algoritmů. Polynomiální algoritmy a algoritmy s exponenciální časovou náročností.

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.

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 lowerbounds for cut-elimination in classical predicate logic, decision procedures for intuitionistic propositional logic. Here is the list of topics (in Czech). SIS: ALG500003.

Exams (Czech)

Ke zkoušce je třeba zvládnout témata dle vlastního výběru, která pokrývají 15 dvouhodinovek. Vlastní referát se do počtu 15 počítá trojnásobně.

Course contents in 2014/15 (Czech)

Pudlákův spodní odhad pro eliminaci řezů (V. Švejdar, 2)
Pudlákova exponenciální aritmetika, různé důkazy sentence P(E(n)(0)). Četba: prezentace ke krátkému kursu. Oprava k přednášce: zatímco věta o eliminovatelnosti řezů se týká všech regulárních sekventů, věta o středním sekventu se vztahuje pouze k regulárním sekventům obsahujícím pouze prenexní formule (pochopitelně, neboť požadavek, aby všechny výrokové kroky předcházely všechny predikátové kroky, by jinak splnit nešlo).
Prosté a hyperprosté množiny (J. Bydžovský, 3)
Definice prostých a hyperprostých množin, různé konstrukce. Jejich aplikace v důkazu tvrzení o nezávislé axiomatizaci Peanovy aritmetiky. Četba: strany 357–9 v Odifreddiho knize, plus (hlavně) handout pana Bydžovského.
Dodatky k intuicionistické logice (A. Kuncová, 3)
Varianty důkazů rozhodnutelnosti a úplnosti intuicionistické výrokové logiky vůči kripkovské sémantice, jejich aspekty, různé kalkuly.
Silné fragmenty Peanovy aritmetiky (K. Přikrylová, 3)
Článek Paris‑Kirby (3.7MB), plus handout.
Dobrá uspořádání v teoretické informatice (J. Seidl, 1)
Článek Dershowitz‑Manna.
Hilbertův program (P. Truhlář, 2)
Zde je k dispozici Smorynského článek (3.6MB) a handout pana Truhláře.
Metamatematika teorií množin (T. Lávička, 3)
Axiomatika teorií ZF, GB a KM. Teorie ZF je ve smyslu zřejmém ale technicky poněkud obtížném (ve smyslu interpretovatelnosti) podteorií teorie GB. O GB je známo, že je konečně axiomatizovatelná. V ZF lze dokázat sentenci Con(ZF) ↔ Con(GB). Související výsledek (vlastně se stejným důkazem) je, že GB je nad ZF konzervativní vůči množinovým formulím. V GB lze napsat formuli Ocp(x), která je netriviálním řezem. V GB tedy není dokazatelná indukce pro všechny formule, a není pravda, že každá formule určuje třídu (všech množin nebo přirozených čísel, které ji splňují). V KM lze dokázat sentenci Con(ZF); KM je tedy ostře silnejší než ZF a GB.
Četba: A. Sochor, metamatematika teorií množin (první čtyři kapitoly); V. Švejdar, Infinite Natural Numbers: an Unwanted Phenomenon, or a Useful Concept?. Původní zdroj k problematice obsaditelných čísel a plné indukce v GB je P. Vopěnka, P. Hájek, Existence of a Generalized Semantic Model of Gödel‑Bernays Set Theory.
Logika dokazatelnosti GL (V. Švejdar, 6)
Aritmetická sémantika logiky GL. PA‑tautologie a N‑tautologie. Axiomatika logiky GL. Variantní axiomy či pravidla: Löbovo pravidlo LR, schéma H. Ekvivalence schématu H s Löbovým axiomem. Pojem charakteristické třídy. Logiky GL a H jsou neekvivalentní, přestože mají stejnou charakteristickou třídu. Gentzenovský kalkulus logiky GL. Některé aplikace logiky GL v metamatematice: jednoznačná řešitelnost gödelovských autoreferenčních rovnic, explicitní vyjádřitelnost jejich řešení.
Autoreference (V. Švejdar, 4)
Znění věty o autoreferenci. Gödelova sentence, První Gödelova věta. Löbovy podmínky, Σ‑úplnost, formalizovaná Σ‑úplnost. Rosserova sentence; formalizovatelnost důkazu její nedokazatelnosti i důkazu její nevyvratitelnosti. Henkinova sentence, Löbovo řešení Henkinova problému. Gödelova autoreference a problém s ní spojený: má každá gödelovská autoreferenční rovnice jednoznačně určené řešení? Důkaz věty o autoreferenci a důkaz tvrzení v něm použitého, že každá rekurzívní funkce je v Robinsonově aritmetice slabě reprezentovatelná.
Četba: části oddílu 4.5 a úvod oddílu 5.3 v knize.

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

Hanba novému českému prezidentovi

Já vím, že na profesionální web politika nepatří. Ale ten odpudivý nacionalismus a nečestný způsob vedení volební kampaně překročily meze demokratické politiky. Dopisy, které jsem v lednu 2013 mezi oběma koly prezidentské volby napsal paní Táně Fischerové předtím panu Václavu Moravcovi zde ponechávám k nahlédnutí. Shame on the Czech president!

Vědecké a pedagogické výsledky Katedry logiky

Ponechávám zde k nahlédnutí seznam publikací Katedry logiky, který jsem ve spolupráci s kolegy sestavil v prosinci 2014, když jsem se paní děkance snažil doložit pedagogické a vědecké výsledky pracovište, jakož i některé z dopisů, které jsem v souvislosti s jednáním o rozpočtu katedry paní děkance poslal (jeden a ještě jeden).