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

Logika: neúplnost, složitost a nutnost (Logic: Incompleteness, Complexity, and Necessity), Academia Praha, 2002. 464 pages, section 5.2 about Gödel-Dummett fuzzy logic was written by Petr Hájek. See the "Book" tab above.

Some workshop or conference presentations

Logika, Gödel, neúplnost (Logic, Gödel, Incompleteness). A talk at Friday meetings of Sysifos, February 23th, 2018. A videorecord created by Ludvík Hájek is available on YouTube.
Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and Incompleteness). A talk at Hvězdárna and planetárium Brno (Brno Observatory and Planetarium), March 9th, 2017. A videorecord created by Josef Forman is available on YouTube.
Rosser Sentences and Rosser Logics. A talk at the Prague gathering of logicians, Jan 2017.
On Purely implicational Fragments of Intuitionistic Propositional Logic. A talk at the Logica '11 International Conference, Hejnice, Czech Republic, June 2011. [pdf4]

Papers

Do We Need Recursion? In I. Sedlár and M. Blicha, eds., The Logica Yearbook 2019, pp. 193–204. College Publications, London, 2020. [pdf][talk]
Modern Czech Logic: Vopěnka and Hájek, History and Background. Journal of Applied Logics — IfCoLoG Journal of Logics and their Applications, 5(6):1261–1271, 2018. [pdf]
Předmluva: o logice 20. století (Preface: On the 20th Century Logic). In L. Dostálová, ed., Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and Incompleteness), pp. 13–53. OPS in collaboration with University of West Bohemia Publishing, Plzeň, 2015. ISBN 978-80-87269-39-8. In Czech. [pdf]
On Strong Fragments of Peano Arithmetic. In P. Arazim and M. Dančák, eds., The Logica Yearbook 2014, pp. 281–291. College Publications, London, 2015. [pdf][talk]
Výuka logiky bez logických pojmů (Teaching logic without the use of logical notions). In L. Dostálová and K. Šebela, eds., Organon VII — Nihil novi, pp. 49–57. University of West Bohemia Publishing, Plzeň, 2011. ISBN 978-80-261-0035-5. In Czech. [pdf][pdf2]
Infinite natural numbers: an unwanted phenomenon, or a useful concept? In M. Peliš and V. Punčochář, eds., The Logica Yearbook 2010, pp. 283–294. College Publications, London, 2011. [pdf][pdf2][talk]
Decision Problems of Some Intermediate Logics and Their Fragments. In M. Peliš, ed., The Logica Yearbook 2009, pp. 297–307. College Publications, London, 2010. [pdf][pdf2][talk]
Relatives of Robinson Arithmetic. In M. Peliš, ed., The Logica Yearbook 2008, pp. 253–263. College Publications, London, 2009. [pdf][pdf2][talk]
On Interpretability in the Theory of Concatenation. Notre Dame Journal of Formal Logic, 50(1):87–95, 2009. [pdf][pdf2]
Weak Theories and Essential Incompleteness. In M. Peliš, ed., The Logica Yearbook 2007, pp. 213–224. Filosofia, Praha, 2008. [pdf][pdf2][talk]
An Interpretation of Robinson Arithmetic in its Grzegorczyk's Weaker Variant. Fundamenta Informaticae, 81(1–3):347–354, 2007. [pdf][pdf2]
Gödel-Dummett Predicate Logics and Axioms of Prenexability. In O. Tomala and R. Honzík, eds., The Logica Yearbook 2006, pp. 251–260. Filosofia, Praha, 2007. [pdf][pdf2][talk]
On Modal Systems with Rosser Modalities. In M. Bílková and O. Tomala, eds., The Logica Yearbook 2005, pp. 203–214. Filosofia, Praha, 2006. [pdf][pdf2][talk]
On Sequent Calculi for Intuitionistic Propositional Logic. Comm. Math. Univ. Carolinae, 47(1):159–173, 2006. [pdf][pdf2]
With Blanka Kozlíkova, On Interplay of Quantifiers in Gödel-Dummett Fuzzy Logics. Archive for Math. Logic, 45(5):569–580, 2006. [pdf][pdf2]
Note on Inter-Expressibility of Logical Connectives in Finitely-Valued Gödel-Dummett Logics. Soft Computing, 10(7):629–630, 2006. [pdf][pdf2]
Gödlov prvi izrek o nepolnosti. Obzornik za matematiko in fyziko, 51(4):113–121, 2004.
The limit lemma in fragments of arithmetic. Comm. Math. Univ. Carolinae, 44(3):565–568, 2003. [pdf][pdf2]
A note on arithmetical completeness of theories with Rosser modalities. In K. Bendová and P. Jirků, eds., Miscellanea logica V, pp. 123–132. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
On structural proofs of Gödel First Incompleteness Theorem. In K. Bendová and P. Jirků, eds., Miscellanea logica V, pp. 115–122. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
The decision problem of provability logic with only one atom. Archive for Math. Logic, 42(8):763–768, 2003. Errata: The final paragraph, just before the list of references, contains an unpleasant misprint: 'added in January 2002', should be 'added in January 2003'. My apologies! [pdf][pdf2]
On the polynomial-space completeness of intuitionistic propositional logic. Archive for Math. Logic, 42(7):711–716, 2003. [pdf][pdf2]
With K. Bendová, On Inter-Expressibility of Logical Connectives in Gödel Fuzzy Logic. Soft Computing, 4(2):103–105, 2000. [pdf][pdf2]
On Provability Logic. Nordic Journal of Philosophical Logic, 4(2):95–116, 2000. [pdf][pdf2]
Arithmetical Classification of the Set of All Provably Recursive Functions. Comm. Math. Univ. Carolinae, 40(4):631–634, 1999. [pdf][pdf2]
Poznamka o vztahu vyplyvani v klasicke predikatove logice (A Note on the Consequence Relation in Classical Predicate Logic). In P. Jirků and V. Švejdar, eds., Miscellanea Logica II. Karolinum, Praha, 1999. In Czech.
Logika v aritmetice. In P. Jirků and V. Švejdar, eds., Miscellanea Logica I. Karolinum, Praha, 1998. In Czech.
With P. Hájek, Matematicka logika (Mathematical Logic). Praha, November 1994. Lecture notes, electronic version only, in Czech.
Some Independence Results in Interpretability Logic. Studia Logica, 50(1):29–38, 1991.
With P. Hájek, A Note on the Normal Form of Closed Formulas of Interpretability Logic. Studia Logica, 50(1):25–28, 1991.
Modal Analysis of Generalized Rosser Sentences. J. Symb. Logic, 48(4):986–999, 1983. [JSTOR]
A Sentence that is Difficult to Interpret. Comm. Math. Univ. Carolinae, 22(4):661–666, 1981.
Degrees of Interpretability. Comm. Math. Univ. Carolinae, 19(4):789–813, 1978.

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.

