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.

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í (s využitím přinesených poznámek) 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 2018/19 (Czech)

10. ledna 2019
Zobecněná primitivní rekurze (course-of-values recursion). Množina je rekurzívně spočetná, právě když je konečná nebo je oborem hodnot nějaké prosté rekurzívní funkce. Prosté (simple) množiny. Prostá množina S očividně nemůže být rekurzívní, ale do přednášky se už nevešla úvaha, že nemůže být ani Σ1-kompletní. Pokud by totiž byla Σ1-kompletní, pak by na ni byla převeditelná množina K, takže na její komplement - S by byla převeditelná množina - K, takže - S by byla produktivní a měla by tedy nekonečnou rekurzívně spočetnou podmnožinu.
8. ledna 2019
Každá produktivní množina má nekonečnou rekurzívně spočetnou podmnožinu. Kódování konečných posloupností.
3. ledna 2019
Operace primitivní rekurze. Množina je Δ1, právě když je oborem hodnot nějaké rostoucí rekurzívní funkce.
20. prosince 2018
Věta o pevném bodu. Indexové množiny. Riceova věta: indexová množina A není převeditelná na vlastní komplement; takže pokud navíc A ≠ ∅A ≠ N, množina A není rekurzívní. Vyřešeno cvičení 30.
18. prosince 2018
Produktivní množiny. Množina K je produktivní. Každá množina, na kterou je převeditelná produktivní množina, je také produktivní. Důkaz věty o rekurzi (jednoduché verze týkající se rovnice pro neznámě číslo).
13. prosince 2018
Další příklady na převody: množiny Unb a Tot jsou Π2-kompletní. Vyřešeno cvičení 26.
11. prosince 2018
Důsledek věty o parametrech vhodný ke konstrukci převodů.
6. prosince 2018
Užití věty o parametrech ke konstrukci převodů: například množina K je Σ1-kompletní.
4. prosince 2018
Existence Σn- a Πn-kompletních množin. Existence nejmenších horních závor vůči m-převeditelnosti.
29. listopadu 2018
M-převeditelnost a její vlastnosti. Důležitá vlastnost množiny K0: každá RE množina je na ni m-převeditelná.
27. listopadu 2018
K problematice rekurzívnosti grafu a definičního oboru funkce vyřešena cvičení 9 a 19. Patří k tomu také cvičení 20. Prominentní množiny Tot, Unb a Rec. Tarského-Kuratowského algoritmus pro určení aritmetické klasifikace množiny.
22. listopadu 2018
Částečně rekurzívní funkce, která nemá žádné rekurzívní prodloužení. Existence dvojice disjunktních rekurzívně neoddělitelných RE množin. Věta o parametrech: znění a náznak důkazu.
20. listopadu 2018
Pro každou třídu Σn (je-li n nenulové) existuje univerzální relace, která je také Σn. Z toho plyne, že aritmetická hierarchie nekolabuje.
15. listopadu 2018
Enumerace částečně rekurzívních funkcí a rekurzívně spočetných množin. Diagonální metoda. Prominentní množiny K a K0.
13. listopadu 2018
Kódování syntaktických objektů, dokončení: konfigurace, výpočty, Turingův predikát. Věta o normální formě.
8. listopadu 2018
Kódování syntaktických objektů pomocí přirozených čísel obecně, a objektů souvisejících s vývojovými diagramy zvlášť. Zatím došlo na instrukce a diagramy.
6. listopadu 2018
Alternativní důkazy Postovy věty, náznak jejího významu v logice. Příklady na to, že když RE množina má určitou matematickou strukturu, musí být rekurzívní.
1. listopadu 2018
Věta o výběrové funkci (či o aproximaci RE množiny pomocí funkce): každá RE relace má podmnožinu se stejným oborem hodnot, která je částečně rekurzívní funkcí. Důsledky této věty jsou: (i) každá funkce, jejíž graf je RE, je FPartR, (ii) větvení podle rekurzívní podmínky jako odvozená operace s částečně rekurzívními funkcemi, (iii) Postova věta: Δ1 = Σ1Π1, (iv) věta o redukci (označení "věta o separaci" uvedené ve cvičení 11 pravděpodobně nesedí), (v) každé dvě Π1 množiny jsou rekurzívně oddělitelné.
D. cv. Cvičení 12.
30. října 2018
Ekvivalentní podmínky pro rekurzívní spočetnost: Množina (relace) je RE, právě když je projekcí nějaké Δ1 relace. A množina (relace) je RE, právě když je definičním oborem nějaké částečně rekurzívní funkce (této ekvivalenci se říká věta o projekci). Množina čísel je RE, právě když je prázdná nebo je oborem hodnot nějaké rekurzívní funkce.
25. října 2018
Mod, Div, párovací funkce a funkce l a r jsou příklady užitečných funkcí, jejichž rekurzívnost lze dokázat na základě toho, že mají Δ0 graf. Graf Každé částečně rekurzívní funkce je Σ1 čili rekurzívně spočetný. Z toho plyne, že Δ1 je podtřídou jak třídy Σ1, tak třídy Π1.
23. října 2018
Uzavřenost tříd ΣnΠn na operace. Každá Δ0 podmínka je rekurzívní. To dohromady s větou, že totální funkce je FGR, právě když její graf je Δ1, dává účinný i když ne vždy aplikovatelný nástroj pro prokazování rekurzívnosti funkcí.
18. října 2018
Δ0 podmínky (omezené podmínky). Aritmetická hierarchie. Důležité Δ0 množiny: množina všech prvočísel, množina všech mocnin dvojky.
16. října 2018
Odvozené metody pro prokazování rekurzívnosti (funkcí nebo množin): rekurzívní podmínky jsou uzavřeny na booleovské operace, dosazení rekurzívních funkcí do rekurzívní podmínky dá vždy rekurzívní podmínku, minimalizaci je legální uplatnit i na rekurzívní podmínku. To poslední je v seznamu cvičení (zatím) uvedeno pod číslem 4. Cvičení 1, 3, a 5 jsou také řešitelná (nebo už byla vyřešena).
11. října 2018
Každou FPartR počítá nějaký vývojový diagram. Triviální operace s částečně rekurzívními funkcemi: přidání jalové proměnné, dosazení konstanty, ztotožnění proměnných, permutace proměnných. Charakteristická funkce množiny, rekurzívní (Δ1) množiny.
D. cv. Dokažte, že neostré uspořádání, tj. množina { [x,y] ; xy }, je rekurzívní množina (dvojic).
9. října 2018
Definice částečně rekurzívních (FPartR) a rekurzívních (FGR) funkcí.
4. října 2018
Ještě vývojové diagramy. Z šesti instrukcí některé lze simulovat pomocí ostatních, ale některé nelze, a lze to dokázat. Částečné funkce k proměnných.
2. října 2018
Úvod: plánem je definovat pojem algoritmu a tím možnost klasifikovat úlohy jako algoritmicky rozhodnutelné a algoritmicky nerozhodnutelné. Ty nerozhodnutelné také hodláme spolu porovnávat. Vývojové diagramy.

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 2018/19 (Czech)

