V.Š. V.Š.

Introduction

About me

Associate professor at the Department of Logic, College of Arts ("Faculty of Arts"), Charles University in PragueFilozofická fakulta UK, Palachovo nám. 2, 11638 Praha 1. Courses Computability (an introduction to recursive functions), Classical Logic II (with an emphasis on incompleteness and undecidability), and some others related to metamathematics or to algorithms.

Research interests

Interpretability of axiomatic theories, arithmetization, related modal logics, algorithmic aspects of non-classical logics.

Experience and education

During 1982-90 worked as a software developer for an industrial company ČKD Polovodiče. Participation in writing a control system for PDP-11 computers. The system was designed by Jan Pavelka*)Accidentally the same Jan Pavelka who, a few years before turning into a respected software developer, wrote innovative papers about fuzzy logics., and was successfully applied in several branches of industry like steel rolling or international transport of natural gas.

Ph.D. in mathematical logic, Ph.D. study in the Institute of Mathematics of the Academy of Sciences of the Czech Republic. Dissertation Self-Reference and Modal Logic, 1982, supervisor Petr Hájek. Graduated in mathematics from Charles University, 1978, master's thesis Degrees of Interpretability.

Office info, events, miscellaneous updates

Office hours Thu 15:00, or by appointment. For more info please see the image above, or the web of the department.

Nabídka témat bakalářských a diplomových prací: TemataPraci13.pdf

Publications

BibTeX file

BibTeX entries can be taken from sv.bib. Note that the file contains a preamble with some strings and macros.

Book

Some workshop or conference presentations

Papers

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

I do not think logic is a field where people are taught how to think logically. Instead, I consider it a theory about deductive thinking for people who already are able to think logically, usually because they have some experience with academic mathematics.

My ambition was to have more than a list of definitions, theorems, and proofs; I am trying to include comments and explanations, and I believe that the reader should be led from some questions to some solutions.

I am grateful to Petr Hájek, who was my teacher and who gave one of the initial impulses for writing this book. He actually wrote only a small part of the text, but much larger part and perhaps everything was inspired by him.

As a result of an agreement with the Academia publishing company, a pdf version of the book is now available (full text!) for study purposes (only!). When downloading the file, it is recommended to download also Errata and save both files to the same folder on local computer. That will activate the links in the text marked by big red 'E'. Redistribution and modifications of the file are not allowed! Printing of (any part of) the document is not allowed!

Po domluvě s nakladatelstvím Academia je nyní plný text knihy ve formátu pdf přístupný pro studium (pouze!). Při kopírování souboru na lokální počítač je doporučeno stáhnout také Errata a umístit oba soubory do téže složky. Soubor nesmí být dále šířen ani nesmí být modifikován! Žádná jeho část nesmí být tištěna!

Click on the blue word 'Academia' on the first page of the book to obtain further information about their bookstores and other books they publish.

Comments and additions to Errata are welcome.

Modal and non-classical logics

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

Course contents in Fall 2020/21 (Czech)

22. října 2020
Schéma K a hilbertovský kalkulus pro logiku K. Věta o korektnosti této logiky vůči kripkovské sémantice.
Cvičení. S využitím tautologií a tautologických důsledků zdůvodněte, že všechny instance schématu A & □A → □(A & B) jsou v hilbertovském kalkulu pro logiku K dokazatelné. Formule p → □□p ale dokazatelná není.
15. října 2020
Ještě kripkovská sémantika.
Cvičení. Uvažujte rámec 〈W,R〉, kde W = {a,b,c} a R = {[a,b],[b,c],[c,c]}. Takže a vidí pouze b, kdežto b a c vidí c a nic jiného. Atom p je splněn v b a v c, ale ne v a, ostatní atomy jsou všude nesplněny. Dokažte, že b a c nelze odlišit žádnou modální formulí, tj. že každá modální formule, která je splněna v b, je splněna i v c.
8. října 2020
Věta o kompaktnosti v klasické výrokové logice. Kripkovské rámce a kripkovské modely pro modální výrokovou logiku.
Domácí cvičení. Uvažujte rámec se čtyřmi vrcholy 1, 2, 3 a 4, v němž z 1 jsou dosažitelné vrcholy 3 a 4, z 2 je dosažitelný 1, z 4 jsou dosažitelné 4 a 2. Atom p je splněn ve vrcholech 1 a 2. Ve kterých vrcholech je splněna formule ◇□◇p?
1. října 2020
Opakování klasické výrokové logiky: logické spojky, tautologie, ekvivalentní formule, důsledek.
Domácí cvičení. Promyslete následující variantu Příkladu 1.1.7 v knize [Šv02]. Nechť množina Γ výrokových formulí je definována jako { pipi+1 ; i ∈ N }. Které z formulí tvaru pipj jsou logickým důsledkem (vyplývají) z množiny Γ? Je pravda, že ta, která vyplývá, vyplývá i z některé konečné podmnožiny množiny Γ? Z které?