Course contents in Fall 2024/25

Nov 14th, 2024: A strong variant of completeness theorem for K: every sequent has a cut-free proof or a finite cycle-free counterexample. Thus the cut-elimination theorem and finite model property hold for K. One of several consequences is the following. The set of all formulas provable in K is closed under the rule LR: if □A → A is provable in K, then also A is provable. Thus adding LR to K yields no new provable formulas.
Homework. Invent a brief semantic argument (a picture and a comment in one or two lines) showing that the set of all formulas provable in K is closed under the un-necessitation rule: if □A is provable in K, then also A is provable.
Nov 7th, 2024: First of several soundness theorems: K is sound w.r.t. the class of all Kripke models, T and K4 are sound w.r.t. the class of all models whose accessibility relation is reflexive (or transitive, respectively). An algorithm (processing sequents) about which it is clear that it terminates on every input. Next week we will deduce some theorems, completeness of K included, from this algorithm.
Homework 1. Find a Kripke model K = 〈W,R,⊩〉 and a formula A such that □A → A is but A is not valid in K. Can the model K be chosen so that it is irreflexive, i.e. such that no node in it is accessible from itself?
Homework 2. Characterize (describe in words) all Kripke models in which the formula ¬□⊥ → ¬□¬□⊥ is valid. Construct a model demonstrating that □(□p → p) → □p is not provable in K4 plus ¬□⊥ → ¬□¬□⊥. Again, can the model be chosen so that it is irreflexive?
Oct 31st, 2024: Equivalent axiomatizations of GL: K4 plus L, or K plus L, or K4 plus LR, or K4 plus H. Problems to be solved: can L (or the schema 4) be proved in K plus LR? Can L (or the schema 4) be proved in K plus H? Kripke semantics of modal logic: frames, models and forcing relations (written as ⊩).
Homework 1. Consider a model having four nodes 1, 2, 3 and 4 such that the nodes 3 and 4 are accessible from 1, the node 1 is accessible from 2, and the nodes 2 and 4 are accessible from 4. The atom p is satisfied at 1 and 2. Identify the nodes at which the formula ◇□◇p is satisfied.
Homework 2. Consider a model having three nodes 1, 2 and 3 where 1 sees 2 and both 2 and 3 see 3. Let p be satisfied at 2 and 3 and refuted at 1, and let all other atoms be everywhere refuted. Prove (write down a full proof consisting of Czech or English sentences) that every modal formula A is satisfied at 2 if and only if it is satisfied at 3. Conclude that all instances of the schema 4 are satisfied at all three nodes of this model.
Oct 24th, 2024: Arithmetic semantics of modal logic: necessity is understood as provability formalized inside Peano arithmetic PA. The set ArTaut of all modal formulas that are arithmetic tautologies contains all propositional tautologies and all instances of the schemas K and 4, and is closed under MP, Nec and Löb's rule LR, which makes it possible to derive A from □A → A. Löb's axiom schema L is □(□A → A) → □A. It is equivalent to LR over K4. The official definition of GL, provability logic, is K4 plus L. The formula □⊥ → ⊥ is an example of a formula not in ArTaut. It also shows that the the logic T is not a sublogic of GL. It is not a sublogic of K4 either. These are in fact our first unprovability results.
Oct 17th, 2024: Soundness and completeness of the calculus GK. The cut-elimination theorem for it. Sequent calculus for the logic K and a verification that it simulates the Hilbert-style calculus for K.
Homework. Extend the calculus GK for the case where the equivalence connective ≡ is also considered a basic symbol. The rules should be sound with respect to the truth-value semantics, they should satisfy the subformula property and the proof of the completeness and cut-elimination theorem should go through.
Hint. One left and one right rule are needed, and both are supposed to be binary.
Oct 10th, 2024: Sequent calculus GK for classical propositional logic. The corresponding terminology: sequent, antecedent, succedent, principal, active and side formulas, initial sequents, context sensitive and context insensitive variants of binary rules.
Homework. Find a proof of the sequent 〈 A → B ⇒ ¬A ∨ B 〉.
Oct 3rd, 2024: The traditional modal logics K, T, K4, S4 and S5. Their Hilbert-style calculi. Every modal formula is T‑equivalent to ⊤, or to ⊥, or to a formula not containing the symbols ⊤ and ⊥. The formulas □□A and □A, and also the formulas ◇◇A and ◇A, are S4‑equivalent. Thus in S4 every modality followed by the same modality can be equivalently dropped. The formulas □◇□A → □□A, □A → ◇□A and ◇□A → □◇□A are provable in S5. Indeed, the first can be obtained from the symmetric form of axiom 5 using Thm K(a), the second is an instance of the symmetric form of axiom T, and the third is an instance of schema 5. A tautological consequence of the three formulas is □A → □□A. Thus S5, defined as T plus 5, is in fact an extension of S4.
Homework. (a) Fill the missing part in the proof that □ commutes with conjunction in K. (b) The schema A → □◇A is known as schema B. Prove that B and 5 are equivalent over S4.
Hint. Substitute ◇A for A in schema B. Then prove □◇◇A → □◇A using the symmetric form of 4 (which is already known to be provable in S5).

