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.

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.

Modal and non-classical logics

SIS ALG119008, Zoom cuni-cz.zoom.us/j/99702828164.

Exams

Please prepare answers/explanations to the following list of topics.

Course contents in Fall 2020/21 (Czech)

7. ledna 2021
Standardní překlad modální logiky do klasické predikátové logiky. Věta o úplnosti a rozhodovací procedura pro logiku GL.
Cvičení. Standardní překlad prosím konfrontujte s (opravte dle) toho, co píše van Benthem v úvodní kapitole ke knize Handbook of Modal Logics.
17. prosince 2020
Věta o úplnosti a rozhodovací procedura pro logiku K. Věta o eliminovatelnosti řezů, finite model property. Odvozená pravidla A / AAA / A (Löbovo pravidlo LR).
Cvičení. Je-li A libovolná formula a označíme-li B formuli □(□AA)→□A, pak v logice K4 lze dokázat formuli □BB. Takže logiku GL lze také axiomatizovat přidáním pravidla LR k logice K4.
10. prosince 2020
Gentzenovský kalkulus pro logiku K a důkaz jeho úplnosti.
3. prosince 2020
Varianty axiomatizace logiky GL: z L lze dokázat schéma 4, z H a 4 lze dokázat L. Gentzenovský kalkulus pro klasickou výrokovou logiku. Varianty pravidel.
26. listopadu 2020
Bisimulační kontrakce modelu. Cresswellův model demonstrující, že schémata H a L nejsou ekvivalentní.
19. listopadu 2020
Bisimulace, podmodely a disjunktní sjednocení modelů (rámců). Příklady tříd rámců, které nejsou charakterizovatelné: nereflexivní rámce, antireflexivní rámce, rámce 〈W,R〉, kde R = W2, a antisymetrické rámce.
Cvičení. Uvažujte modely M a N z přednášky (v M je cyklus z r do s a zpět a navíc r vidí t a s vidí u, kdežto v N je obdobný cyklus z c do d a zpět a dvě další šipky do e a do f, ale obě začínají v d). Najděte formuli neobsahující atomy, která platí jen v jednom z těchto modelů.
12. listopadu 2020
Přehled charakteristických tříd různých logik. Modely a rámce generované prvkem.
Cvičení. Domyslete důkaz tvrzení, že "schéma 5", čili schéma ◇A→□◇A, charakterizuje eukleidovskost.
5. listopadu 2020
Charakteristické třídy logik K4, T, B, H a L.
Cvičení. Nalezněte logiku, která charakterizuje eukleidovskost. Domyslete úvahu týkající se charakterizace lokálně silně souvislé relace.
29. října 2020
Logiky T a K4. Charakteristické třídy logik.
Cvičení (formulace upravena 31.10.). Domyslete tvrzení, že logika K + ◇A→◇◇A charakterizuje hustotu (relace dosažitelnosti). Najděte logiku, která charakterizuje symetrii.
22. října 2020
Schéma K a hilbertovský kalkulus pro logiku K. Věta o korektnosti této logiky vůči kripkovské sémantice.
Cvičení. S využitím tautologií a tautologických důsledků zdůvodněte, že všechny instance schématu A & □B → □(A & B) jsou v hilbertovském kalkulu pro logiku K dokazatelné. Formule p → □□p ale dokazatelná není.
15. října 2020
Ještě kripkovská sémantika.
Cvičení. Uvažujte rámec 〈W,R〉, kde W = {a,b,c} a R = {[a,b],[b,c],[c,c]}. Takže a vidí pouze b, kdežto b a c vidí c a nic jiného. Atom p je splněn v b a v c, ale ne v a, ostatní atomy jsou všude nesplněny. Dokažte, že b a c nelze odlišit žádnou modální formulí, tj. že každá modální formule, která je splněna v b, je splněna i v c.
8. října 2020
Věta o kompaktnosti v klasické výrokové logice. Kripkovské rámce a kripkovské modely pro modální výrokovou logiku.
Domácí cvičení. Uvažujte rámec se čtyřmi vrcholy 1, 2, 3 a 4, v němž z 1 jsou dosažitelné vrcholy 3 a 4, z 2 je dosažitelný 1, z 4 jsou dosažitelné 4 a 2. Atom p je splněn ve vrcholech 1 a 2. Ve kterých vrcholech je splněna formule ◇□◇p?
1. října 2020
Opakování klasické výrokové logiky: logické spojky, tautologie, ekvivalentní formule, důsledek.
Domácí cvičení. Promyslete následující variantu Příkladu 1.1.7 v knize [Šv02]. Nechť množina Γ výrokových formulí je definována jako { pipi+1 ; i ∈ N }. Které z formulí tvaru pipj jsou logickým důsledkem (vyplývají) z množiny Γ? Je pravda, že ta, která vyplývá, vyplývá i z některé konečné podmnožiny množiny Γ? Z které?

