V.Š. V.Š.

Introduction

K nadcházející prezidentské volbě

Styl polemizování pana Michaela Žantovského mě přiměl k napsání jakési reakce na jeho Facebook. Dávám ji zde k dispozici: dopisMZantovsky.pdf.

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.

Computability

SIS ALG110010

Exams

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

Ke zkoušce si prosím připravte seznam dvaceti čtyř cvičení, která umíte řešit. Správné vyřešení (s využitím přinesených poznámek) namátkově vybraného (vybraných) cvičení je podmínkou pro připuštění k vlastní zkoušce. Cvičení 29 zůstalo za obzorem kursu.

Course contents in Fall 2018/19 (Czech)

10. ledna 2019
Zobecněná primitivní rekurze (course-of-values recursion). Množina je rekurzívně spočetná, právě když je konečná nebo je oborem hodnot nějaké prosté rekurzívní funkce. Prosté (simple) množiny. Prostá množina S očividně nemůže být rekurzívní, ale do přednášky se už nevešla úvaha, že nemůže být ani Σ1-kompletní. Pokud by totiž byla Σ1-kompletní, pak by na ni byla převeditelná množina K, takže na její komplement - S by byla převeditelná množina - K, takže - S by byla produktivní a měla by tedy nekonečnou rekurzívně spočetnou podmnožinu.
8. ledna 2019
Každá produktivní množina má nekonečnou rekurzívně spočetnou podmnožinu. Kódování konečných posloupností.
3. ledna 2019
Operace primitivní rekurze. Množina je Δ1, právě když je oborem hodnot nějaké rostoucí rekurzívní funkce.
20. prosince 2018
Věta o pevném bodu. Indexové množiny. Riceova věta: indexová množina A není převeditelná na vlastní komplement; takže pokud navíc A ≠ ∅A ≠ N, množina A není rekurzívní. Vyřešeno cvičení 30.
18. prosince 2018
Produktivní množiny. Množina K je produktivní. Každá množina, na kterou je převeditelná produktivní množina, je také produktivní. Důkaz věty o rekurzi (jednoduché verze týkající se rovnice pro neznámě číslo).
13. prosince 2018
Další příklady na převody: množiny Unb a Tot jsou Π2-kompletní. Vyřešeno cvičení 26.
11. prosince 2018
Důsledek věty o parametrech vhodný ke konstrukci převodů.
6. prosince 2018
Užití věty o parametrech ke konstrukci převodů: například množina K je Σ1-kompletní.
4. prosince 2018
Existence Σn- a Πn-kompletních množin. Existence nejmenších horních závor vůči m-převeditelnosti.
29. listopadu 2018
M-převeditelnost a její vlastnosti. Důležitá vlastnost množiny K0: každá RE množina je na ni m-převeditelná.
27. listopadu 2018
K problematice rekurzívnosti grafu a definičního oboru funkce vyřešena cvičení 9 a 19. Patří k tomu také cvičení 20. Prominentní množiny Tot, Unb a Rec. Tarského-Kuratowského algoritmus pro určení aritmetické klasifikace množiny.
22. listopadu 2018
Částečně rekurzívní funkce, která nemá žádné rekurzívní prodloužení. Existence dvojice disjunktních rekurzívně neoddělitelných RE množin. Věta o parametrech: znění a náznak důkazu.
20. listopadu 2018
Pro každou třídu Σn (je-li n nenulové) existuje univerzální relace, která je také Σn. Z toho plyne, že aritmetická hierarchie nekolabuje.
15. listopadu 2018
Enumerace částečně rekurzívních funkcí a rekurzívně spočetných množin. Diagonální metoda. Prominentní množiny K a K0.
13. listopadu 2018
Kódování syntaktických objektů, dokončení: konfigurace, výpočty, Turingův predikát. Věta o normální formě.
8. listopadu 2018
Kódování syntaktických objektů pomocí přirozených čísel obecně, a objektů souvisejících s vývojovými diagramy zvlášť. Zatím došlo na instrukce a diagramy.
6. listopadu 2018
Alternativní důkazy Postovy věty, náznak jejího významu v logice. Příklady na to, že když RE množina má určitou matematickou strukturu, musí být rekurzívní.
1. listopadu 2018
Věta o výběrové funkci (či o aproximaci RE množiny pomocí funkce): každá RE relace má podmnožinu se stejným oborem hodnot, která je částečně rekurzívní funkcí. Důsledky této věty jsou: (i) každá funkce, jejíž graf je RE, je FPartR, (ii) větvení podle rekurzívní podmínky jako odvozená operace s částečně rekurzívními funkcemi, (iii) Postova věta: Δ1 = Σ1Π1, (iv) věta o redukci (označení "věta o separaci" uvedené ve cvičení 11 pravděpodobně nesedí), (v) každé dvě Π1 množiny jsou rekurzívně oddělitelné.
D. cv. Cvičení 12.
30. října 2018
Ekvivalentní podmínky pro rekurzívní spočetnost: Množina (relace) je RE, právě když je projekcí nějaké Δ1 relace. A množina (relace) je RE, právě když je definičním oborem nějaké částečně rekurzívní funkce (této ekvivalenci se říká věta o projekci). Množina čísel je RE, právě když je prázdná nebo je oborem hodnot nějaké rekurzívní funkce.
25. října 2018
Mod, Div, párovací funkce a funkce l a r jsou příklady užitečných funkcí, jejichž rekurzívnost lze dokázat na základě toho, že mají Δ0 graf. Graf Každé částečně rekurzívní funkce je Σ1 čili rekurzívně spočetný. Z toho plyne, že Δ1 je podtřídou jak třídy Σ1, tak třídy Π1.
23. října 2018
Uzavřenost tříd ΣnΠn na operace. Každá Δ0 podmínka je rekurzívní. To dohromady s větou, že totální funkce je FGR, právě když její graf je Δ1, dává účinný i když ne vždy aplikovatelný nástroj pro prokazování rekurzívnosti funkcí.
18. října 2018
Δ0 podmínky (omezené podmínky). Aritmetická hierarchie. Důležité Δ0 množiny: množina všech prvočísel, množina všech mocnin dvojky.
16. října 2018
Odvozené metody pro prokazování rekurzívnosti (funkcí nebo množin): rekurzívní podmínky jsou uzavřeny na booleovské operace, dosazení rekurzívních funkcí do rekurzívní podmínky dá vždy rekurzívní podmínku, minimalizaci je legální uplatnit i na rekurzívní podmínku. To poslední je v seznamu cvičení (zatím) uvedeno pod číslem 4. Cvičení 1, 3, a 5 jsou také řešitelná (nebo už byla vyřešena).
11. října 2018
Každou FPartR počítá nějaký vývojový diagram. Triviální operace s částečně rekurzívními funkcemi: přidání jalové proměnné, dosazení konstanty, ztotožnění proměnných, permutace proměnných. Charakteristická funkce množiny, rekurzívní (Δ1) množiny.
D. cv. Dokažte, že neostré uspořádání, tj. množina { [x,y] ; xy }, je rekurzívní množina (dvojic).
9. října 2018
Definice částečně rekurzívních (FPartR) a rekurzívních (FGR) funkcí.
4. října 2018
Ještě vývojové diagramy. Z šesti instrukcí některé lze simulovat pomocí ostatních, ale některé nelze, a lze to dokázat. Částečné funkce k proměnných.
2. října 2018
Úvod: plánem je definovat pojem algoritmu a tím možnost klasifikovat úlohy jako algoritmicky rozhodnutelné a algoritmicky nerozhodnutelné. Ty nerozhodnutelné také hodláme spolu porovnávat. Vývojové diagramy.

