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

Course contents in Spring 2018/19 (Czech)

21. května 2019
Znovu řády prvků v grupách. Podrobné ověření, že číslo 193 707 721 je prvočíslo. Návod k ověření, že čísla 43 a 53 jsou pro m = 2127 - 1 generátory grupy Φ(m), neboli že každé z nich má v této grupě řád m - 1. Z toho plyne, že i toto číslo m je prvočíslo.
10. května 2019 (pátek)
Řády prvků v grupě Φ(m). Cyklické grupy. Metoda pro prokázání, že velké číslo m je prvočíslo: nalézt číslo r < m, o kterém lze ověřit, že je prvkem grupy Φ(m) a má v ní řád m - 1.
7. května 2019
Praktická ukázka fungování metody RSA, při níž bylo víceméně vyřešeno cvičení 9. Mersennova prvočísla. Úlohy ve třídě NP. Jak bylo řečeno v první přednášce, nemáme dost znalostí k důkazu, že úloha Primes má polynomiální algoritmus. Budeme ale schopni dokázat (vysvětlit) slabší ale také netriviální výsledek: je to úloha ve třídě NP.
23. dubna 2019
Výpočet Eulerovy funkce pro libovolný argument. Kryptografická metoda RSA.
16. dubna 2019
Důkaz čínské zbytkové věty pomocí ekvivalentní podmínky pro nesoudělnost.
9. dubna 2019
Modulární reprezentace a čínská zbytková věta.
D. cv. Najděte modulární reprezentaci čísla 2340 vůči modulům 31 a 11.
2. dubna 2019
Pseudoprvočísla. Komutativní (čili Abelovy) grupy. Eulerova grupa Φ(m) čísla m. Důkaz Eulerovy věty pomocí komutativních grup.
D. cv. Pomocí Eulerovy věty a na základě znalosti hodnoty Eulerovy funkce pro argument 10 určete poslední desetinnou číslici čísla 7999.
26. března 2019
Umocňování ve struktuře Zm. Malá Fermatova a Eulerova věta (zatím bez důkazu). Eulerova funkce.
D. cv. Určete hodnotu Eulerovy funkce pro argumenty 21 a 25.
19. března 2019
Charakterizace invertibilních prvků v Zm pomocí Bezoutovy věty. Dva ze základních algebraických pojmů: okruh a monoid. Dokazování z axiomů okruhu. Opačné prvky.
D. cv. Uvažujte operaci ∗, která je na tříprvkové množině {0,1,2} definována takto: ab = 2 pro ab, ab = b pro a > b. Určete, zda tato operace je asociativní.
12. března 2019
Důkaz indukcí, že čtyřsloupcové rozšíření Eukleidova algoritmu je korektní. Teoretický důsledek Bezoutovy věty: když prvočíslo dělí součin dvou čísel, musí dělit i některý z činitelů. Modulární aritmetika. Invertibilní prvky ve struktuře Zm.
D. cv. Určete všechny invertibilní prvky ve struktuře Z15.
5. března 2019
Teoretický důsledek Eukleidova algoritmu: mezi společnými děliteli dvou čísel jsou takové, které jsou dělitelné všemi ostatními, což umožňuje formulovat elegantní definici největšího společného dělitele, která je nezávislá na uspořádání a která se nemusí měnit při přechodu mezi různými číselnými (nebo jinými) obory. V podobném duchu lze definovat i nesoudělnost a prvočíselnost. Eukleidův algoritmus má (čtyřsloupcové) rozšíření, které nalezne řešení Bezoutovy rovnice.
D. cv. 1(a) a 2. Další dvě cvičení 3 a 4 beru zpět: 3 bylo v hodině vlastně uděláno, 4 je plán na začátek příští hodiny.
26. února 2019
Úloha GCD (greatest common divisor, čili nalézt největšího společného dělitele dvou čísel). Eukleidův algoritmus pro tuto úlohu. Důkaz jeho korektnost a faktu, že pracuje v polynomiálním čase.
D. cv. Dopočítejte cvičení 1 a předběžně si prosím trochu prohlédněte cvičení 3.
19. února 2019
Časové nároky algoritmů, algoritmy pracující v polynomiálním čase (tj. polynomiální algoritmy). Školní algoritmus pro úlohu Násobení je polynomiální, konkrétně pracuje v kvadratickém čase. O úloze Factoring se předpokládá, že polynomiální algoritmus nemá, ale dokázáno to není. Úloha Primes má polynomiální algoritmus, ale je to obtížnější nedávný výsledek, který zůstane za obzorem kursu.

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.

Course contents in 2019/20 (Czech)

Logika dokazatelnosti (V. Švejdar, 26.11.-)
PA-tautologie a ℕ-tautologie. Logiky K a K4.
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