Properties of axiomatic theories

SIS ALG119006, Zoom Tue, Zoom Thu.

Excercises

Please pay attention to the list of excercises (minor corrections Jan 30 and Feb 4).

Exams

Ke zkoušce si prosím připravte seznam dvaceti cvičení, která dovedete řešit.

Course contents in Fall 2020/21 (Czech)

7. ledna 2021
První Gödelova věta: každé korektní rekurzívně axiomatizovatelné rozšíření T Robinsonovy aritmetiky, které je formulované v aritmetickém jazyce, je neúplné a nerozhodnutelné.
Cvičení. Zdůvodněte, že předpoklad o rekurzívní axiomatizovatelnosti nehraje roli pro tvrzení o nerozhodnutelnosti.
5. ledna 2021
Věta o Σ-úplnosti Robinsonovy aritmetiky: každá Σ-sentence platná v ℕ je v Q dokazatelná.
22. prosince 2020
Ještě Δ0-definovatelnost mocniny. Důležitá (avšak nedokázaná) ingredience budoucího důkazu První Gödelovy věty o neúplnosti: každá RE relace je Σ1-definovatelná. Věta o dokazatelnosti v Robinsonově aritmetice.
17. prosince 2020
Δ0-formule a Σ1-formule. Každá Δ0-definovatelná množina je rekurzívní. Takže každá Σ1-definovatelná je RE. Množina { [n,k,m] ; m=nk } je Δ0-definovatelná.
15. prosince 2020
Užití eliminace kvantifikátorů k charakterizaci definovatelných množin v určité struktuře. Například, každá množina přirozených čísel definovatelná ve struktuře 〈N,0,s,<〉 je buď konečná, nebo má konečný komplement. Omezené formule (Δ0-formule).
Cvičení. Najděte Δ0-formuli, která ve struktuře ℕ definuje množinu všech mocnin dvojky.
10. prosince 2020
Sjednocení a průnik RE množin je opět RE množina. Definovatelné podmnožiny a prvky struktur.
Cvičení. Dokažte, že sentence x(xmx=0 ∨ x=1 ∨ . . ∨ x=m)x(xmmx) jsou v Robinsonově aritmetice dokazatelné pro každé m.
Cvičení. Projekce RE množiny je opět RE množina.
8. prosince 2020
Postova věta, věta o projekci. Aplikace Postovy věty v logice: každá úplná rekurzívně axiomatizovatelná teorie je rozhodnutelná.
Cvičení 1. Když X a Y jsou RE úlohy takové, že XY = ∅ a XY je rekurzívní, pak X i Y je rekurzívní.
Cvičení 2. Nechť teorie T v jazyce L má pouze n navzájem neekvivalentních úplných rozšíření T1, . . ,Tn formulovaných v tomtéž jazyce L. Pak Thm(T) = ⋂iThm(Ti). Takže když všechny Ti jsou rozhodnutelné, i T je rozhodnutelná.
3. prosince 2020
Rekurzívní množiny jsou uzavřeny na booleovské operace. Rekurzívně spočetné (RE) množiny. Každá rekurzívní množina je RE. Projekcí rekurzívní množiny vznikne množina, která je RE.
1. prosince 2020
Kódování syntaktických objektů pomocí přirozených čísel. Rekurzívně axiomatizovatelné teorie. Robinsonova aritmetika Q.
Cvičení. Zdůvodněte, že sentence 5+2=75·2=10 jsou dokazatelné v Q. Také sentence xy(x+y=0 → x=0 & y=0) je dokazatelná. Avšak sentence x(0+x=x)x(0·x=0) dokazatelné nejsou.
26. listopadu 2020
Algoritmy, úlohy, rozhodnutelné teorie.
24. listopadu 2020
Axiomatizaze struktury 〈R,+,0,1〉.
Cvičení. Zůstalo nevyjasněné, jestli je nutné přidat k axiomům ještě schéma xy(nx=nyx=y).
19. listopadu 2020
Eliminace kvantifikátorů pro teorii DOS. Z toho plyne úplnost obou teorií DOS a DO.
Cvičení (nepovinné). Podobně lze dokázat úplnost pro teorii DNO (za předpokladu, že mezi logickými symboly jsou symboly pro pravdu a nepravdu) a pro teorii SUCC. Obtížnější ale pořád pravděpodobně zvládnutelný je projekt axiomatizovat strukturu 〈R,<,+,0,1〉.
12. listopadu 2020
Modelová podmínka pro konzervativní rozšíření. Teorie DOS jako konzervativní rozšíření jak teorie SUCC, tak teorie DO. První kroky v důkazu její úplnosti.
10. listopadu 2020
Varianty Löwenheimovy-Skolemovy věty. Neaxiomatizovatelnost třídy všech silně souvislých orientovaných grafů. Rozšíření a konzervativní rozšíření teorie.
Cvičení nezadáno, ale prohlédněte si prosím ty varianty Löwenheimovy-Skolemovy věty, zvlášť přehledně to dnes řečeno nebylo.
5. listopadu 2020
Axiomatizovatelné (tj. elementární) a konečně axiomatizovatelné třídy struktur.
Cvičení. Dokažte s užitím věty o kompaktnosti, že je-li třída struktur axiomatizovatelná a její komplement také, pak jsou obě konečně axiomatizovatelné.
3. listopadu 2020
Vaughtův test, κ-kategorické teorie. Úplnost teorií SUCC a DNO. Charakterizace modelů teorie DO: všechny struktury tvaru ω + (ω*+ω)·λ, kde λ je libovolný model teorie LO.
Cvičení. Formulujte bezespornou teorii v prázdném jazyce, která nemá žádné konečné modely. Pomocí Vaugtova testu dokažte její úplnost. Je teorie s prázdným jazykem a jediným axiomem ∀xy(x=y) úplná?
29. října 2020
Izomorfní a elementárně ekvivalentní struktury. Charakterizace modelů teorie SUCC: všechny struktury tvaru 〈N,0,s〉 + 〈Z,s〉·λ, kde λ je libovolný kardinál.
Cvičení: tentokrát nezadáno.
27. října 2020
Úplné teorie. Důkaz Löwenheimovy-Skolemovy věty s použitím věty o kompaktnosti. Teorie SUCC jako kandidát na úplnou teorii.
Cvičení. Pro strukturu 〈N,<〉 nebo pro strukturu  〈Q,<〉 vytipujte teorii, která ji axiomatizuje.
22. října 2020
Věta o silné úplnosti, věta o kompaktnosti a dvě verze Löwenheimovy-Skolemovy věty. Souvislosti mezi nimi.
Cvičení. Pro každou ze struktur 〈N,<〉, 〈Z,<〉 〈Q,<〉 (přirozená, celá resp. racionální čísla s ostrým uspořádáním) nalezněte sentenci, která v ní platí, ale neplatí v ostatních dvou.
20. října 2020
Souvislosti mezi větou o korektnosti (jejím důkazem), definicí vyplývání a logicky platnými formulemi. Sporné a bezesporné teorie.
Cvičení. Uvažujte teorii s prázdným jazykem a prázdnou množinou axiomů. Popište všechny její modely. Najděte příklady sentencí, které platí jen v některých z nich.
15. října 2020
Teorie struktury, logicky platné formule, model teorie.
Cvičení. Fragment teorie množin z minulé hodiny (to cvičení 21) je pořád aktuální. Dále cvičení 2 na straně 156, ale většinu jsme již vyřešili. Je některá z formulí x(P(x) → ∀yP(y)) a x(P(x) → ∀yP(y)) logicky platná?
13. října 2020
Tarského definice, platnost formule ve struktuře, logicky platné formule. Věta o korektnosti: každá formule dokazatelná z množiny předpokladů platí v každé struktuře, v níž platí všechny předpoklady.
Cvičení. Domácí úkol se sentencemi (iv) a (v) z minulého týdne je pořád aktuální. Řešitelné je také cvičení 21 na straně 182 knihy [Šv02].
8. října 2020
Hilbertovský kalkulus. Syntaktické pojmy: důkaz, modus ponens, pravidla generalizace, výrokové axiomy, axiomy specifikace, axiomy rovnosti, věta o dedukci.
Domácí cvičení. Připomeňte si větu o korektnosti a pokuste se ji použít ke zdůvodnění, že sentence (iv) x(S(x)≠x) a (v) x(x=0 ∨ ∃y(x=S(y))) nejsou dokazatelné v teorii s axiomy Q1 a Q2.
6. října 2020
Formální a neformální důkazy (tří sentencí z minulé hodiny). Užití (výrokových) tautologií a tautologického důsledku při konstrukci důkazů v hilbertovském kalkulu pro klasickou predikátovou logiku s rovností. Ručně psanými poznámkami se moc chlubit nemohu (prosím nešířit), ale třeba trochu pomohou.
Domácí cvičení. (a) Podejte příklad termu, který je substituovatelný za nějakou proměnnou v nějaké formuli, a jiného termu, který substituovatelný není (třeba za tutéž proměnnou v téže formuli). (b) Nalezněte důkaz (neformální nebo i formální) sentence x(P(F(x)) ∨ ¬P(x)) v teorii, která má prázdnou množinu axiomů, unární predikát P a unární funkční symbol F.
1. října 2020
Formule klasické predikátové logiky s rovností.
Domácí cvičení. Uvažujte teorii s jazykem {0,S} a s axiomy xy(S(x)=S(y) → x=y)x(S(x)≠0). Nalezněte neformální důkazy následujících sentencí: (i) S(0)≠0, (ii) S(S(0))≠S(0), (iii) xy(S(y)≠x).

