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í namátkově vybraného (vybraných) cvičení je podmínkou pro připuštění k vlastní zkoušce.

Course contents in Fall 2016/17 (Czech)

4. ledna 2018
Turingovy stroje. Úvahy o "bobří soutěži" poskytují poměrně jednoduše definovanou funkci, o které se celkem jednoduše dá dokázat, že není rekurzívní.
19. prosince 2017
Imunní a prosté množiny. Ještě jedna konstrukce prosté množiny.
14. prosince 2017
Příklad na použití věty o rekurzi a rovnic pro neznámou funkci: každá částečně produktivní množina je úplně produktivní. Ještě jeden příklad může být toto: důkaz z přechozí přednášky o kreativních množinách lze zobecnit do tvrzení, že množina - K je převeditelná na každou produktivní množinu. Konstrukce RE množiny, která není ani rekurzívní, ani Σ1 kompletní.
12. prosince 2017
Každá produktivní množina má nekonečnou RE podmnožinu. Množina je kreativní, právě když je Σ1 kompletní.
7. prosince 2017
Produktivní a kreativní množiny. Množina K je kreativní, její komplement - K je produktivní. Množina, na kterou je převeditelná produktivní množina, je produktivní.
5. prosince 2017
Indexové množiny, Riceova věta: indexová množina není rekurzívní, takže pokud ona sama i její komplement jsou neprázdné, pak není rekurzívní.
30. listopadu 2017
Další příklady na konstrukce převodů. Π2-kompletnost množin Unb a Tot. První úvahy (důkaz pomocí plného znění věty o parametrech) věty o rekurzi.
28. listopadu 2017
Použití věty o parametrech ke konstrukci převodů. Σ1-kompletnost množiny K.
23. listopadu 2017
Věta o parametrech (s-n-m theorem). Její jednodušší varianty týkající se enumerace funkcí nebo enumerace množin, které obvykle stačí ke konstrukci převodů.
21. listopadu 2017
Vlastnosti m-převeditelnosti. Definice m-kompletnosti, Σ1-kompletnost množiny K0.
16. listopadu 2017
Další prominentní množiny: K0, Unb, Tot, Rec. Tarského-Kuratowského algoritmus. Nerekurzívnost množiny K. Definice m-převeditelnosti.
14. listopadu 2017
Enumerace RE množin a relací. Pro každé nenulové n existuje univerzální Σn relace. Aritmetická hierarchie nekolabuje.
9. listopadu 2017
Univerzální funkce a věta o normální formě. Částečně rekurzívní funkce, která nemá žádné rekurzívní prodloužení. Rekurzívně neoddělitelné množiny.
7. listopadu 2017
Kódování instrukcí, diagramů, konfigurací a výpočtů, dokončení. Funkce je FPartR, právě když ji počítá některý vývojový diagram. Churchova téze.
2. listopadu 2017
Funkce počitatelné na vývojových diagramech. Kódování diagramů a jejich výpočtů.
31. října 2017
Cvičení: každá nekonečná RE množina obsahuje nekonečnou rekurzívní podmnožinu. Vývojové diagramy.
26. října 2017
Uzavřenost třídy FGR na rekurzi. Příklady použití rekurze. Nekonečná množina čísel je rekurzívní, právě když je oborem hodnot jisté rostoucí FGR. Nekonečná množina čísel je rekurzívně spočetná, právě když je oborem hodnot jisté prosté FGR.
24. října 2017
Kódování posloupností. Primitivní rekurze a zobecněná (ordinální) rekurze (course of values recursion).
19. října 2017
Postova věta. Neprázdná množina čísel je RE, právě když je oborem hodnot jisté FGR.
17. října 2017
Množina je RE, právě když je definičním oborem jisté FPartR, a také právě když je projekcí jisté rekurzívní relace. Párovací funkce. Každou RE relaci lze aproximovat částečně rekurzívní funkcí. Důsledkem je, že každá funkce s RE grafem je FPartR.
12. října 2017
Charakteristická funkce množiny, rekurzívní (Δ1) množiny. Všechny uvažované třídy (množin i funkcí) jsou uzavřené na čtyři triviální operace (přidání jalové proměnné, permutace proměnných, ztotožnění proměnných a dosazení konstanty). Odvozené operace: dosazením rekurzívních funkcí do rekurzívní (ale i Σn nebo Πn pro nenulové n) vznikne opět rekurzívní (Σn nebo Πn) podmínka, a minimalizace se smí aplikovat i na rekurzívní podmínku. Důsledkem je, že totální funkce je rekurzívní, právě když má rekurzívní graf. Rekurzívní množiny jsou uzavřeny na booleovské operace i na omezené kvantifikátory. Takže každá Δ0 množina je rekurzívní. Dělení se zbytkem, tj. funkce Mod a Div, jsou rekurzívní.
10. října 2017
Operace minimalizace. Definice částečně rekurzívních (FPartR) a rekurzívních (FGR) funkcí. Každá částečně rekurzívní funkce má RE graf.
5. října 2017
Aritmetická hierarchie. Uzavřenost tříd Σn a Πn na operace. Pojem graf funkce.
3. října 2017
Úvod: plánem je zabývat se algoritmicky rozhodnutelnými a algoritmicky nerozhodnutelnými úlohami, a algoritmicky počitatelnými funkcemi. Vše v oboru přirozených čísel, a to přestože pro relevantní úlohy většinou platí, že jejich instance nejsou přirozená čísla, ale syntaktické objekty. První přiblížení se k definici algoritmicky počitatelné úlohy: omezené čili Δ0 podmínky (množiny).

Classical Logic II

SIS ALG110014

Excercises

Please pay attention to the list of excercises.

Course contents in Spring 2017/18 (Czech)

20. února 2018
Opakování: hilbertovský kalkulus pro predikátovou logiku s rovností. Termy, formule, sentence. Substituce a substituovatelné termy, Axiomy specifikace. Axiomy rovnosti. 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

Course contents in Spring 2017/18 (Czech)

20. února 2018
Dělitelnost v oboru přirozených čísel, některé vlastnosti. Prvočísla. Některé úlohy související s aritmetikou přirozených čísel (Násobení, Primes, Div, Mod) a algoritmy, které je počítají.

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)

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