23. května 2019
Korektnost a úplnost kalkulu GJ vůči kripkovské sémantice. FMP, eliminovatelnost řezů, rozhodnutelnost. Glivenkova věta (věrný překlad klasické logiky do intuicionistické).
21. května 2019
Konstrukce kripkovských modelů. Disjunction property.
9. května 2019
Korektnost a úplnost kalkulu GK vůči sémantice klasické výrokové logiky. Kripkovská sémantika intuicionistické výrokové logiky.
7. května 2019
Pravidla sekventového kalkulu. Bezřezové důkazy. Korektnost pravidel.
2. května 2019
Klasický důkaz První Gödelovy věty a jeho prodloužení na důkaz Druhé Gödelovy věty. Formalizace Druhé Gödelovy věty v PA. Souvislosti s Hilbertovým programem, s modální logikou... Sekventové (gentzenovské) kalkuly.
25. dubna 2019
Užití rekurzívně neoddělitelných množin k důkazu Rosserovy věty: Robinsonova aritmetika je podstatně neúplná a podstatně nerozhodnutelná. Aritmetizace logické syntaxe a Löbovy podmínky.
23. dubna 2019
První Gödelova věta o neúplnosti, dokončení důkazu. Existence teorií, které jsou bezesporné, ale nikoliv Σ-korektní.
16. dubna 2019
Dokončení důkazu Σ-úplnosti Robinsonovy aritmetiky. Σ-korektní teorie. První Gödelova věta.
11. dubna 2019
Σ-úplnost Robinsonovy aritmetiky.
9. dubna 2019
Rozhodnutelné a nerozhodnutelné teorie. Craigův trik. Úplná a rekurzívně axiomatizovatelná teorie je rozhodnutelná. Rozhodnutelnost konečného rozšíření rozhodnutelné teorie.
4. dubna 2019
Užití eliminace kvantifikátorů k charakterizaci definovatelných množin v určité struktuře. Hierarchie aritmetických formulí a definovatelné množiny ve struktuře N.
2. dubna 2019
0-kategorické teorie, Vaughtův test, teorie DNO. Definovatelné množiny ve struktuře.
28. března 2019
Konzervativní rozšíření teorie a rozšíření teorie o definice. Teorie DOS připouští eliminaci kvantifikátorů, z čehož plyne, že ona i teorie DO jsou úplné.
26. března 2019
Eliminace kvantifikátorů pro teorii SUCC, dokončení. Teorie DO.
21. března 2019
Důkaz úplnosti teorie SUCC pomocí eliminace kvantifikátorů: první dvě ze tří pomocných tvrzení.
19. března 2019
Axiomatizovatelné (elementární) a konečně axiomatizovatelné třídy struktur. Věta o kompaktnosti jako nástroj pro prokazování, že některé třídy axiomatizovatelné nejsou.
14. března 2019
Důležité věty a souvislosti mezi nimi: úplnost, silná úplnost, kompaktnost, Löweheimova-Skolemova věta. Struktura nestandardního modelu Peanovy aritmetiky.
12. března 2019
V PA lze dokázat, že prvočísel je nekonečně mnoho. Vlastnosti axiomatických teorií: konečná axiomatizovatelnost, bezespornost, úplnost. Teorie struktury. Množiny Thm(T) a Ref(T).
7. března 2019
Schéma indukce je nad Q s dodatečným axiomem x(x < S(x)) ekvivalentní se schématem LNP. Všechna očekávaná tvrzení o sčítání a násobení přirozených čísel (obojí asociativita, distributivita, atd.) a o vztazích operací k uspořádání jsou v PA dokazatelná.
5. března 2019
Schémata dokazatelná v Robinsonově aritmetice. Peanova aritmetika. Jednoduché příklady na užití schématu indukce.
28. února 2019
Robinsonova aritmetika. Její jednoduchý nestandardní model.
26. února 2019
Platnost formule ve struktuře, definice vyplývání. Věta o korektnosti. Vyvratitelné a nezávislé sentence.
Všechna cvičení 1–8 jsou teď řešitelná.
21. února 2019
Dokončení přehledu logické syntaxe (k podrobné definici důkazu a k větě o dedukci). Struktury, realizace symbolů, Tarského definice.
19. února 2019
Opakování logické syntaxe: termy, formule, sentence, axiomy specifikace. Tautologie. Dokazatelnost v teorii 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 jedenácti cvičení, která umíte řešit (i s vysvětlením matematického pozadí), nebo jedno z témat uvedených v seznamu cvičení. Zkouška by v každém případě měla zahrnout i prodiskutování některého důkazu. Zkouška může proběhnout kdykoliv se domluvíme (ale raději to prosím moc neodkládejte) přes Hangouts (s kamerou) nebo při osobním setkání v Celetné.