Arithmetics and algorithms

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

SIS ALG110008, Zoom.

Exams (Czech)

Zkouška může proběhnout pokud možno co nejdříve v termínu dle domluvy (preferuji Po a Út dle celkem kdykoliv, St navečer a Pá ráno). Mám pro tento účel rezervované termíny 25.5., 8.6. a 29.6. vždy od 15h v Hlavní budově, ale není nutné se omezovat na tyto doby. Ke zkoušce si prosím připravte (přineste) řešení jedenácti cvičení vybraných z množiny 1 až 14 (i s vysvětlením matematického či algoritmického pozadí). Zkouška by v každém případě měla zahrnout i prodiskutování některého důkazu. Zkoušku přes Zoom nevylučuji.

Course contents in Spring 2020/21 (Czech)

13. května 2021
Kryptografická metoda RSA. Důkaz její korektnosti pomocí modulárních reprezentací. Mersennova prvočísla a Coleův výsledek z roku 1903 týkající se čísla 267 - 1. Neformální vysvětlení, co je třída NP (úloh rozhodnutelných v tzv. nedeterministickém polynomiálním čase).
6. května 2021
Čínská zbytková věta: když m je součin navzájem nesoudělných čísel p1,..,pn a [r1,..,rn] je n-tice čísel takových, že 0 ≤ ri < pi, pak [r1,..,rn] je modulární reprezentací nějakého (ale jediného) a ∈ ℤm. Užití modulárních reprezentací k důkazu, že 341 je pseudoprvočíslo.
29. dubna 2021
Umocňování v okruhu ℤm. Pseudoprvočísla. Modulární reprezentace.
22. dubna 2021
Eulerova grupa a Eulerova funkce. Eulerova (Malá Fermatova) věta.
Cvičení. Užijte Eulerovu větu a případně i Bezoutovu větu a spočítejte 7107 v ℤ27. Určete číslo φ(100).
15. dubna 2021
Komutativní monoidy, Abelovy grupy a komutativní okruhy. Eulerova grupa okruhu ℤm.
Cvičení. Kolik prvků má Eulerova grupa okruhu ℤm, když m je prvočíslo? Kolik má prvků, když m je součin dvou různých prvočísel?
8. dubna 2021
Přehled důsledků Bézoutovy věty pro prvočíselnost, nesoudělnost, společný násobek a určování inverzních a invertibilních prvků v ℤm.
Cvičení nezadáno, avšak nahlédněte prosím nahoře do pdf souboru s cvičeními.
1. dubna 2021
Opakování a zpřesnění ireducibilních čísel a prvočísel. Inverzní a invertibilní prvky ve struktuře ℤm.
Záznam přednášky: těm, kteří se nemohli zúčastnit, možná pomohou poznámky nebo videozáznam celé přednášky. Ale moc dobré studijní materiály to nejsou, takže zájemcům nabízím individuální konzultaci. Videozáznam z mého počítače spustit šel, ale kdyby z Vašeho nešel, ozvěte se, mám od Zoomu ještě heslo.
Cvičení. Dokažte (užitím Bezoutovy věty na a a b), že když a a b jsou nesoudělná, pak splňují podmínku z(abzaz). Vysvětlete, že pokud a a b tuto podmínku splňují, nemusí být nesoudělná.
25. března 2021
Užití Bézoutovy věty k důkazu, že každé ireducibilní číslo je prvočíslo. Definice komutativního okruhu.
Cvičení. Jak je třeba opravit definice, aby vyšlo, že každé prvočíslo je ireducibilní?
17. března 2021
Bézoutova věta. Zobecněný (čtyřsloupcový) Eukleidův algoritmus pro nalezení řešení Bézoutovy rovnice.
Cvičení. Pro která čísla c je rovnice 78x + 21y = c řešitelná?
11. března 2021
Když n není prvočíslo, pak ani 2n - 1 není prvočíslo. Teoretický důsledek Eukleidova algoritmu: každá dvě celá čísla mají společného dělitele, který je dělitelný všemi jejich společnými děliteli. Obecné definice pojmů týkajících se dělitelnosti (největší společný dělitel, nesoudělná čísla, ireducibilní čísla). Oprava (doplnění) k číslu 0: dvě čísla definujeme jako soudělná, jestliže nejsou nesoudělná, čili jestliže mají společného dělitele, který není dělitelem jedničky. Pak vyjde, že nula je nesoudělná s děliteli jedničky, soudělná se všemi ostatními čísly.
Cvičení. Zdůvodněte, že rovnice 4495x + 2356y = 160 nemá v oboru celých čísel řešení.
4. března 2021
Eukleidův algoritmus pro úlohu GCD. Jeho časové nároky.
Cvičení. Nalezněte největšího společného dělitele čísel 829 931715 997.
25. února 2021
Časové nároky algoritmů. Algoritmy pracující v polynomiálním čase, tj. polynomiální algoritmy. Polynomiálně počitatelné úlohy. Dělitelnost v oboru celých čísel. Vlastnosti relace dělitelnosti.
18. února 2021
Úlohy a algoritmy. Úlohy Mult, Factoring, GCDPrimes, 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.

