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.

ProfZlatuska.pdf je dopis, který jsem ke skandálům okolo ministra financí 12.5.2017 napsal prof. Jiřímu Zlatuškovi.

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 zůstalo za obzorem kursu.

Course contents in Fall 2016/17 (Czech)

5. ledna 2017
Imunní a prosté (simple) množiny. Produktivní množiny a produktivita všech množin, na které je převeditelná množina K.
3. ledna 2017
Kódování posloupností a užití zobecněné primitivní rekurze. Nekonečná množina je rekurzívně spočetná, právě když je oborem hodnot prosté rekurzívní funkce. Počáteční úvahy směřující ke konstrukci tzv. prosté (simple) množiny.
D. cv.: K primitivní rekurzi se vztahují 13–15, avšak 14 a 15 byla vyřešena v přednášce (a 15 je také obsahem příkladu 2.2.21 v anglickém textu).
22. prosince 2016
Zobecněná primitivní rekurze (course of values recursion). Funkce související se (zatím nespecifikovaným) kódováním posloupností.
20. prosince 2016
Množina K není indexová. Operace primitivní rekurze. Nekonečná množina je rekurzívní, právě když je oborem hodnot jisté rostoucí rekurzívní funkce.
D. cv.: Cvičení 13.
15. prosince 2016
Věta o rekurzi. Indexové množiny a Riceova věta.
D. cv.: Cvičení 28. Dále 30 by teď už mělo být řešitelné.
13. prosince 2016
Další příklady na konstrukci převodů. Π2‑kompletnost množin Tot a Unb.
D. cv.: 23 a 24 jsou stále aktuální. Ve cvičení 22 možná zbyly nějaké nedořešené body. Cvičení 25 a 26 jsou obtížnější, ale řešitelná jsou. Přitom u 25 je poněkud demotivující to, že u obou množin už máme dokázanou Π2‑kompletnost. Naopak 26 je zajímavé tím, že navazuje na 23 a 24, a bude mít ještě pokračování v 30.
8. prosince 2016
Věta o parametrech a její užití ke konstrukci převodů.
D. cv. 21, 23 a 24 (z nich jen první se vztahuje k větě o parametrech).
6. prosince 2016
M‑převeditelnost a m‑kompletnost. M‑kompletní množiny v každé třídě Σn a Πn.
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 zatím 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 2016/17 (Czech)

