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.

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 AA 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 □(□pp) → □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 AA. Löb's axiom schema L is □(□AA) → □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 AB ⇒ ¬AB.
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

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 ∃ 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), xyR(x,y) → ∀yxR(x,y)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 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 xU. 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ž xy a yx.
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)xyz(xy → (xy+zxz)) 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 Δ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 ∀xy(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 AREΔ1 and φ(x) is a Σ1-formula that defines it, then the equivalence n(nAφ(\bar{n})∈Th(ℕ)) shows that Am 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 Am B, if there exists a recursive function f such that n(nAf(n)∈B). If Am 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

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