Incompleteness and Gödel Theorems

Here is an (incomplete) list of excercises.

SIS ALG119007, Zoom.

Course contents in Fall 2020/21

18. května 2021
Disjunction property. Harropovské formule.
13. května 2021
Kripkovské modely pro intuicionistickou výrokovou logiku. Persistence, vzájemná nevyjádřitelnost logických spojek. Ostatní sémantické pojmy (vyplývání...).
11. května 2021
Interpretovatelnost sentencí Con(τ) a ¬Con(τ).
6. května 2021
Souvislost formalizované konzistence s interpretovatelností: teorie T je interpretovatelná v každé teorii S, která je rozšířením PA a je v ní dokazatelná bezespornost T.
4. května 2021
Podstatná neúplnost a podstatná nerozhodnutelnost. Každá bezesporná rozhodnutelná teorie má rozšíření (se stejným jazykem), které je rozhodnutelné a úplné.
29. dubna 2021
Rosserova věta a její formalizace v PA. Aplikovatelnost modální logiky v metamatematice.
27. dubna 2021
Důkaz Löbovy věty převedením na Gödelovu větu. Rosserova sentence.
22. dubna 2021
Souvislost Druhé Gödelovy věty s modální logikou. Löbova věta. Löbova rovnice také má jednoznačně určené a explicitně vyjádřitelné řešení.
20. dubna 2021
Druhá Gödelova věta. Některé souvislosti, Hilbertův program.
15. dubna 2021
Druhá Gödelova věta. Její formalizace v PA. Gödelova autoreferenční rovnice má jednoznačně určené a navíc explicitně vyjádřivelné řešení, totiž sentenci vyjadřující konzistenci.
13. dubna 2021
Slabá reprezentovatelnost funkcí v Q. Různé autoreferenční sentence: Gödelova, Henkinova plus dva dodatečné (školní) příklady, které demonstrují, že autoreferenční sentence může tvrdit něco nejen přímo o sobě, ale i o výsledku zpracování sebe sama nějakou Δ0-definovatelnou funkcí, a druhý navíc ukazuje, že řešení autoreferenční rovnice nemusí být určené jednoznačně.
8. dubna 2021
Věta o autoreferenci. Gödelova sentence a Henkinova sentence.
6. dubna 2021
Podmínky pro dokazatelnost (Löbovy podmínky). Některé jejich důsledky.
1. dubna 2021
Formalizovaná bezespornost. Formalizované numerály a formalizovaná věta o Σ-úplnosti.
30. března 2021
Podmínka D1. Dokazatelnost bezespornosti teorie, která má prázdnou množinu axiomů (jazyk libovolný). Existence definice π*(z) Peanovy aritmetiky, pro kterou platí PA ⊢ Con(π*).
25. března 2021
Vlastnosti formalizované dokazatelnosti. Přirozené definice teorií Q a PA. Formalizovaná věta o dedukci. Podmínka D2 (Löb's second derivability condition).
23. března 2021
Princip kolekce. Σm(PA)- a Πm(PA)-formule.
18. března 2021
Formalizace syntaktických pojmů, včetně pojmů důkaz, dokazatelnost a bezespornost.
16. března 2021
Formalizace termů, kvazitermů a formulí v Peanově aritmetice.
11. března 2021
Počítání jedniček v binární expanzi čísla. Z toho plyne možnost počítat znaky v textových řetězcích. Formalizace některých syntaktických pojmů (proměnné, numerály).
Cvičení. Nechť slovo u je vyvážený podřetězec slova w vymezený čísly i1 a j1 (v tom smyslu, že nejlevější znak slova u je na pozici i1, kdežto j1 určuje první pozici za u, takže u má délku j1 - i1). Nechť v je jiný vyvážený podřetězec slova w vymezený čísly i2 a j2 a platí i1i2 < j1. Pak j2j1.
9. března 2021
Formalizace pojmů v PA: prvočísla, mocniny dvojky, exponenciální funkce. Existují modely PA obsahující nestandardní Δ0-definovatelné prvky.
4. března 2021
V PA lze dokázat Bezoutovu větu. Dále, ireducibilní čísla jsou přesně ta čísla, která jsou prvočísly, a je jich nekonečně mnoho.
2. března 2021
Ekvivalennce schémat Ind a LNP nad Robinsonovou aritmetikou s jedním dodatečným axiomem. Vlastnosti operací a uspořádání dokazatelné v PA. Dělení se zbytkem.
25. února 2021
Schémata Ind a LNP. Teorie R. Nestandardní model Robinsonovy aritmetiky, v němž leccos neplatí, avšak schéma LNP platí. Užití schématu Ind k důkazům vlastností operací.
23. února 2021
Hierarchie aritmetických formulí. Axiomy Robinsonovy aritmetiky Q. Q není konzervativním rozšířením teorie s axiomy Q1-Q5, ta ale je konzervativním rozšířením teorie s axiomy Q1-Q3.
18. února 2021
Struktura nestandardního modelu teorie Th(ℕ). Δ0-formule, jejich důležité příklady.
16. února 2021
Opakování: kalkuly, struktury, uspořádané množiny, struktura přirozených čísel; izomorfismus a elementární ekvivalence.

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.

Exams (Czech)

Ke zkoušce je třeba zvládnout témata dle vlastního výběru, která pokrývají 13 dvouhodinovek. Vlastní referát se do počtu 13 počítá trojnásobně.

Course contents in 2019/20 (Czech)

Konce semestru (18. května)
Na posledním setkání 5.5. domluveno, že během nadcházejícího víkendu (10.5.) dá pan Štefanišin vědět, jestli má smysl se ještě jednou setkat. V tom případě by připadalo v úvahu Po 18.5. odpoledne (nebo v Út 19.5. v 9:10). 12.5. se nescházíme.
Gentzenův důkaz bezespornosti Peanovy aritmetiky (J. Štefanišin, 14. až 5. května, 3)
Přednášeno dle diplomové práce Anny Horské.
Pudlákův spodní odhad pro eliminovatelnost řezů (J. Urbánek, 7. a 13. dubna, 2)
Pudlákova exponenciální aritmetika PEX, superexponenciální spodní odhad.
Eliminovatelnost řezů pro klasickou predikátovou logiku (J. Rýdl, 24. března, 2)
Z více důkazů je do mé knihy převzat ten, který vychází ze Schwichtenbergovy kapitoly v Handbooku (Barwise), ale je upraven pro kalkulus se všemi logickými symboly a se sekventy jako množinami.
Rozhodnutelnost a kripkovská úplnost logiky dokazatelnosti (V. Švejdar, 17. března, 1)
Zpětným užitím pravidel gentzenovského kalkulu lze získat buď bezřezový důkaz, nebo kripkovský protipříklad. Téma malinko navazuje na předchozí, protože argument, že algoritmus konverguje (termination argument) není zcela triviální.
Dobrá uspořádání v teoretické informatice (J. Štefanišin, 3. března, 2)
U složitějšího algoritmu může vzniknout problém jak dokázat, že se na každém vstupu dopočítá a že je korektní. To lze řešit pomocí nějaké vhodně vymyšlené terminační funkce, ale lze i definovat vtipné multimnožiny a využít obecnou větu, která se týká jejich dobrého uspořádání.
Turingovy stroje (Š. Laichter, 2)
Původní článek obsahující definici Turingova stroje (ne úplně shodnou s dnes používanými). K Busy Beaver Competition pan Laichter dává k dispozici články [Rado62] a [ShenLinRado65].
Logika dokazatelnosti (V. Švejdar, 5)
PA-tautologie a ℕ-tautologie. Logiky K a K4. Charakteristické třídy logik. Kalkuly pro logiku dokazatelnosti.
Autoreference (J. Urbánek, 2)
Je známo (a v přednášce bylo trochu naznačeno) Gödelova-Bernaysova teorie množin GB (nověji bývá označována NBG) je konzervativní nad ZF vůči množinovým sentencím a je konečně axiomatizovatelná. V jazyce teorie GB lze napsat formuli (vlastnost přirozených čísel) J(x), která je vlastním řezem: sentence J(0) a x(J(x) → J(S(x))) v GB dokázat lze, ale x(J(x)) dokázat nelze. Toto je pravděpodobně Vopěnkův výsledek: plná indukce (pro všechny formule) v GB neplatí. Konstrukce řezu také ukazuje, jaký problém by vznikl, kdybychom chtěli zobecnit logickou sémantiku (rozšířit Tarského definici) tak, aby se jako struktury a modely teorií připouštěly i vlastní třídy.
Autoreference (V. Švejdar, 5)
Větu o autoreferenci lze chápat jako větu o řešitelnosti rovnice pro neznámou sentenci. Löbovo řešení Henkinova problému vlastně ukazuje, že Henkinova rovnice má jednoznačně určené řešení (každá dvě řešení jsou dokazatelně ekvivalentní). Také Gödelova rovnice má jednoznačně určené řešení. Existují ale rovnice, pro které to neplatí. Rozdíl mezi Gödelovou a Rosserovou sentencí: v případě Gödelovy sentence lze v PA formalizovat důkaz její nedokazatelnosti, ale důkaz její nevyvratitelnosti formalizovat nelze, kdežto v případě Rosserovy sentence lze v PA formalizovat jak důkaz nedokazatelnosti, tak důkaz nevyvratitelnosti.

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