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)

15. května 2018
Sémantika intuicionistické výrokové logiky.
10. května 2018
Gentzenovský kalkulus pro predikátovou logiku.
3. května 2018
Věta o autoreferenci, Druhá Gödelova věta.
26. dubna 2018
Podmínky pro dokazatelnost (Löb's derivability conditions).
24. dubna 2018
Dokazatelnost v Peanově aritmetice.
19. dubna 2018
Rosserova věta: místo Σ-korektnosti stačí předpokládat bezespornost. Avšak k (pravdivému) závěru, že Thm(T) je Σ1-kompletní, by bylo potřeba použít efektivně rekurzívně neoddělitelné množiny místo pouze rekurzívně neoddělitelných.
17. dubna 2018
První Gödelova věta: každá rekurzívně axiomatizovatelná teorie T, která je rozšířením Robinsonovy aritmetiky a je Σ-korektní, je neúplná a nerozhodnutelná. Existují Σ1- a Π1-sentence nezávislé na T, a Thm(T) je Σ1-kompletní.
12. dubna 2018
Pozititní a negativní kroky v důkazu Σ-úplnosti.
10. dubna 2018
Dokončení konstrukce jednoduchého modelu Robinsonovy aritmetiky, který ukazuje, že univerzální sentence jsou v Q málokdy dokazatelné.
5. dubna 2018
Množina Th(N) není v aritmetické hierarchii. Z toho plyne jednoduchá verze První Gödelovy věty o neúplnosti.
3. dubna 2018
Eliminace kvantifikátorů jako nástroj pro zkoumání definovatelných množin. Hierarchie aritmetických formulí. Definovatelnost ve struktuře N.
29. března 2018
Rozhodnutelné a nerozhodnutelné teorie a struktury. Úplná rekurzívně axiomatizovatelná teorie je rozhodnutelná. Craigův trik. Rozhodnutelnost konečného rozšíření rozhodnutelné teorie. Definovatelné množiny.
27. března 2018
Neaxiomatizovatelnost třídy všech silně souvislých orientovaných grafů. Rekurzívně axiomatizovatelné teorie. Množiny Thm(T) a Ref(T).
22. března 2018
Důsledky věty o kompaktnosti. Axiomatizovatelné a konečně axiomatizovatelné třídy struktur. Příklady neaxiomatizovatelných struktur.
20. března 2018
Vaughtův test a jeho aplikace na teorii DNO. Věta o kompaktnosti.
18. března 2018
Dokončení úvah o eliminaci kvantifikátorů pro teorii DOS. Další známé teorie, které umožňují eliminaci kvantifikátorů (bez důkazu): Presburgerova aritmetika, teorie struktury reálných čísel.
13. března 2018
Teorie DO a DOS. Pojmy rozšíření, konzervativní rozšíření a rozšíření teorie o definice.
8. března 2018
Eliminace kvantifikátorů pro teorii SUCC.
6. března 2018
Věta o úplnosti. Různé významy pojmu úplnost. Úplné teorie. Teorie struktury. Teorie následníka (SUCC).
1. března 2018
Vyplývání, logicky platné formule.
27. února 2018
Opakování sémantických pojmů: struktura, ohodnocení proměnných, splněnost formule ohodnocením, platnost formule ve struktuře. Věta o korektnosti.
22. února 2018
Pokračování úvah o dokazatelnosti a nedokazatelnosti v teorii s axiomy Q1 a Q2.
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 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

Exams (Czech)

Ke zkoušce si prosím připravte seznam třiná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.

Course contents in Spring 2017/18 (Czech)

15. května 2018
Přehled důležitých pojmů: Eulerovy grupy a řády prvků v nich, úlohy ve třídě P a úlohy ve třídě NP. Prattův výsledek, že Primes je úloha ve třídě NP, je závislý na následující větě: když m je prvočíslo a k je dělitel čísla m - 1, pak v grupě Φ(m) je přesně φ(k) prvků řádu k. Probabilistické algoritmy. Absolutní pseudoprvočísla.
26. dubna 2018
Číslo m = 289 - 1 je prvočíslo: číslo 61 je prvek grupy Φ(m), má v ní řád m - 1, takže počet prvků této grupy je m - 1. Náznak zdůvodnění, že tento postup funguje pro každé prvočíslo, což má dále důsledek, že Primes je úloha ve třídě NP.
19. dubna 2018
Kryptografická metoda RSA. Výsledek F. Colea z roku 1903: 267 - 1 není prvočíslo. Úlohy ve třídě NP. Řády prvků v grupách.
D. cv. Určete řády všech prvků v grupách Φ(7), Φ(8), a Φ(15).
10. dubna 2018
Komutativní grupy. V konečné komutativní grupě s n prvky platí an = 1 pro každý prvek. Z toho máme jednak (malou) větu Fermatovu: když m je prvočíslo, pak pro každý nenulový prvek a struktury Zm platí am-1 = 1, a také obecnější Eulerovu větu: pro každý prvek a Eulerovy grupy Φ(m), tj. pro každý invertibilní prvek struktury Zm, kde m nemusí být prvočíslo, platí aφ(m) = 1.
D. cv. Druhá část cvičení 7 (poslední dvě desetinné cifry čísla 6121).
3. dubna 2018
Důkaz čínské zbytkové věty. Pseudoprvočísla. Užití čínské zbytkové věty k důkazu tvrzení o Eulerově funkci: jsou-li a a b nesoudělná, pak φ(a·b) = φ(a)·φ(b).
D. cv. Dokažte pomocí modulárních reprezentací, že číslo 561 je pseudoprvočíslo.
27. března 2018
Nejen sčítání a násobení, ale i určování invertibility a výpočet inverzního prvku v okruhu Zm jsou polynomiálně počitatelné úlohy. Eulerova funkce, Modulární reprezentace.
D. cv. oficiálně nezadáno, ale celkem k věci by mohlo být toto: určete hodnotu Eulerovy funkce pro argumenty 35 a 51 (což je trochu snazší než vyřešit celé cvičení 6).
20. března 2018
Modulární aritmetika, tj. počítání ve struktuře Zm. Komutativní okruh, bezprostřední důsledky axiomů. Zobecněný Eukleidův algoritmus jako nástroj pro detekci invertibilních prvků a pro výpočet inverzního prvku.
D. cv. Cvičení 5.
13. března 2018
Algebraické (aritmetické) důsledky Bezoutovy věty: ekvivalentní podmínky pro nesoudělnost a prvočíselnost. Cvičení 4 bylo v přednášce v podstatě vyřešeno, až na to, že dělitelům jedničky se tam říká invertibilní prvky.
6. března 2018
Časové nároky Eukleidova algoritmu: je to algoritmus pracující v polynomiálním čase. Algebraickým důsledkem Eukleidova algoritmu je tvrzení ze cvičení 3 (které je tím vyřešeno). Dělitelnost a dělení se zbytkem v oboru celých čísel. Bezoutova rovnice, podmínka pro její řešitelnost a zobecněný (čtyřsloupcový) algoritmus pro nalezení některého řešení.
D. cv. Cvičení 2.
27. února 2018
Další důležité úlohy: GCD, Factoring, Coprimes. Časové nároky algoritmů, algoritmy pracující v lineárním, kvadratickém či exponenciálním čase. Polynomiální algoritmy a polynomiálně počitatelné úlohy.
D. cv. Cvičení 1 v seznamu nahoře.
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)

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