18. května 2017
Korektnost, úplnost a eliminovatelnost řezů pro klasický výrokový kalkulus GK. Korektnost kalkulu GJ. Důkaz úplnosti kalkulu GJ zůstal nedokončen, avšak vezmeme-li jej jako celkem jasný a přijatelný, kromě úplnosti z něj plyne i eliminovatelnost řezů a vlastnost konečných modelů (finite model property). Z vlastnosti konečných modelů plyne take rozhodnutelnost intuicionistické výrokové logiky.
16. května 2017
Gentzenovský kalkulus pro klasickou logiku. Sekvent, antecedent, sukcedent. Principální, postranní a vstupní formule pravidla. Iniciální a finální sekventy v důkazech, bezřezové důkazy.
11. května 2017
Intuicionistické tautologie. Disjunction property: disjunkce dvou formulí může být intuicionistickou tautologií pouze v případě, když nejméně jedna z oněch formulí je intuicionistickou tautologií.
9. května 2017
Problematika související s Druhou Gödelovou větou: Hilbertův program, logika dokazatelnosti, teorie důkazů. Kripkovské modely pro intuicionistickou výrokovou logiku.
4. května 2017
Věta o autoreferenci, klasický důkaz První Gödelovy věty. Druhá Gödelova věta a její formalizace v PA.
2. května 2017
Formalizace logické syntaxe v PA. Löbovy podmínky.
27. dubna 2017
Princip nejmenšího prvku a jeho vztah ke schématu indukce. Eukleidův důkaz, že prvočísel je nekonečně mnoho, lze s menšími úpravami formalizovat v PA.
25. dubna 2017
Peanova aritmetika PA. Vlastnosti operací a uspořádání dokazatelné v PA.
20. dubna 2017
Rosserovo zobecnění První Gödelovy věty o neúplnosti: pro důkaz nerozhodnutelnosti a existence nezávislých Σ1 a Π1 sentencí stačí místo Σ-korektnosti předpokládat bezespornost.
18. dubna 2017
Dokončení důkazu věty o Σ‑úplnosti Robinsonovy aritmetiky. První Gödelovy věty o neúplnosti: když T je rekurzívně axiomatizovatelné Σ‑korektní rozšíření Robinsonovy aritmetiky, pak nejenže T je nerozhodnutelná, dokonce Thm(T) je Σ1‑kompletní. Nejenže T je neúplná, dokonce existují nezávislé sentence, které jsou Σ1 (nebo Π1).
13. dubna 2017
Pět schémat dokazatelných v Robinsonově aritmetice Q. První kroky v důkazu věty o Σ‑úplnosti.
11. dubna 2017
Třídy aritmetických formulí (Σn, Πn, Σ) a třídy množin, které takové formule definují. Robinsonova aritmetika Q a její jednoduchý nestandardní model.
6. dubna 2017
Definovatelnost ve struktuře přirozených čísel. Th(N) je nearitmetická množina. Z toho plyne jednoduchá varianta První Gödelovy věty o neúplnosti: žádná rekurzívně axiomatizovatelná teorie, pro niž je struktura N jedním z jejích modelů, není úplná.
4. dubna 2017
Příklad neúplné teorie, která je rozhodnutelná. Craigův trik. Rozhodnutelnost konečné struktury pro konečný jazyk. Definovatelné množiny.
30. března 2017
Rekurzívnost logické syntaxe. Úplné rekurzívně axiomatizovatelné teorie jsou rozhodnutelné. Rozhodnutelnost konečného rozšíření rozhodnutelné teorie.
28. března 2017
Příklady neaxiomatizovatelných tříd struktur: dobře uspořádané množiny, silně souvislé orientované grafy.
D. cv. Zajímavá cvičení na větu o kompaktnosti jsou 21 a 22.
23. března 2017
Existence nestandardních modelů teorie Th(N), jejich struktura. Axiomatizovatelné (elementární) a konečně axiomatizovatelné třídy struktur.
21. března 2017
Teorie DNO, důkaz její úplnosti pomocí Vaughtova testu.
D. cv. V přednášce bylo vyřešeno cv. 18. Ve cv. 16 je návod na důkaz eliminovatelnosti kvantifikátorů pro strukturu reálných čísel bez násobení. Ve cv. 13 je ještě jedna z mála dalších teorií, na které je aplikovatelný Vaughtův test.
16. března 2017
Konstrukce lineárně uspořádaných množin (z jiných lineárně uspořádaných množin). Charakterizace modelů teorie DO. Rozšíření teorie o definice jako speciální případ konzervativního rozšíření. Úplnost teorie DO plyne z toho, že úplnost teorie DOS, která je konzervativním rozšířením teorie DO, lze dokázat pomocí eliminace kvantifikátorů.
14. března 2017
Dokončení eliminovatelnosti kvantifikátorů pro teorii SUCC. Teorie DO a DOS. Rozšíření teorie o definici funkčního nebo predikátového symbolu.
D. cv. Cvičení 14 je návod jak dokázat, že pro teorii SUCC eliminovatelnost kvantifikátorů neplatí. K problematice izomorfních resp. elementárně ekvivalentních struktur se vztahují cvičení 15 a 12.
9. března 2017
První kroky v důkazu eliminovatelnosti kvantifikátorů pro teorii SUCC.
7. března 2017
Věta o úplnosti. Löwenheim-Skolemova věta. Úplné a neúplné teorie. Teorie SUCC.
2. března 2017
Užití věty o korektnosti pro prokazování nedokazatelnosti. Sporné a bezesporné teorie. Věta o úplnosti.
D. cv. Nedokazatelnosti v axiomatické teorii se týká cv. 8. Cvičení 4‑7 jsou řešitelná také, přičemž ale 4 zvlášť zajímavé není, kdežto 5‑7 jsou možná trochu obtížnější.
28. února 2017
Opakování logické sémantiky: platnost formule ve struktuře, splněnost formule ve struktuře určitým ohodnocením, některé prominentní struktury, logicky platné formule.
D. cv. Logicky platných formulí se týká cv. 1.
23. února 2017
Složitější důkaz v teorii s axiomy Q1 a Q2. Věta o korektnosti. Model teorie.
21. února 2017
Pojmy potřebné pro definici hilbertovského kalkulu pro predikátovou logiku s rovností a pro definici axiomatické teorie: volné a vázané výskyty proměnných, sentence, axiomy specifikace, substituce a substituovatelné termy, 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

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 2016/17 (Czech)