Properties of axiomatic theories

SIS ALG119006, Zoom Tue, Zoom Thu.

Course contents in Fall 2020/21 (Czech)

22. října 2020
Věta o silné úplnosti, věta o kompaktnosti a dvě verze Löwenheimovy-Skolemovy věty. Souvislosti mezi nimi.
Cvičení. Pro každou ze struktur 〈N,<〉, 〈Z,<〉 〈Q,<〉 (přirozená, celá resp. racionální čísla s ostrým uspořádáním) nalezněte sentenci, která v ní platí, ale neplatí v ostatních dvou.
20. října 2020
Souvislosti mezi větou o korektnosti (jejím důkazem), definicí vyplývání a logicky platnými formulemi. Sporné a bezesporné teorie.
Cvičení. Uvažujte teorii s prázdným jazykem a prázdnou množinou axiomů. Popište všechny její modely. Najděte příklady sentencí, které platí jen v některých z nich.
15. října 2020
Teorie struktury, logicky platné formule, model teorie.
Cvičení. Fragment teorie množin z minulé hodiny (to cvičení 21) je pořád aktuální. Dále cvičení 2 na straně 156, ale většinu jsme již vyřešili. Je některá z formulí x(P(x) → ∀yP(y)) a x(P(x) → ∀yP(y)) logicky platná?
13. října 2020
Tarského definice, platnost formule ve struktuře, logicky platné formule. Věta o korektnosti: každá formule dokazatelná z množiny předpokladů platí v každé struktuře, v níž platí všechny předpoklady.
Cvičení. Domácí úkol se sentencemi (iv) a (v) z minulého týdne je pořád aktuální. Řešitelné je také cvičení 21 na straně 182 knihy [Šv02].
8. října 2020
Hilbertovský kalkulus. Syntaktické pojmy: důkaz, modus ponens, pravidla generalizace, výrokové axiomy, axiomy specifikace, axiomy rovnosti, věta o dedukci.
Domácí cvičení. Připomeňte si větu o korektnosti a pokuste se ji použít ke zdůvodnění, že sentence (iv) x(S(x)≠x) a (v) x(x=0 ∨ ∃y(x=S(y))) nejsou dokazatelné v teorii s axiomy Q1 a Q2.
6. října 2020
Formální a neformální důkazy (tří sentencí z minulé hodiny). Užití (výrokových) tautologií a tautologického důsledku při konstrukci důkazů v hilbertovském kalkulu pro klasickou predikátovou logiku s rovností. Ručně psanými poznámkami se moc chlubit nemohu (prosím nešířit), ale třeba trochu pomohou.
Domácí cvičení. (a) Podejte příklad termu, který je substituovatelný za nějakou proměnnou v nějaké formuli, a jiného termu, který substituovatelný není (třeba za tutéž proměnnou v téže formuli). (b) Nalezněte důkaz (neformální nebo i formální) sentence x(P(F(x)) ∨ ¬P(x)) v teorii, která má prázdnou množinu axiomů, unární predikát P a unární funkční symbol F.
1. října 2020
Formule klasické predikátové logiky s rovností.
Domácí cvičení. Uvažujte teorii s jazykem {0,S} a s axiomy xy(S(x)=S(y) → x=y)x(S(x)≠0). Nalezněte neformální důkazy následujících sentencí: (i) S(0)≠0, (ii) S(S(0))≠S(0), (iii) xy(S(y)≠x).