Course contents in Spring 2019/20 (Czech)

18. května 2020
Prattův výsledek o certifikátech prvočísel (článek stojí za prohlédnutí, ale není to žádný požadavek ke zkoušce). K tomu prezentace: aa200518.pdf.
7. května 2020
Řády prvků v grupách. K tomu prezentace (doplněná a opravená): aa200507.pdf.
Domácí cvičení: Stanovte řády všech prvků v grupě Φ(9).
Závěr semestru: poslední přednáška je v pondělí 18.5., předtím ve čtvrtek 14.5. se setkání nekoná. Setkáme se opět virtuálně, a mimo jiné se domluvíme o datu a formě zkoušky.
30. dubna 2020
Mersennova prvočísla. Nekompletní prezentace: aa200430.pdf. Držíme se nového linku do Hangouts: https://hangouts.google.com/call/RSgb49Si_qLcnzEkRE16AEEI .
23. dubna 2020
Kryptografická metoda RSA. Prezentace: aa200423.pdf. Nadále používáme jiný link do Hangouts: https://hangouts.google.com/call/RSgb49Si_qLcnzEkRE16AEEI , ten dřívější přestal fungovat.
D. cv.: Cvičení 9 v seznamu nahoře.
20. dubna 2020 (v 10h nahrazujeme přednášku z 16. dubna)
Modulární reprezentace a čínská zbytková věta. Prezentace (aktualizovaná 20.4.): aa200416.pdf.
9. dubna 2020
Polynomiální algoritmus pro umocňování v ℤm. Důsledky Bézoutovy věty. Prezentace: aa200409.pdf (tato i předchozí prezentace trochu aktualizovány 9. dubna).
2. dubna 2020
Rozšířený Eukleidův algoritmus a Bezoutova věta. Url do Hangouts se stále nemění: https://hangouts.google.com/call/XpqIiz8M_U4mUcgkFC-DAEEI . Je zde v textové podobě, protože Hangouts očividně počítají s prohlížečem Chrome a není úplně jasné, co by udělal klik, kdyby tato stránka byla otevřena v prohlížeči Edge. Předpokládám tedy, že tu url vkopírujete do adresního řádku Chromu pomocí Ctrl-C a Ctrl-V (což například já dělám, protože jinak používám přednostně Edge). Prezentace: aa200402.pdf.
26. března 2020
Dělení, dělitelnost, Eukleidův algoritmus. K tomu prezentace: aa200326.pdf. Link do Hangouts se nemění: https://hangouts.google.com/call/XpqIiz8M_U4mUcgkFC-DAEEI .
19. března 2020
Eulerova věta týkající se umocňování v komutativních grupách. Souvislost invertibility s dělitelností. Komutativní okruhy. K tomu prezentace: aa200319.pdf. Na dobu určenou pro přednášku, čili Čt 10h, nabízím, že si prezentaci ústně projdeme pomocí aplikace Hangouts. Kdo se ozvete, pošlu ráno příslušný link.
20.3. prezentace rozšířena o obory integrity a o úvahy o opačných prvcích v okruzích.
12. března 2020
Komutativní (čili Abelovy) grupy. Krácení. Eulerova grupa Φ(m) čísla m jako prominentní příklad komutativní grupy.
Režim po dobu uzavření školy. Snažíme se o virtuální kurs. Což si představuji tak, že každé úterý zde dám k dispozici pokud svou možno podrobnou přípravu na přednášku, která by se konala ve čtvrtek. Ve čtvrtek dopoledne a v pondělí dopoledne jsem k dispozici k dovysvětlení a diskusi, možná hromadně ale určitě i individuálně, k obsahu přednášky. Myslím, že každý z vás by mě v této době měl každý týden kontaktovat. A pokud se to podaří realizovat a bude to trvat většinu zbývajícího semestru, budeme to považovat i za závěrečnou zkoušku. Pro komunikaci je možný email, nebo Whatsupp na telefonní číslo, které jsem rozeslal mailem, nebo přes whereby.com, pokud to rozchodíme. Po odpovědi jednoho z vás bych nevylučoval i setkání v nějaké kavárně, souhlasím s tím, že osobní setkání je lepší než nějaké technologie a myslím si, že je nás tak málo, že setkání by nesabotovalo snahy hygienických úřadů. Zde je obsah této přednášky: aa200312.pdf.
Cvičení. Které a kolik prvků mají grupy Φ(3) a Φ(4)? Které prvky jsou invertibilní ve struktuře <Z,·,1>?
5. března 2020
Modulární aritmetika. Některé ze základních algebraických struktur: komutativní monoid a komutativní grupa (Abelova grupa). Invertibilní prvky v komutativním monoidu. Pro každý prvek x komutativního monoidu existuje nejvýše jeden prvek y, který je k x inverzní.
Cvičení. Nalezněte všechny prvky struktury ℤ15, které jsou invertibilní vůči násobení.
27. února 2020
Dvě rozdílné úlohy týkající se prvočísel: PrimesFactoring. O první z nich je od roku 2002 známo, že je rozhodnutelná v polynomiálním čase, ale je to obtížný výsledek mimo obzor tohoto kursu. Polynomiální algoritmus pro Factoring znám není. Odborníci soudí, že nejspíš neexistuje, ale dokázané to není. Dvě úlohy z teorie grafů, které vypadají podobně, ale mají (pravděpodobně) velmi rozdílnou algoritmickou klasifikaci: Eulerian path (curcuit)Hamiltonian path (curcuit).
20. února 2020
Úlohy a algoritmy. Časové nároky algoritmů. Algoritmům pracujícím v lineárním, kvadratickém atd. čase se souhrnně říká polynomiální algoritmy. Příkladem je školní algoritmus pro Násobení. Pro úlohu Primes máme dva přirozené algoritmy, jeden z nich je sice lepší než ten druhý, polynomiální ale není ani jeden z nich.

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.

