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
Course contents in Fall 2024/25
- 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
Exercises
Please pay attention to the list of exercises.
Here are the same exercises in English.
Course contents in Fall 2024/25
- 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 ℵ0-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 ∀x1 . . ∀xn∃y(y≠x1 & . . & y≠xn). 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 {γ2,¬γ3} 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 HKe) 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).
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 ai pro i<k. Avšak když i je soudělné
s k, pak ai 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 267 - 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 ℤ43 platí 214 = 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(zx,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.
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 Δ0, then
Proofτ(x,w) is PA-equivalent to a Σ1-formula (that is,
is Σ1(PA)), or is Δ0 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 Δ0.
- 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Δ0.
The exponential function is formalizable, but the
sentence ∀x∃y(y=2x) is not provable
in IΔ0. It is not known whether the fact that there are infinitely many primes is
provable in IΔ0. 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
Σ1-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 Σ1-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 Σ1-soundness is replaced by mere
consistency.
- Mar 7th, 2024
- Since every RE set is m-reducible to Th(ℕ) and sets
in RE – Π1 exist, Th(ℕ)
is not Π1. 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 Σ1-sound extension of Q,
then T is undecidable (and thus) incomplete. There exist independent sentences that are
as simple as Σ1 (or Π1).
- 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 – Δ1
and φ(x) is a Σ1-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 Σ1 (or Π1, or Δ1), then
A is Σ1 (or Π1, or Δ1
respectively). The function computing the number of primes less than n is clearly recursive, but it is not
known whether its graph is Δ0.
- Feb 22th, 2024
- The graphs of the
functions [x,z] ↦ zx
and [x] ↦ NPB(x) are Δ0-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 Δ0-definable. Also the graph of the
function [x,z] ↦ zx is
Δ0-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)
- Neefektivnost rezoluce (T. Šujan, 22. a 29.10.)
- 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
- the selection
of a db server
On the local computer, TIGER, there are two parallel instances of Firebird.
One communicates through the standard port 3050, the other through port fb25 that translates
to 3060 in the services
file. The user can click on one of them in the listbox,
or say something else. Assume that, since he wants to modify users on the computer JUPITER where
Firebird communicates through port 3060, he deleted the text "TIGER" in the upper text field
and typed "JUPITER/3060" instead. In the two bottom text fields he has to specify the admin login.
In most cases, the admin would be SYSDBA. However, in Firebird 2.0 and later any user can
change his own password.
, and then
- a user action
The version of Firebird addressed as JUPITER/3060 is 2.5.2. Besides SYSDBA, there
are three other database users on that server. Since database user's first and last names are hardly ever needed,
FBUsersSetup somewhat misuses these data and codes the current time into them: JOSEPH and VIOLA
were inserted on Apr 14th, 2013. JASMIN was not inserted using FBUsersSetup and so her
first and last names are unknown. A new database user ADAM is now about to be inserted.
on that server.
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
- the database connection
Our database zoodata.fdb resides on a computer orel where
(the relevant instance of) Firebird communicates thru port 3060;
orel can be a computer in the local network or a
computer visible on internet. Of course, if it is not the local computer
on which DBUSubst is run, the browse button cannot be used; the path to zoodata.fdb
has to be typed.
When developing the database, we accessed it as a user LION.
This user is an owner of the database.
We also have another user VISITOR who is designed to have some restricted
access. Now when the database is about to be
deployed, it appears that the name LION was not wisely selected and that the
owner name should be ZOODBA. So we are about to substitute ZOODBA for LION.
ZOODBA already exists on the server in question, i.e. orel/3060.
with the NEW user's login, and then
- the login of
the dead
user
Since we were allowed to proceed to this dialog window, the login of
ZOODBA was verified against Firebird on orel/3060. It was also detected
that the version of this Firebird server is 2.5.1 and that the owner
of the database is LION, see the blue text labels in the bottom.
We are now selecting LION as the user who will be substituted by ZOODBA,
and we have to specify his password. The password of VISITOR is immaterial
for the current substitution process since VISITOR is not
a grantor of anything. However, if there were other users who
granted something to LION, further dialog windows asking about their
passwords would follow.
, i.e. the user who is to disappear.