Classical Logic II

SIS ALG110014

Excercises

Please pay attention to the list of excercises.

Course contents in Spring 2018/19 (Czech)

21. března 2019
Důkaz úplnosti teorie SUCC pomocí eliminace kvantifikátorů: první dvě ze tří pomocných tvrzení.
19. března 2019
Axiomatizovatelné (elementární) a konečně axiomatizovatelné třídy struktur. Věta o kompaktnosti jako nástroj pro prokazování, že některé třídy axiomatizovatelné nejsou.
14. března 2019
Důležité věty a souvislosti mezi nimi: úplnost, silná úplnost, kompaktnost, Löweheimova-Skolemova věta. Struktura nestandardního modelu Peanovy aritmetiky.
12. března 2019
V PA lze dokázat, že prvočísel je nekonečně mnoho. Vlastnosti axiomatických teorií: konečná axiomatizovatelnost, bezespornost, úplnost. Teorie struktury. Množiny Thm(T) a Ref(T).
7. března 2019
Schéma indukce je nad Q s dodatečným axiomem x(x < S(x)) ekvivalentní se schématem LNP. Všechna očekávaná tvrzení o sčítání a násobení přirozených čísel (obojí asociativita, distributivita, atd.) a o vztazích operací k uspořádání jsou v PA dokazatelná.
5. března 2019
Schémata dokazatelná v Robinsonově aritmetice. Peanova aritmetika. Jednoduché příklady na užití schématu indukce.
28. února 2019
Robinsonova aritmetika. Její jednoduchý nestandardní model.
26. února 2019
Platnost formule ve struktuře, definice vyplývání. Věta o korektnosti. Vyvratitelné a nezávislé sentence.
Všechna cvičení 1–8 jsou teď řešitelná.
21. února 2019
Dokončení přehledu logické syntaxe (k podrobné definici důkazu a k větě o dedukci). Struktury, realizace symbolů, Tarského definice.
19. února 2019
Opakování logické syntaxe: termy, formule, sentence, axiomy specifikace. Tautologie. Dokazatelnost v teorii s axiomy 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