History of Modern Mathematics and Logic

SIS ALGV00120

Course contents in Fall 2019/20

December 19th, 2019
Orders of elements in Euler's groups. The order of a ∈ Φ(m) must be a divisor of φ(m). If m = 261 - 1, one can use a calculator and verify that the primes in the prime factorization of m - 1 are 2, 3, 5, 7, 11, 13, 31, 41, 61, 151, 331 and 1321. If p is any of these twelve primes, then in Φ(m) we have 37(m-1)/p ≠ 1, which can again be verified using the calculator. Thus neither (m-1)/p nor any of its divisors is the order of 37. Then from 37m-1 = 1 it is clear that the order of 37 is m - 1. It follows that m is prime, which is a not so trivial result because m is a big number.
December 12th, 2019
All operations in ℤm (addition, multiplication, invertibility, inverses and also exponentiation) are computable (decidable) in polynomial time. Thus only for prime factorization (the Factoring problem) and for the Euler's function φ we do not have polynomial algorithms. Euler's and Fermat's theorem. Pseudoprimes.
Homework. Download the calculator BNCalc.pdf to a Windows computer (I do not know whether it works on Apple computers) and do some experiments with all three pages in it. For example, verify that 341, 561, 645, 1105, 1387, 1729 and 1905 are pseudoprimes. Or, divide 7 by 10 in ℤ65536. Not using a computer (!), find the last two digits of 7122.
December 5th, 2019
Working with opposite elements in commutative rings. Euler's group of a number. Euler's function. Bézout's theorem and the extended Euclid's algorithm show that deciding about invertibility in ℤm and computing the inverses can be done in polynomial time.
Homework. Find all solutions of the equation 7x = 10 in ℤ65536. Compute φ(21) and φ(81).
November 28th, 2019
Brief survey of commutative monoids, groups and rings. Pre-Euler (abstract Euler) theorem concerning Abelian groups.
Homework. Which elements of ℤ15 are invertible?
November 21st, 2019
Commutative monoids and commutative (Abelian) groups.
Homework. Show that if x and y are any invertible elements of a commutative monoid <G,∗,e>, then xy must be invertible.
November 14th, 2019
The condition z(abzaz) (and its relationship to coprimeness) used to show that if a and b are coprime and both are divisors of c, then abc. Modular arithmetic. The notion of ring.
Homework. Prove that the conditions d(dpd ∣ 1 ∨ p ∣ d) and ab(pabp ∣ a ∨ p ∣ b) are for nonzero p equivalent.
Hint. The proof is similar to the proof concerning the equivalent conditions for coprimeness. When proving ab(…), apply Bézout's theorem to p and a.
November 7th, 2019
A survey of number problems we consider: GDC, coPrimes, Multiplication and Addition are computable in polynomial time. Factoring probably not, but it is an unproved conjecture. Surprisingly, Primes is decidable in polynomial time. This a a difficult result of Agrawal, Kayal and Saxena from 2002 whose verification lies far beyond the scope of this course. One of mathematical consequences of Bézout's theorem: nonzero numbers a and b are coprime if and only if they satisfy the condition z(abzaz). One half of a proof will be given next week.
October 31st, 2019
A naive algorithm for solvability of Bézout's equation ax + by = c based on the observation that it is sufficient to check only finitely many numbers x, namely those satisfying 0 ≤ x < b. The extended (four column) Euclid's algorithm operates in polynomial time. The algorithm also has a mathematical consequence: Bézout's theorem can be symbolically written as abxy(ax + bya & ax + byb).
Homework. Apply the extended Euclid's algorithm to the equation 4495x + 2356y = 155, and also to the equation 4495x + 2356y = 160.
October 24th, 2019
Official definitions of greatest common divisor, coprimes and prime. These definitions are language-efficient in the sense that they are expressed in terms of multiplication only, they do not employ notions like ordering or absolute value. Basic notions from theoretical computer science: problem, instances of a problem, input and output. Time requirements of algorithms. A common name for algorithms that operate in linear, or quadratic, or cubic, or … time is polynomial (time) algorithms. The grade school algorithms for Addition and Multiplication as well as Euclid's algorithm for GCD are polynomial algorithms. However, no polynomial algorithm for Factoring is known.
A correction. The name of the mathematician who in fact proved that Euclid's algorithm operates in polynomial time is Gabriel Lamé, not Gustav Lamé.
Homework. Try to find out whether there exists a pair x and y of integers that is a solution of the equation 54x + 51y = 7. A negative answer can be obtained by thinking about divisibility and about divisors of 54, 51 and 7. Try to think about the equation 53x + 51y = 7. In this case a solution might be obtained experimentally, but I am not sure how difficult it is. This is a topic of our next meeting.
October 17th, 2019
A mathematical consequence of Euclid's algorithm: for any pair [x,y] of numbers there exists their common divisor d that is divisible by all their common divisors. Algorithms working in quadratic or linear time. Euclid's algorithm operates in cubic time, i.e. in time proportional to n3.
Homework. Find historical data about Al Khwarizmi or about Gustav Lamé.
October 10th, 2019
Properties of the divisibility relation in the domain of integers. Euclidean division. Euclid's algorithm for GCD and a proof of its correctness.
Homework. Apply Euclid's algorithm to 829 931 and 715 997.
October 3rd, 2019
Primes, common divisors, prime factorization.
Homework. Find historical data about Euclid of Alexandria or about his Elements.

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.

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