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.

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. Cvičení 29 a 31 zůstala za obzorem kursu.

Course contents in Fall 2015/16 (Czech)

7. ledna 2016
Trochu "informatičtější" interpretace Riceovy věty: žádná netriviální vlastnost programu, která je definována tím, co ten program dělá (beze zmínky o tom, co je napsáno ve zdrojovém textu), se ze zdrojového textu onoho programu nedá poznat algoritmem. Ještě jedno použití diagonalizace: existují rekurzívně neoddělitelné dvojice rekurzívně spočetných množin, tj. existují dvě rekurzívně spočetné množiny takové, že žádná nadmnožina jedné z nich, která je disjunktní s druhou, není rekurzívní. Také existují částečně rekurzívní funkce, které nemají rekurzívní prodloužení.
5. ledna 2016
Věta o rekurzi a věta o pevném bodu (jejich jednodušší varianta mluvící o řešitelnosti určitých rovnic pro neznámé číslo). Indexové množiny a Riceova věta: indexová množina není nikdy převeditelná na vlastní komplement, takže indexová množina, která není prázdná ani nemá prázdný komplement, nemůže být rekurzívní.
17. prosince 2015
Další příklady na větu o parametrech. Π2‑kompletnost množin Unb a Tot.
15. prosince 2015
Věta o parametrech, Σ1‑kompletnost množiny K.
3. prosince 2015
Věta o parametrech, příklady jejího použití.
1. prosince 2015
Definice a základní vlastnosti m‑převeditelnosti. M‑kompletnost. Existence Σn- a Πn‑kompletních množin pro každé nenulové n.
26. listopadu 2015
Aritmetická klasifikace prominentních množin. Tarského‑Kuratowského algoritmus pro nalezení aritmetické klasifikace.
24. listopadu 2015
Univerzální RE relace. Relace univerzální pro třídu všech Δ0 množin, která by sama byla Δ0, neexistuje. Avšak pro každé nenulové n existuje univerzální Σn relace, tj. relace, která je univerzální pro třídu všech Σn množin a přitom sama je Σn. Aritmetická hierarchie nekolabuje. Prominentní množiny: K, K0, Tot, Unb a Rec.
19. listopadu 2015
Turingův predikát, věta o normální formě, diagonální metoda.
12. listopadu 2015
Kódování vývojových diagramů, jejich konfigurací a výpočtů pomocí přirozených čísel. Turingův predikát.
11. listopadu 2015
Uzavřenosti třídy FGR na zobecněnou primitivní rekurzi (ordinální rekurzi). Ještě jedna charakterizace rekurzívně spočetných množin: množina čísel je RE, právě když je konečná nebo je oborem hodnot nějaké prosté (!) FGR.
D. cv. Ackermannova funkce (jedna z jejích variant) je definována rovnostmi f(0,y) = y + 2, f(x+1,y) = f(x,y+1), f(x+1,y+1) = f(x,f(x+1,y)). Určete hodnotu f(3,1).
10. listopadu 2015
Kódování posloupností. Uzavřenosti třídy FGR na operaci primitivní rekurze. Ještě jedna charakterizace rekurzívních množin: množina čísel je rekurzívní, právě když je konečná nebo je oborem hodnot nějaké rostoucí (!) FGR. Zobecněná primitivní rekurze (ordinální rekurze).
9. listopadu 2015 (nahrazení přednášky z 8.12.)
Od kódování množin ke kódování posloupností. Příklady na odvození funkce primitivní rekurzí.
V úterý 10.11. stejně jako ve čtvrtek 12.11. se scházíme normálně. V úterý se pokusíme o domluvu o druhém nahrazování (přednášky z 10.12.), přičemž jedna z možností je už středa 11.11.
5. listopadu 2015
Postova věta. Věta o odvození funkce větvením (rozborem případů). Kódování konečných množin metodou dvou pravítek.
3. listopadu 2015
Různé charakterizace pojmu rekurzívně spočetná množina: množina k‑tic je RE, právě když je definičním oborem jisté částečně rekurzívní funkce; neprázdná množina čísel je RE, právě když je oborem hodnot jisté obecně rekurzívní funkce; množina je RE, právě když je projekcí jisté rekurzívní relace. Každá funkce s RE grafem je částečně rekurzívní.
29. října 2015
Dokončení úvah o uzavřenosti tříd Σn a Πn na operace. Každá částečně rekurzívní funkce má RE graf. Jedním z důsledků je, že každá rekurzívní množina je RE. Tím pádem je ale automaticky i Π1.
27. října 2015
Párovací funkce. Aritmetická hierarchie.
D. cv. Zdůvodněte, že je-li některá z tříd Σn a Πn podtřídou druhé, pak jsou si rovny.
22. října 2015
Δ0 podmínky. Každá Δ0 podmínka je rekurzívní. Důležité Δ0 množiny: relace dělitelnosti, ostré i neostré uspořádání, množina všech prvočísel. Důležité funkce, které mají Δ0 graf, a tudíž jsou rekurzívní: podmíněné odčítání, dělení se zbytkem.
D. cv. Dokažte, že množina všech mocnin dvojky je Δ0.
20. října 2015
Ke každé částečně rekurzívní funkci existuje vývojový diagram, který ji počítá. Δ0 podmínky (tj. omezené podmínky).
D. cv. Cvičení 16 a 17 v seznamu nahoře.
15. října 2015
Poznámka k pojmu graf funkce: rekurzívní funkce musí mít rekurzívní graf, ale nečekáme, že každá částečně rekurzívní funkce má rekurzívní graf. Vývojové diagramy. Diagram počítající funkci.
13. října 2015
Graf funkce. Operace minimalizace. První z několika vět, které dávají do souvislosti rekurzívnost funkce s rekurzívností jejího grafu: totální funkce je rekurzívní, právě když má rekurzívní graf.
8. října 2015
Rekurzívní funkce jako ty funkce, které jsou částečně rekurzívní a totální. Uzavřenost množiny všech částečně rekurzívních i rekurzívních funkcí na čtyři triviální operace (ztotožnění proměnných, dosazení konstanty, zpřeházení proměnných a přidání jalové proměnné). Rekurzívní množiny. Jejich uzavřenost na tytéž čtyři triviální operace a též na booleovské operace.
D. cv. Dokažte postupně, že jednoprvková množina {1} i dvouprvková množina {0,1} jsou rekurzívní.
6. října 2015
Úvod: algoritmicky rozhodnutelné a nerozhodnutelné úlohy. Úloha jako funkce, jejíž argumenty i funkční hodnoty lze zapsat jako konečné posloupnosti symbolů. Úlohy ve skutečnosti ale uvažujeme v ještě užším smyslu, totiž jako funkce v oboru přirozených čísel (libovolného počtu proměnných a případně ne všude definované). Protože algoritmicky zajímavé úlohy se týkají spíše jiných objektů než přirozených čísel (formulí, důkazů nebo počítačových programů), je nutné uvažovat kódování těchto objektů pomocí přirozených čísel. Operace substituce. Šest základních funkcí.

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).