16. května 2017
Úlohy ve třídě NP. Řády prvků v grupách. Cyklické grupy. Z toho, že 3 má v grupě Φ(31) řád 30, plyne, že 31 je prvočíslo. Což je ovšem jasné. Avšak naprosto analogicky z toho, že 37 má v grupě  Φ(261 - 1) řád 261 - 2, plyne, že i 261 - 1 je prvočíslo, což je netriviální výsledek.
9. května 2017
Šifrovací metoda RSA. Výsledek F. Colea týkající se čísla 267 - 1.
2. května 2017
Výpočet hodnot Eulerovy funkce.
25. dubna 2017
Komutativní (čili Abelovy) grupy. Eulerova grupa čísla m. Eulerova (Malá Fermatova) věta: umocníme-li v konečné grupě libovolný její prvek na počet prvků grupy, dostaneme jedničku (té grupy).
18. dubna 2017
Je-li číslo a dělitelné navzájem nesoudělnými čísly, je dělitelné i jejich součinem. Důkaz (nekonstruktivní) Čínské zbytkové věty. Pseudoprvočísla a použití Čínské zbytkové věty k důkazu, že 341 je pseudoprvočíslo.
11. dubna 2017
Věta o krácení v oboru integrity. Použití Bezoutovy věty k důkazu ekvivalentní podmínky pro nesoudělnost: nenulová a a b jsou nesoudělná právě tehdy, když a je dělitelem každého čísla z, pro které platí, že a je dělitelem čísla bz.
4. dubna 2017
Umocňování v okruhu Zm jako polynomiálně počitatelná operace. Tělesa a obory integrity. Dělitelnost v oboru integrity.
28. března 2017
Charakterizace invertibilních prvků v okruhu Zm. Díky (zobecněnému čtyřsloupcovému) Eukleidovu algoritmu lze o invertibilitě v Zm rozhodovat a inverzní prvky určovat v polynomiálním čase.
21. března 2017
Modulární aritmetika. Axiomy okruhu a jejich bezprostřední důsledky. Opačné a inverzní prvky.
Cvičení. Určete, které prvky okruhu Z15 jsou invertibilní.
14. března 2017
Dělitelnost a Eukleidův algoritmus v oboru celých čísel. Zobecněný (ctyřsloupcový) Eukleidův algoritmus, který najde řešení Bezoutovy rovnice.
D. cv. Kromě cvičení 1 je teď řešitelné i cvičení 4.
7. března 2017
Eukleidův algoritmus: jeho korektnost a fakt, že pracuje v polynomiálním čase. Bezoutova rovnice je rovnice tvaru ax + by = c (v oboru celých čísel, jedna rovnice pro dvě neznámé). Není-li c dělitelné největším společným dělitelem čísel a a b, tato rovnice řešení nemá.
D. cv. Cvičení 1 v seznamu nahoře.
28. února 2017
Úlohy počitatelné v kvadratickém, lineárním resp. polynomiálním čase. Rozlišení úloh FactoringPrimes: pouze první z nich (pravděpodobně) není počitatelná v polynomiálním čase. Všechny ostatní zatím uvažované polynomiálně počitatelné jsou: o úloze GCD to příště celkem snadno zdůvodníme, avšak dokázat to o úloze Primes je obtížný výsledek, který zůstane za obzorem kursu.
21. února 2017
Dělitelnost, prvočísla a největší společný dělitel. Úlohy a algoritmy. Některé důležité úlohy: Násobení, Primes, GCD.

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