Properties of axiomatic theories

SIS ALG119006, Zoom.

Exercises

Please pay attention to the list of exercises. Here are the same exercises in English.

Course contents in Fall 2024/25

19. listopadu 2024: Eliminace kvantifikátorů je užitečná nejen jako metoda pro prokazování úplnosti teorií, ale poskytuje také informaci o množinách definovatelných ve strukturách. Δ₀ množiny (relace) jako množiny definovatelné Δ₀‑formulemi.
14. listopadu 2024: Ještě dva příklady neaxiomatizovatelných tříd: všechny silně souvislé orientované grafy a všechny dobře uspořádané množiny. Definovatelné množiny ve strukturách.
12. listopadu 2024: Struktura nestandardního modelu teorie Th(ℕ). Má-li teorie T neomezeně velké konečné modely, pak má i nekonečné modely. Z toho plyne, že je-li L libovolný jazyk, pak třída všech konečných struktur pro L není axiomatizovatelná. Z toho je dále jasné, že její komplement čili třída všech nekonečných struktur, o kterém víme, že axiomatizovatelný je, není konečně axiomatizovatelný. Löwenheimova-Skolemova věta "směrem nahoru", plná verze: má-li T v L modely, pak má i modely mohutnosti nejvýše |L| + ℵ₀; má-li navíc nekonečné modely, pak má i modely každé mohutnosti od |L| + ℵ₀ výše.
D. úkol. Cvičení 15 v seznamu nahoře.
7. listopadu 2024: Presburgerova aritmetika je teorie struktury 〈N,+,0,s〉 a z literatury je o ní známo, že umožňuje eliminaci kvantifikátorů. Axiomatizovatelné (elementární) a konečně axiomatizovatelné třídy struktur. Komplement konečně axiomatizovatelné třídy je opět konečně axiomatizovatelná třída. Teorie Th(ℕ) má i nestandardní modely.
5. listopadu 2024: Teorie DOS připouští eliminaci kvantifikátorů a je tedy úplná. Z toho plyne, že i teorie DO je úplná. Zvláštním případem konzervativního rozšíření teorie je definiční rozšíření (rozšíření o definice). Rozdíl mezi konzervativním rozšířením a rozšířením o definice ale nehraje roli v důkazech úplnosti.
31. října 2024: Rozšíření teorie a podteorie. Expanze struktury. Postačující podmínka pro to, aby rozšíření S teorie T bylo konzervativní: každý model T má expanzi, která je modelem S. Teorie DOS je konzervativním rozšířením jak teorie SUCC, tak teorie DO.
29. října 2024: Teorie SUCC umožňuje eliminaci kvantifikátorů, a je tedy úplná. Teorie DO diskétního lineárního uspořádání (discrete order). Jejím preferovaným modelem je struktura 〈N,<〉, kterou značíme ω. Operace s lineárně uspořádanými množinami: λ* je struktura získaná z λ obrácením všech šipek, λ + θ sestává z disjunktních kopií struktur λ a θ, uvnitř nichž je uspořádání zachováno beze změny, avšak navíc jsou všechny prvky v λ menší než všechny prvky v θ, a konečně λ · θ vznikne tak, že v θ nahradíme každý prvek disjunktní kopií struktury λ. Je-li λ libovolné lineární uspořádání, pak ω + (ω* + ω) · λ je model teorie DO.
24. října 2024: Podstatné kroky v důkazu, že teorie SUCC umožňuje eliminaci kvantifikátorů. Z lemmatu 2 (je-li φ konjunkce literálů, pak ∃xφ je ekvivalentní s otevřenou formulí) zbývá dořešit poslední případ, kdy každý literál ve φ obsahující x je negativní, vpravo od nerovnítka se v něm nevyskytuje x a vlevo od nerovnítka je v něm term S^(m)(x) vždy se stejným m.
22. října 2024: Teorie SUCC a DNO. Vaughtův test, jeho nikoliv nejsilnější varianta: má-li T nejvýše spočetný jazyk a je bezesporná, pak je-li navíc ℵ₀-kategorická a nemá konečné modely (dokonce stačí, že každé dva její nejvýše spočetné modely jsou spolu izomorfní), pak je úplná. Takže například DNO je úplná. Nechť γ_n pro n>0 je sentence ∀x₁ . . ∀x_n∃y(y≠x₁ & . . & y≠x_n). Pak {γ_n ; n>0 } je úplná teorie (s prázdným jazykem), což je řešení cvičení 10 a 13. Také cvičení 12 bylo na přednášce vyřešeno. Teorie {γ₂,¬γ₃} je úplná, ovšem nesplňuje podmínku, že nemá konečné modely. O teorii SUCC umíme dokázat, že není ekvivalentní s žádnou svou konečnou podteorií. Plánem do budoucna ale je dokázat, že není ekvivalentní s vůbec žádnou konečnou teorií. Přesně totéž lze říci o teorii z cvičení 10.
17. října 2024: Věta o úplnosti. Slabá verze Löwenheimovy-Skolemovy věty. Tzv. Skolemův paradox: má-li teorie množin modely, pak má i nejvýše spočetné modely (je ale jasné, že konečné modely nemá). Úplné teorie. Množiny Thm(T) a Ref(T) sentencí dokazatelných a vyvratitelných v T. Pokus o přehlednou axiomatizaci struktury 〈N,0,s〉, čili o nahrazení množiny Th(ℕ) jednodušší množinou axiomů.
15. října 2024: Korektnost pravidel kalkulu HK vůči sémantice klasické predikátové logiky. Relace důsledku. Větu o korektnosti lze pro teorie formulovat také takto: když T ⊢ φ, pak T ⊧ φ.
10. října 2024: Izomorfní a neizomorfní struktury. Ohodnocení proměnných, Tarského definice, platnost formule ve struktuře. Výroková část kalkulu HK je korektní vůči sémantice predikátové logiky s rovností v tom smyslu, že v každé struktuře každé ohodnocení splňuje každou tautologii a když ohodnocení splňuje implikaci i její premisu, splňuje i její závěr.
D. úkol. Vyřešte sémantickou část cvičení 1 (pdf soubor na webu kursu): pro formuli vzniklou obrácením nejvnějšnější implikace existuje ve všech pěti případech existuje struktura, ve které ta formule neplatí. Nebo vyřešte cvičení 9, tam možná jsou zajímavější konstrukce struktur.
8. října 2024: Věta o dedukci v predikátové logice. Sporné a bezesporné teorie. Věta o korektnosti jako základní a možná jediný nástroj pro prokazování nedokazatelnosti. Struktury. Příklady, prominentní číselné struktury.
3. října 2024: Doprohlédnutí hilbertovského kalkulu HK (či HK_e) pro klasickou predikátovou logiku s rovností: axiomy rovnosti, pravidla generalizace.
D. úkol. S využitím tautologických důsledků a případně neformálních důkazů zdůvodněte dokazatelnost sentencí ∀x(P(x) → Q(x)) → (∃xP(x) → ∃xQ(x), ∃x∀yR(x,y) → ∀y∃xR(x,y) a ∃x(P(x) → ∀yP(y)).
Návod. Začněte s tautologií ¬P(z) → (P(z) → ∀yP(y)) a s instancí axiomu specifikace, která má v premise závěr této implikace. Méně názorný ale o dost kratší důkaz lze také založit na tom, že pravidlo generalizace aplikujete na formuli ¬∃x(P(x) → ∀yP(y)) → P(y).
1. října 2024: Přehled logické syntaxe: od termů k axiomatickým teoriím. Jednoduchá teorie s axiomy Q1 a Q2. Logické axiomy. Použití tautologií a tautologických důsledků v predikátové logice, neformální důkazy.

Arithmetics and algorithms

Exercises (updated May 19, 2024).

SIS ALG110008, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení cvičení 8 a dalších libovolně zvolených třinácti cvičení (i s vysvětlením matematického či algoritmického pozadí). Zkouška pak pokračuje prodiskutováním některého důkazu. Kromě termínů vypsaných v SISu se lze domluvit i na jinou dobu, ale ve středu obvykle mohu až tak od 17h, a v pátek pouze ráno a pouze možná. Všechny termíny lze využívat i jako konzultace.

Course contents in Spring 2023/24 (Czech)

14. května 2024: Chybějící část důkazu z minulé přednášky: když m je prvočíslo a a∈Φ(m) má řád k, pak každý prvek b řádu k se rovná některému aⁱ pro i<k. Avšak když i je soudělné s k, pak aⁱ nemá řád k. Takže počet prvků řádu k je nejvýše φ(k).
7. května 2024: Několik poznatků, které se skládají na tvrzení, že když m je prvočíslo a k je dělitel čísla m - 1, pak v grupě Φ(m) je přesně φ(k) prvků řádu k. Toto bylo téměř ale ne zcela dokončeno. Dokončení a vysvětlení, jak na základě těchto úvah definovat certifikát pro prvočíslo, je (kromě konzultace na jakékoliv téma), plánem na Út 14.5.
25. dubna 2024: Mersennova čísla a Mersennova prvočísla. Výsledek Franka Colea z roku 1903, že jedním z dělitelů čísla 2⁶⁷ - 1 je 193 707 721, umožňuje neformálně vysvětlit, co je třída NP. Úloha U je ve třídě NP, jestliže pro ni lze definovat krátká data (certifikát), která když jsou pro daný vstup x předložena, lze z nich a z x polynomiálním algoritmem potvrdit, že x ∈ U. Jinými slovy, úlohy ve třídě NP jsou úlohy s efektivní verifikovatelností pozitivních instancí. Certifikát pro složené číslo větší než 2 je přirozené definovat jako (některý) dělitel onoho čísla. Takže množina všech složených čísel větších než 2 je úlohou ve třídě NP. Třída P všech polynomiálně rozhodnutelných úloh je podtřídou třídy NP. Řády prvků v grupách. Řád libovolného prvku grupy Φ(m) musí být dělitelem čísla φ(m). Úvahy o řádech směřují k výsledku, že i množina všech prvočísel je úlohou ve třídě NP. Což je (na rozdíl od celkem nedávného silnějšího výsledku, že množina všech prvočísel je dokonce úlohou ve třídě P) fakt na školní úrovni celkem dosažitelný.
23. dubna 2024: Výpočet čísla φ(m) na základě seznamu prvočísel v prvočíselném rozkladu čísla m. Šifrovací metoda RSA. K jejímu prolomení by stačil polynomiální algoritmus pro nalezení prvočíselného rozkladu. Stačil by i algoritmus pro výpočet funkce φ, ale ani jeden z takovýchto algoritmů není znám (protože pravděpodobně neexistuje).
16. dubna 2024: Důkaz čínské zbytkové věty. Počítání s modulárními reprezentacemi. Pseudoprvočísla.
Cvičení. Ověřte pomocí počítání s modulárními reprezentacemi, že 567 je pseudoprvočíslo. Číslo 641, které pravděpodobně bylo zmíněno v přednášce, pseudoprvočíslem není (protože je to prvočíslo). Ale s užitím faktu, že v ℤ₄₃ platí 2¹⁴ = 1, by šlo ověřit, že 645 je pseudoprvočíslo.
9. dubna 2024: Nejen určování invertibility v ℤ_m a výpočet inverzního prvku jsou polynomiálně počitatelné. Také pro umocňování, tj. pro výpočet funkce [m,x,z] ↦ Mod(z^x,m) existuje polynomiální algoritmus. Eulerova grupa a Eulerova funkce. Eulerova věta: pro libovolné m a libovolné x∈Φ(m) platí x^φ(m) = 1. V tomto tvaru ji budeme potřebovat, ale přehlednější důkaz má trochu obecnější verze: v komutativní grupě s n prvky umocnění libovolného prvku na n-tou dá jedničku čili neutrální prvek té grupy. Modulární reprezentace.
2. dubna 2024: Dva důsledky Bézoutovy věty, tj. dvě tvrzení dokazatelná v teorii, jejímiž axiomy jsou Bézoutova věta a axiomy obory integrity: ekvivalentní podmínka pro nesoudělnost a fakt, že každé ireducibilní číslo je prvočíslem. To druhé je domácí úkol kontrolovaný (až) u zkoušky. Eukleidův algoritmus lze užít k rozhodnování o invertibilitě v ℤ_m. Jeho čtyřsloupcovou variantu lze užít k výpočtu inverzního prvku. Když m je prvočíslo, pak ℤ_m je těleso. Není-li m prvočíslo, pak ℤ_m není ani obor integrity.
26. března 2024: V libovolném oboru integrity platí, že každé prvočíslo je ireducibilní. Rozšířený (čtyřsloupcový) Eukleidův algoritmus. Z něj (z jeho analýzy) plyne Bézoutova věta pro strukturu celých čísel: ke každé dvojici a a b existuje dvojice x a y taková, že ax + by je společným dělitelem (je jasné, že největším společným dělitelem) čísel a a b.
19. března 2024: ℤ a ℚ[x] jako příklady oborů integrity. Také každé těleso je oborem integrity. Nenulovým prvkem lze v oboru integrity krátit. Dělitelnost v oborech integrity: asociované prvky, dělitelé jedničky, nesoudělnost, největší společný dělitel. Prvky x a y jsou spolu asociované, právě když x ∣ y a y ∣ x.
12. března 2024: Definice okruhu a příklady: ℚ, ℤ, ℤ_m a ℚ[x]. Invertibilní prvky komutativního monoidu tvoří pod-monoid, který je grupou. V případě (multiplikativní části) okruhu ℤ_m se tato grupa nazývá Eulerovou grupou čísla m a značí se Φ(m). Například nosná množina grupy Φ(15) je {1,2,4,7,8,11,13,14}.
5. března 2024: Eukleidův algoritmus pracuje v polynomiálním čase. Monoidy a inverzní a invertibilní prvky v nich.
Cvičení. Je-li na množině {0,. .,14} operace ∗ definována předpisem x∗y = Mod(xy,15), které prvky jsou invertibilní? Uvažujte (nekomutativní) monoid všech funkcí z tříprvkové množiny {a,b,c} do sebe. Je funkce {[a,a],[b,a],[c,b]} invertibilní? Je {[a,c],[b,a],[c,b]} invertibilní?
27. února 2024: Vlastnosti relací obecně, vlastnosti relace dělitelnosti. Na ∀x(x ∣ 0) a ∀x∀y∀z(x ∣ y → (x ∣ y+z ≡ x ∣ z)) lze založit ověření, že Eukleidův algoritmus správně počítá úlohu GCD, tj. že k libovolným dvěma číslům nalezne jejich největšího společného dělitele. Ale lze uvažovat i opačným směrem a z korektnosti Eukleidova algoritmu odvodit čistě matematický poznatek: ke každým dvěma číslům existuje jejich společný dělitel, který je dělitelný všemi jejich (ostatními) společnými děliteli.
20. února 2024: Úloha a algoritmus jako základní pojmy teoretické informatiky. Časové nároky algoritmů. Školní algoritmus pro úlohu Mult pracuje v kvadratickém čase, školní algoritmus pro sčítání dokonce v lineárním čase. Pro algoritmy, které pracují v linárním, kvadratickém, kubickém atd. čase máme souhrnný název polynomiální algoritmy. Úlohou, pro kterou polynomiální algoritmus neexistuje, je pravděpodobně Factoring, čili úloha nalézt prvočíselný rozklad daného čísla. Ale dokázané to není, nalezení důkazu je otevřeným problémem. Dva algoritmy, který bychom dostali modifikací těch algoritmů pro úlohu Primes, které byly uvedeny v přednášce, pracují v exponenciálním čase, takže polynomiální rozhodně nejsou.

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 (updated May 2nd, 2024) list of exercises.

SIS ALG119007, Zoom.

Exams (Czech)

Please be ready to discuss any of the 14 exercises. However, the exam requirements end with the proof of Löb's theorem. Further consultation and exam days (other than given in SIS) are possible.

Course contents in Spring 2023/24

May 16th, 2024: Solovay's completeness theorem for GL: a modal formula A is provable in GL if and only if it is a PA-tautology. We did not discuss the completeness of another logic, sometimes denoted by GLS. It is complete with respect to ℕ-tautologies, and the proof is very similar and is also contained in Solovay's paper.
May 14th, 2024: Soundness of GL w.r.t. Kripke semantics (finished). The proofs of completeness and of finite model property are skipped. However, they have a clear consequence: GL is decidable. A plan for the next talk is Solovay's arithmetic completeness proof: a finite Kripke counterexample for a modal formula A can be converted to an arithmetic counterexample, i.e. to an arithmetic valuation ∗ such that PA ⊬ A^∗.
May 7th, 2024: Two variants of the substitution theorem are provable in K4. An application of GL in metamathematics: a solution of a Gödelian self-reference equation (like Gödel's, Henkin's or Löb's sentence) is uniquely determined. A sentence is obtained by Gödelian self-reference if the claim it says about itself can be expressed using the formula Pr_π(x), which can be nested, parameters, and nothing else. However, a general unique solvability theorem is not true. This is clear from some exercises. Kripke semantics for GL: it is sound w.r.t. the class of all transitive and reversely well-founded frames (to be finished). Some connections of reverse well-foundedness and irreflexivity: a well-founded frame is irreflexive, and a finite transitive and irreflexive frame is reversely well-founded.
May 5th, 2024: Logic GL can be defined by two equivalent ways, as the extension of K4 by Löb's rule, or the extension of K4 by Löb's axiom scheme. The latter is preferable in the literature.
May 2nd, 2024: An alternative proof of Löb's theorem. Modal formulas, PA-tautologies and ℕ-tautologies. Modal logics K and K4. Löb's rule and Löb's axiom scheme.
Apr 25th, 2024: As we know, if T and τ(z) are as usual, then (T+Con(τ)) can prove the unprovability of the sentence Con(τ). However, (T+Con(τ)) cannot prove the independence of the sentence Con(τ). This is an example on the situation where Gödel's second theorem works as a technical tool used in some proof. Henkin's question concerning a self-referential sentence asserting its own provability. Löb's solution: all such sentences are provable.
Apr 23rd, 2024: Some connections to Gödel's second theorem. First, Paris and Harrington and some other authors exhibited sentences that are independent of PA and speak about numbers, not about formalized logic. There is a link from these results to Gentzen who considered the question what arithmetic axioms, if added to PA, make it possible to prove the consistency of PA. Second, reasoning about self-referential sentences can be simulated in modal logic, and modal logic even has some applications in that reasoning. And third, most philosophers agree that Gödel's result in fact refutes Hilbert's program, but the opposite opinion and further considerations are still possible. While PA cannot prove its own consistency, some consistency proofs in PA are possible. For example, PA ⊢ Con(∅).
Apr 18th, 2024: Gödel's second incompleteness theorem. It is often cited as follows: no sufficiently strong recursively axiomatized theory can prove its own consistency. More exactly, if τ(z) is Σ and defines T (in which case T must be recursively axiomatizable), and T is consistent, then T ⊬ Con(τ). In particular, PA ⊬ Con(π) where π is the natural definition of PA in ℕ.
Apr 16th, 2024: The self-reference theorem. Formalized Σ-completeness theorem. Gödel's self-referential sentence asserting its own unprovability.
Apr 11th, 2024: The formulas Pr_τ(x) and Con(τ). Facts about formalized provability and formalized consistency provable in PA. Löb's derivability conditions.
Apr 9th, 2024: Formulas describing further syntactic notions. They can be used to write down a formula Proof_τ(x,w) containing a formula τ(z) as a subformula. If τ(z) is Σ or Δ₀, then Proof_τ(x,w) is PA-equivalent to a Σ₁-formula (that is, is Σ₁(PA)), or is Δ₀ respectively. If τ(z) defines T, then Proof_τ(x,w) defines the set of all pairs [φ,m] such that m is a proof of φ in T.
Apr 4th, 2024: String functions in PA. Formulas Var(v) and Term(t). They express the property "the number v is a variable" and "the number t is a term", respectively, in the arithmetic language. Writing down the former is straightforward (using Euclidean division and the exponential function), but defining terms involves speaking about balanced strings and quasiterms. Both formulas are Δ₀.
Apr 2nd, 2024: Formalization in arithmetic (arithmetization) of a notion involves finding a formula that defines the notion in ℕ and proving in PA that the notion, if described by that formula, has the expected properties. Notions formalizable in PA include primes (irreducibles), powers of two, Euclidean division and the function NPB. Most of these notion are formalizable already in IΔ₀. The exponential function is formalizable, but the sentence ∀x∃y(y=2^x) is not provable in IΔ₀. It is not known whether the fact that there are infinitely many primes is provable in IΔ₀. If two formulas define the same set in ℕ, then they are (of course) Th(ℕ)-equivalent, but they may be PA-inequivalent.
Mar 26th, 2024: Euclidean division in PA. The claim that there are infinitely many irreducible numbers (before we prove that being irreducible is the same as being prime, we distinguish between the two notions) is expressible in the arithmetic language. In fact the classical (Euclid's) proof is formalizable in PA, but is seems adequate to avoid speaking about the factorial function and about the prime factorization of a number. The fact that every nonzero number is the product of some irreducible numbers is objectionable since it is an infinite disjunction and thus it is problematic to consider it a sentence.
Mar 21st, 2024: The relationship between the schemas LNP and Ind. A model showing that they are not equivalent over Q.
Mar 19th, 2024: Peano arithmetic PA and provability in it: both operations are commutative and associative, · is distributive over +, both cancellation rules hold, the strict order is transitive, irreflexive and linear, the unstrict order relates to the strict order as expected, and also the interaction of the order relations and the operations is as expected.
Homework. Using the fact that a consistent decidable theory has a complete decidable extension show that a theory T is essentially undecidable (in the sense that every consistent extension of T is undecidable) if and only if T is essentially incomplete (in the sense that every recursively axiomatizable extension of T is incomplete).
Mar 14th, 2024: A finally finished full proof of Rosser's theorem: if T is any consistent recursively axiomatizable extension of Q, then T is incomplete (if fact, already some Σ₁-sentences are independent) and undecidable (more than that, Thm(T) and Ref(T) are recursively inseparable RE sets).
Mar 12th, 2024: An addendum to Gödel's 1st theorem: if T satisfies the assumptions, then Thm(T) is Σ₁-complete (in the sense that every RE set is m-reducible to it). So it is one of the algorithmically most complicated RE sets. A finite extension of a decidable theory must again be decidable. From this it follows that the set of all logically valid arithmetic formulas is not decidable. Thus predicate logic is not decidable in general. However, there are some special cases that are decidable. For example, if the language consists of only finitely many unary predicate symbols. Rosser's theorem (to be finished or repeated): the claim of Gödel's 1st theorem remains true if Σ₁-soundness is replaced by mere consistency.
Mar 7th, 2024: Since every RE set is m-reducible to Th(ℕ) and sets in RE – Π₁ exist, Th(ℕ) is not Π₁. Since the arithmetic hierarchy does not collapse (sets in Σ_n – Π_n exist for every nonzero n), this argument can be repeated at every level n≠0: Th(ℕ) is not Π_n. The whole fact is cited as Tarski's theorem on the undefinability of truth: arithmetic truth (the set of all formulas valid in ℕ) is not arithmetical (is not in the union of all Π_n, which equals the union of all Σ_n; or put otherwise, no formula defines it in ℕ). Gödel's 1st incompleteness theorem: if T is a Σ₁-sound extension of Q, then T is undecidable (and thus) incomplete. There exist independent sentences that are as simple as Σ₁ (or Π₁).
Mar 5th, 2024: We know that if T is recursively axiomatizable, then Thm(T) is RE. Craig's theorem (known as Craig's trick) says that the opposite is also true: if Thm(T) is RE, then there exists a recursive is S equivalent to T. If is T is recursively axiomatizable and complete, then it is decidable. Therefore, SUCC, DNO and other theories from the Fall semester are decidable. All their models (like ω + (ω* + ω) · ω) are decidable structures. Any finite structure for a finite language is decidable. If A ∈ RE – Δ₁ and φ(x) is a Σ₁-formula that defines it, then the equivalence ∀n(n∈A ⇔ φ(\bar{n})∈Th(ℕ)) shows that A ≤_m Th(ℕ). Thus ℕ is an undecidable structure.
Feb 29th, 2024: Course-of-values recursion and some examples on its use. (i) Hofstadter's function is recursive. (ii) For every recursive function g of one variable such that Rng(g) is infinite there exists a one-to-one recursive function f having the same range. This fact is a key step in proving a characterization of RE subsets of N: a set A ⊆ N is RE if and only if it is finite or it is the range of some one-to-one recursive function. (iii) The set of all terms (in the arithmetic language) is recursive. From this it is possible to continue to other syntactic notions (formulas, free and bound variables etc.) and conclude that if T is recursive or RE, then the binary relation "d is a proof of φ in T" is recursive or RE respectively.
Feb 27th, 2024: A set A ⊆ N is m-reducible to a set B ⊆ N, which we denote by A ≤_m B, if there exists a recursive function f such that ∀n(n∈A ⇔ f(n)∈B). If A ≤_m B and B is Σ₁ (or Π₁, or Δ₁), then A is Σ₁ (or Π₁, or Δ₁ respectively). The function computing the number of primes less than n is clearly recursive, but it is not known whether its graph is Δ₀.
Feb 22th, 2024: The graphs of the functions [x,z] ↦ z^x and [x] ↦ NPB(x) are Δ₀-definable. A function derived from a (partial) recursive function via primitive recursion must again be (partial) recursive.
Feb 20th, 2024: The graph of the functions Div and Mod are Δ₀-definable. Also the graph of the function [x,z] ↦ z^x is Δ₀-definable (to be finished).

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) in the academic year 2024-25. SIS: ALG500003.

Course contents in 2024/25 (Czech)

Eliminovatelnost řezů v klasické predikátové logice (M. Georgiu, od 12.11.): Regulární formule a sekventy, regulární důkazy. Lemma o redukci: důkaz, jehož posledním krokem je řez na formuli θ a v němž všechny ostatní řezové formule mají hloubku menší než θ, lze přepracovat na důkaz téhož sekventu, který má nižší rank než původní důkaz.
Neefektivnost rezoluce (T. Šujan, 22.10. až 5.11., tři přednášky): Rezoluční kalkulus. Efektivní a neefektivní výrokové kalkuly.
Dobrá uspořádání v teoretické informatice (L. Clowez, 15. a 22.10.): Na množině všech konečných multimnožin sestavených z prvků fundovaně uspořádané množiny lze přirozeným způsobem definovat uspořádání a dokázat o něm, že je také fundované. To pak lze v některých případech použít k důkazu, že určitý algoritmus se dopočítá na každém vstupu. McCarthyho 91-funkce.
Úvod (V. Švejdar, 8.10.): Upřesnění programu pro zimní semestr. Timotej, Martin Georgiu a Jiří připravují nebo již mají připraveny přednášky. Plány nad to existují ale moc určité zatím nejsou. Krátký výklad o univerzálních relacích pro určitou třídu množin jako pokus o úvod (začátek úvodu) do zamýšlených přednášek Timoteje nebo Martina Putzera o rekurzívních funkcích.

Interpretation of Gödel incompleteness theorems

About

A seminar based on students' presentations, devoted to reading papers mainly by Smorynski and Detlefsen. Here is a course announcement. SIS: ALGV19006.

Course contents in 2023/24

Smorynského článek Hilbert's Programme (Adam Fürstenzeller, od 14.12., 2 přednášky): Abstrakt (poskytnutý přednášejícím): Smoryńského článek popisuje situaci, ve které se matematika jako vědecká disciplína ocitla na začátku dvacátého století. Mezi matematiky se vedly diskuse týkající se formulování samotných základů této vědní disciplíny. Jednou z teorií byl intuicionismus, za jehož zakladatele se považuje L. E. J. Brouwer, který ve své disertaci (1907) zformuloval základní myšlenky tohoto směru. Intuicionisté odmítali aktuální nekonečno a využívání aristotelské logiky, zejména zákonu vyloučení třetího, pro nekonečné objekty. Dalším rozšířeným směrem byl formalismus v čele s Davidem Hilbertem. Hlavní myšlenkou formalismu je budování bezesporných axiomatických teorií — sad axiomů, které úplně popisují danou matematickou teorii (věty a axiomy jsou pravdivé, když nejsou ve sporu se svými důsledky — nemusí se nutně jednat o “evidentní” pravdy).
Názorová rozepře mezi Hilbertem a Brouwerem je ústředním tématem celého článku. Smoryński důkladně popisuje jak osobní vztah hlavních dvou protagonistů, tak i ohlasy, které jejich práce vyvolaly. Počátkem dvacátých let získává Brouwer nové stoupence. Jedním z nich byl také H. Weyl, jehož přednáška z roku 1920 přiměla Hilberta znovu se plně věnovat práci v oblasti základů matematiky. Společně se svými stoupenci se snaží dokázat bezespornost aritmetiky (v širším smyslu, zahrnujícím i analýzu a teorii množin) — tzv. Hilbertův program. Ideový spor mezi Hilbertem a Brouwerem se postupně přesouvá i do osobní roviny. Jeho vrcholem je vyloučení Brouwera z Matematische Annalen, které inicioval Hilbert.
V průběhu dvacátých let 20. století předkládá Hilbert rozpracované důkazy Ackermanna a Von Neumanna a zdá se, že důkaz bezespornosti aritmetiky a s ním i dokončení Hilbertova programu je na dosah ruky. Zvrat však přináší rok 1931 a Gödelovy věty o neúplnosti. V první z nich Gödel dokázal, že každá bezesporná rekurzivně axiomatizovatelná teorie obsahující aritmetiku je neúplná (existuje v ní nezávislé tvrzení) a tím prokázal neuskutečnitelnost Hilbertova programu.
Eckart Menzler-Trott: Logic's Lost Genius — The Life of Gerhard Gentzen (Timea Cochová, od 30.11., 2 přednášky): Zaoberali sme sa životným príbehom matematika a logika Dr. habil. Gerharda Gentzena. Od detstva, cez štúdium a prácu až po jeho tragickú smrť v Prahe. Nahliadli sme k jeho práci a komunikácii s matematikmi vtedajšej doby, ako boli napríklad Hilbert a Bernays. Z oficiálnych dokumentov, spovedí blízkych, pracovných a osobných listov sa dozvedáme o jeho charaktere a sledovali sme rozvoj jeho nápadov a práce. Taktiež sme si priblížili ako vyzerala veda a hlavne matematika a logika v nacistickom Nemecku a v zvyšku sveta.
Ukážky niektorých listov a dokumentov: PDF1, PDF2.
L. E. J. Brouwer: Life, Art and Mysticism (Šimon Pošta, 23.11., 1 přednáška): Brouwerův výchozí bod Smutného světa, role člověka jako individua a jako člena kolektivu, zásadnost karmického řádu a jeho prohlédnutí skrze přivrácení se k sobě, druhy řečí, pravd a jejich vztah k vědám, speciálně k logice a matematice. K tomu podrobnější shrnutí.
Detlefsenův článek z roku 79 (Timotej Šujan, od 2.11, 1.5 přednášky): Abstrakt (poskytnutý přednášejícím): Detlefsen v první části článku kritizuje takovou skeptickou interpretaci (SI) Gödelovy druhé věty (G2), která by se snažila dojít ke skeptickému závěru, že víru v konzistenci teorie T nelze odůvodnit důkazem sentence Con(T). Tvrdí, že tento závěr z G2 žádným zřejmým způsobem neplyne, a tedy je potřeba dokázat určité pomocné předpoklady SUP1 a SUP2. Následně se snaží ukázat, že platnost SUP1 vyvrací původní SI — v jeho argumentu jsou ústřední pojmy jako reflexivní teorie či (jeho vlastní pojem) epistemicky kompaktní teorie. V druhé části článku se snaží upravit SI tak, aby unikla ze spárů jeho kritiky, avšak následně i takovou upravenou SI odmítá jako nepodloženou. V třetí části krátce odmítá jako nepodloženou Resnikovu interpretaci G2 v kontextu “nejsilnějšího/nejsložitějšího systému, který jsme ještě ochotní vážně zkoumat”, a to i kvůli nejasnému popisu takového systému. V závěrečné části se pak snaží zachránit Hilbertův program tak, že představuje tzv. omezené ω-pravidlo, které je dle něj v souladu s finitními metodami, které Hilbertův program vyžaduje, a tvrdí, že např. Con(PA) je dokazatelné z PA+(ω-pravidlo).
Gödelův článek z roku 1931 (L. Clowez, od 19.10., 2.5 přednášky): Kódování logické syntaxe, které je založeno na prvočíselných rozkladech přirozených čísel. Definice kalkulu poměrně podobná dnešní definici kalkulu hilbertovského. Gödel pracuje s axiomatickou teorií, která odráží takzvanou teorii typů. Viditelný rozdíl vůči dnešním přístupům je to, že nepracuje s nějakým předem fixovaným jazykem. Pouze trvá na tom, že k dispozici jsou symboly pro nulu a následnickou funkci. Článek pracuje s “rekurzívními” funkcemi, ale definici se shoduje s tím, čemu se dnes říká primitivně rekurzívní funkce (dnes víme, že rekurzívní funkce lze ztotožnit s funkcemi algoritmicky počitatelnými a je jich víc než primitivně rekurzívních). Jako celkem věrohodná tedy vypadá historická hypotéza, že kromě vět o neúplnosti je článek důležitý také tím, že v něm byly zavedeny primitivně rekurzívní funkce.
Dnešní pohled na Gödelovy věty (V. Švejdar, 2 týdny): Trochu životopisných údajů ke Gödelovi. Ingredience důkazu jeho vět o neúplnosti: kódování syntaxe, numerály, definovatelné množiny, Σ-formule a věta o Σ-úplnosti, predikát dokazatelnosti, věta o autoreferenci.

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

Vítězslav Švejdar

Introduction

About me

Research interests

Experience and education

Office info, events, miscellaneous updates

Publications

BibTeX file

Book

Some workshop or conference presentations

Papers

Logic: Incompleteness, Complexity, and Necessity (Academia, 2002)

Modal and non-classical logics

SIS ALG119008.

Course contents in Fall 2024/25

Properties of axiomatic theories

SIS ALG119006, Zoom.

Exercises

Course contents in Fall 2024/25

Arithmetics and algorithms

SIS ALG110008, Zoom.

Exams (Czech)

Course contents in Spring 2023/24 (Czech)

Huge number calculator

Incompleteness and Gödel Theorems

SIS ALG119007, Zoom.

Exams (Czech)

Course contents in Spring 2023/24

Chapters in Classical Logic

About

Course contents in 2024/25 (Czech)

Interpretation of Gödel incompleteness theorems

About

Course contents in 2023/24

Other activities

FBUsersSetup

DBUSubst