Course contents in Spring 2018/19 (Czech)

19. března 2019
Charakterizace invertibilních prvků v Zm pomocí Bezoutovy věty. Dva ze základních algebraických pojmů: okruh a monoid. Dokazování z axiomů okruhu. Opačné prvky.
D. cv. Uvažujte operaci ∗, která je na tříprvkové množině {0,1,2} definována takto: ab = 2 pro ab, ab = b pro a > b. Určete, zda tato operace je asociativní.
12. března 2019
Důkaz indukcí, že čtyřsloupcové rozšíření Eukleidova algoritmu je korektní. Teoretický důsledek Bezoutovy věty: když prvočíslo dělí součin dvou čísel, musí dělit i některý z činitelů. Modulární aritmetika. Invertibilní prvky ve struktuře Zm.
D. cv. Určete všechny invertibilní prvky ve struktuře Z15.
5. března 2019
Teoretický důsledek Eukleidova algoritmu: mezi společnými děliteli dvou čísel jsou takové, které jsou dělitelné všemi ostatními, což umožňuje formulovat elegantní definici největšího společného dělitele, která je nezávislá na uspořádání a která se nemusí měnit při přechodu mezi různými číselnými (nebo jinými) obory. V podobném duchu lze definovat i nesoudělnost a prvočíselnost. Eukleidův algoritmus má (čtyřsloupcové) rozšíření, které nalezne řešení Bezoutovy rovnice.
D. cv. 1(a) a 2. Další dvě cvičení 3 a 4 beru zpět: 3 bylo v hodině vlastně uděláno, 4 je plán na začátek příští hodiny.
26. února 2019
Úloha GCD (greatest common divisor, čili nalézt největšího společného dělitele dvou čísel). Eukleidův algoritmus pro tuto úlohu. Důkaz jeho korektnost a faktu, že pracuje v polynomiálním čase.
D. cv. Dopočítejte cvičení 1 a předběžně si prosím trochu prohlédněte cvičení 3.
19. února 2019
Časové nároky algoritmů, algoritmy pracující v polynomiálním čase (tj. polynomiální algoritmy). Školní algoritmus pro úlohu Násobení je polynomiální, konkrétně pracuje v kvadratickém čase. O úloze Factoring se předpokládá, že polynomiální algoritmus nemá, ale dokázáno to není. Úloha Primes má polynomiální algoritmus, ale je to obtížnější nedávný výsledek, který zůstane za obzorem kursu.

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 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 2017/18 (Czech)

Dobrá uspořádání v teoretické informatice (V. Jelínková, 15.3., 2)
Důkaz faktu, že daný počítačový program se pro každý vstup dopočítá, může u některých programů být netriviálním matematickým výsledkem. Může v tom pomoci vhodně zvolené dobré uspořádání.
Logika dokazatelnosti (V. Švejdar, 9.11.-)
Logiky K, K4, GL. Varianty axiomatizace: Axiom 4 je v GL redundantní, Löbův axiom je nad logikou K4 ekvivalentní s Löbovým pravidlem, Löbův axiom je nad logikou K4 ekvivalentní také s axiomem H. Kripkovská sémantika modální logiky, korektnost logiky K. Je-li rámec modelu obráceně fundovaný, což je splněno mimo jiné tehdy, je-li konečným acyklickým grafem, pak množina všech formulí platných v onom modelu je uzavřena na Löbovo pravidlo. Takže v logice K, čili bez axiomu 4, nelze dokázat Löbův axiom ani s užitím Löbova pravidla LR. 23. a 30.11. jsme dokazovali, že logiky H a GL mají stejnou charakteristickou třídu. Jejich neekvivalenci tudíž nelze dokázat obvyklými postupy, nicméně Cresswellův model ukazuje, že H je slabší než GL. Pro 7.12. máme zatím nepotvrzený plán, že pan Maxa bude mluvit o neefektivnosti rezoluce.
Autoreference (V. Švejdar, 3)
Gödelova, Henkinova a Löbova autoreferenční sentence. Löbovy podmínky, formalizovaná Σ‑úplnost. Rosserova sentence a důležitý rozdíl vůči Gödelově sentenci: jak důkaz nedokazatelnosti, tak důkaz nevyvratitelnosti lze formalizovat v PA. Problematika jednoznačné řešitelnosti autoreferenčních rovnic. Další možná četba a další možný referát (ale ne tak snadný) je článek Guaspariho a Solovaye "Rosser Sentences" (ta část, kde během konstrukce možná zazvoní zvon). Ale celkem snadno lze ověřit, že obecná věta o jednoznačné řešitelnosti autoreferenčních rovnic určitě neplatí.
Č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