Arithmetics and algorithms

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

SIS ALG110008

Exams (Czech)

Ke zkoušce si prosím připravte seznam jedenácti cvičení, která umíte řešit (i s vysvětlením matematického pozadí), nebo jedno z témat uvedených v seznamu cvičení. Zkouška by v každém případě měla zahrnout i prodiskutování některého důkazu. Zkouška může proběhnout kdykoliv se domluvíme (ale raději to prosím moc neodkládejte) přes Hangouts (s kamerou) nebo při osobním setkání v Celetné.

Course contents in Spring 2019/20 (Czech)

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

Huge number calculator

The calculator BNCalc.pdf is implemented as a (set of scripts behind a) pdf document and can be used for operating with really huge integers. Note that there are some undocumented key combinations that make it easier to repeat the given operation. The "result" text field in the "Factoring" page, marked by an arrow in this image, accepts Shift‑M (or Shift‑B with the same meaning). Also, the result text field on the preceding page accepts Shift‑M and Shift‑B.

History of Modern Mathematics and Logic

SIS ALGV00120

Course contents in Fall 2019/20

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

Huge number calculator

The calculator BNCalc.pdf is implemented as a (set of scripts behind a) pdf document and can be used for operating with really huge integers. Note that there are some undocumented key combinations that make it easier to repeat the given operation. The "result" text field in the "Factoring" page, marked by an arrow in this image, accepts Shift‑M (or Shift‑B with the same meaning). Also, the result text field on the preceding page accepts Shift‑M and Shift‑B.

Chapters in Classical Logic

About

A seminar partly based on students' presentations, devoted to various topics in metamathematics, non-classical logics, and proof theory. The topics usually include: Provability Logic, independence of the Paris-Harrington combinatorial principle over Peano arithmetic, relations between ZF, GB and the Kelly-Morse set theories, upper and lower bounds for cut-elimination in classical predicate logic, decision procedures for intuitionistic propositional logic. Here is the list of topics (in Czech). SIS: ALG500003.

Exams (Czech)

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

Course contents in 2019/20 (Czech)

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

Other activities

TeX/LaTeX, pdf, ...

FBUsersSetup

The Firebird SQL server comes with a command line utility gsec for manipulating database users. Using it, one can add, delete, or modify server's users, where a modification practically means a password change.

FBUsersSetup.exe is written as an Inno Setup Windows installer*)Unlike normal installers, it does not write anything to the registry and does not leave any trace on your computer. So no deinstallation is provided/needed. and it basically is a gui wrapper for the gsec utility. As such, it has little additional functionality in comparison to gsec. However, it is easy to use, it can modify users on any computer in or outside the local network, it never gets confused if there are parallel instances of Firebird running on the local computer, and it can detect the properties of the local Firebird(s).

The utility is rather self-explanatory, the essential dialog pages being

DBUSubst

The utility DBUSubst.exe can substitute one Firebird database user for another. A substitution of user M for existing user D in a database means that M becomes an owner of all database objects that user D owned, he inherits all privileges that were granted to D, and he becomes a grantor of all privileges that D granted. After being substituted out, user D grants and is granted nothing, and owns no database object. If D was an owner of a database then M becomes a new database owner. Thus user substitution is a more general operation than database ownership change.

Similarly as FBUsersSetup, DBUSubst.exe is written as a (harmless for your computer) Inno Setup Windows installer. It basically is a wrapper for the isql command line utility and some sql scripts. The scripts are available in DBUSubst.zip. They are documented and thus contain a detailed information about the substitution process. The document DBUSubst.pdf contains some introductory information about the user privileges and some Firebird internals. Two essential dialog pages of DBUSubst.exe are