Vítězslav Švejdar

In TeX/LaTeX, it is
V{\'\i}t{\v e}zslav {\v S}vejdar,
with spaces after both \v's.
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.

Exams

Ke zkoušce si prosím připravte seznam šesti cvičení ze seznamu cvModL.pdf, která dovedete řešit. Na poslední přednášce si tento požadavek upřesníme.

Course contents in Fall 2022/23 (Czech)

5. ledna 2023
Podrámce a disjunktní sjednocení rámců jako speciální případy bisimulace mezi rámci. Charakteristická třída libovolné logiky je uzavřena na podrámce, disjunktní sjednocení a p-morfní obrazy.
22. prosince 2022
Cresswellův model. Logika K + H je slabší než GL.
15. prosince 2022
Charakteristická třída logiky GL je třída všech tranzitivních obráceně fundovaných rámců. Táž třída je i charakteristickou třídou pro schéma H.
8. prosince 2022
Logika S5 a její charakteristická třída. Schéma 4 je dokazatelné v S5. V logice S4 platí, že z dvojice sousedících a stejných modalit lze jednu ekvivalentně vypustit. V S5 platí, že ze dvou sousedících libovolných modalit lze první ekvivalentně vypustit. Logika GL. Schéma 4 je dokazatelné v GL.
1. prosince 2022
Schémata 4, T, B a 5 a jejich charakteristické třídy. Logika S4.
24. listopadu 2022
Logika K4, příklad důkazu v ní, její gentzenovský kalkulus. Charakteristické třídy logik.
Domácí cvičení. 1. Dokažte, že hilbertovský a gentzenovský kalkulus se navzájem simulují. Takže jsou spolu ekvivalentní.
2. Nalezněte charakteristickou třídu logiky, která vznikne přidáním schématu A → □◇A k logice K.
3. Nalezněte charakteristickou třídu logiky, která vznikne přidáním formule ¬□⊥ → ¬□¬□⊥ ke K.
10. listopadu 2022
Logika K je rozhodnutelná. Pro oba její kalkuly platí věta o úplnosti. Pro gentzenovský kalkulus platí i věta o eliminovatelnosti řezů. Vlastnost konečných modelů: každá nedokazatelná formule má kripkovský protipříklad, který je konečným antireflexivním stromem.
3. listopadu 2022
Gentzenovský kalkulus pro logiku K. Vzájemná simulovatelnost gentzenovského a hilbertovského kalkulu. Podmodel kripkovského modelu generovaný prvkem.
27. října 2022
Zbývající pravidla kalkulu GK. Subformula property. Pro kalkulus GK platí věta o korektnosti, věta o úplnosti a věta o eliminovatelnosti řezů.
Domácí cvičení. Navrhněte vhodná pravidla pro spojku ≡.
20. října 2022
Dokazatelnost a nedokazatelnost v logice K. Gentzenovský kalkulus GK pro klasickou výrokovou logiku.
13. října 2022
Splněnost formule ve vrcholu kripkovského modelu, platnost formule v modelu. Schéma □A → □□A platí v každém modelu, jehož rámec je tranzitivní (ale i v některých jiných modelech). Logika K a její hilbertovský kalkulus.
Domácí cvičení. S užitím faktu, že všechny tautologie jsou dokazatelné, zdůvodněte, že □A&□B → □(A&B) je v K dokazatelná pro každou volbu formule A.
6. října 2022
Opakování klasické výrokové logiky: logické spojky, tautologie, tautologický důsledek, věta o kompaktnosti. Modality nutnosti a možnosti. Modální výrokové formule. Různé modální principy. Například □A → A se tradičně nazývá princip T. Dále □(□A → A) → □A je Löbův axiom, kdežto □A → A / A je Löbovo pravidlo.
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?

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 2023/24

Nov 30th, 2023
Examples of axiomatizable classes and classes that are not axiomatizable. The complement of a finitely axiomatizable class C, i.e. the class of all structures for the given language that are not in C, is again finitely axiomatizable. Definable sets and definable elements of a structure.
Homework. Exercises 10–13 are not so difficult and they are partly already solved. 14 and 17 are hopefully illustrative but also not very difficult. 15 and 16 are more tricky. Please pick some of these and send a solution or questions concerning them.
Nov 28th, 2023
General Łoś-Vaught test: if T is consistent, has no finite models and is κ-categorical for some uncountable κ, then it is complete. SUCC is an example of a theory to which this theorem is applicable. Axiomatizable and finitely axiomatizable classes of structures. Example: if L is an arbitrary language, then the class of all finite structures for L is not axiomatizable. This is an almost immediate consequence of the theorem saying that if T has unboundedly large finite models, then it also as infinite models.
Nov 23rd, 2023
Review of semantic results and their consequences: Weak Löwenheim-Skolem theorem, Weak Łoś-Vaught test (we already discussed it on Tuesday), the compactness theorem. If T has unboundedly large finite models, then it also has infinite models. It T has infinite models, then it has models of any cardinality κ ≥ |L| + ℵ0. A consequence is that Th(〈N,+,0,s〉) has models of any infinite cardinality. It is clear that the order type of an uncountable model of this theory is  ω + (ω* + ω) · λ where λ is a dense linear order. It remains to prove the existence of countable nonstandard models of this theory.
Nov 21st, 2023
Vaught (Łoś-Vaught) test: if T is consistent, its language is at most countable and every two at most countable models of T are isomorphic, then T is complete. There are not so many theories to which this test is applicable. One example is DNO, the theory of dense linear order with no endpoints.
Nov 16th, 2023
Quantifier elimination for the theory DOS. Other classroom examples of structures that admit quantifier elimination (i.e., from which a theory admitting quantifier elimination can be spotted out) are 〈R,<〉 and 〈R,+,0,1〉. More difficult examples, important in the history of logic, are as follows. In 1929 Presburger showed that 〈N,+,0,s〉 admits quantifier elimination. The theory of this structure is called Presburger arithmetic. Later Tarski showed the same about the structure ℝ of the reals (with both addition and multiplication). For more about the history (of quantifier elimination) see the paper Doner-Hodges and Tarski's bibliography by Givant. They cite Tarski's book published in 1948 but they also seem to suggest that Tarski obtained this result already in 1930. Probably not: the same Wilfred Hodges speaks here about the year 1949.
Homework. Exercise 19.
Nov 14th, 2023
DO, the theory of discrete linear order. The theory DOS is a conservative extension of DO. In fact, it is an extension by definitions. It is also a conservative extension of SUCC. Some notation for types of linear order: ω and η are shorthands for the types of 〈N,<〉 and 〈Q,<〉 respectively. Examples of models of DO are ω, ω + ω* + ω, and also ω + (ω* + ω) · λ where λ is any linear order.
Nov 9th, 2023
The remaining part of the proof of quantifier elimination for the theory SUCC. This theory is complete. It is clear that any two models of a complete theory are elementarily equivalent. That is, they do not differ in the validity of any sentence. In particular, 〈N,0,s〉 and 〈N,0,s〉 + 〈Z,s〉 are elementarily equivalent. There is no formula in the language {0,S} saying that “the number x is reachable from zero by finitely many steps of the successor function”. Contrary to what was said today, the book does not contain a brief proof of the quantifier elimination for SUCC, my apologies. It discusses a closely related theory DOS. This is a plan for the next talk.
Nov 7th, 2023
Three lemmas concerning the theory Q where the third of them says that every open sentence in the arithmetic language is either provable or refutable in Q. The same three lemmas clearly hold also for the theory SUCC. The theory SUCC admits quantifier elimination: every formula φ in the language {0,S} is SUCC-equivalent to a quantifier-free formula containing no other free variables than those occurring free in φ. To show this, it is sufficient to treat formulas of the form ∃xψ where ψ is a clause (a conjunction of literals).
Nov 2nd, 2023
The axioms Q1–Q9 of Robinson arithmetic Q. Facts about ≤ and < provable and unprovable in Q. A simple model with two nonstandard elements shows that the properties of operations (like the commutativity and distributivity) and of order (like the transitivity) are usually unprovable in Q. Robinson arithmetic is not a conservative extension of Q1–Q5.
Oct 31st, 2023
Extensions and conservative extensions of a theory. Q1–Q5 is a conservative extension of Q1–Q3. The axioms Q8 and Q9 concerning the unstrict and strict order. Example sentences provable and unprovable in Q1–Q5,Q8,Q9. A special case of conservative extension is extension by definitions. Q8 and Q9 are definitions in this sense, and Q1–Q5,Q8,Q9 is thus a conservative extension of Q1–Q5 (and of Q1–Q3).
Oct 26th, 2023
Aspects of the completeness theorem: the strong completeness theorem is in fact a conjunction of two claims, the completeness theorem (no adjective) and the compactness theorem. The fact that the Zermelo-Fraenkel set theory, if it is consistent, also has countable models is called Skolem's paradox. However, there is nothing paradoxical about it. The axioms Q4 and Q5. Example sentences provable from Q1–Q5.
Homework. Show that every model of Q1–Q3 has an expansion that is a model of Q1–Q5.
Hint. We know how each model of Q1–Q3 looks like: the standard part, which is isomorphic to 〈N,0,s〉, plus any number of finite loops of arbitrary sizes, plus any number of chains isomorphic to 〈Z,s〉.
Oct 24th, 2023
Many different models for various theories, some notation for them (like 〈N,0,s〉 + 〈Z,s〉 + 〈Z,s〉). The theory SUCC. The strong completeness theorem and the Löwenheim-Skolem theorem.
Oct 19th, 2023
Standard and nonstandard elements of structures in which at least Q1 and Q2 are valid. Standard and nonstandard models. Logically valid formulas. The consequence relation. Contradictory and consistent theories.
Homework. No homework is officially assigned. However, all exercises 1–11 are solvable now. Anyone who can solve Exercise 4 obviously mastered the definition of the consequence relation.
Oct 17th, 2023
Tarski's definition. Lines concerning connectives imply that all tautologies are valid in every structure. The soundness of the generalization rules. The strong soundness theorem as a tool for proving unprovability.
Homework. Exercise 9.
Oct 12th, 2023
The deduction theorem. A review of semantic notions: valuation of variables in a structure, formula satisfied by a valuation in a structure, formula valid in a structure. The soundness theorem.
Oct 10th, 2023
A survey of Hilbert-style calculus HKe. A formal proof of ∃x(P(x) → ∀yP(y)) in the theory with no axioms and of ∀x∃y(S(y) ≠ x) in the theory having Q1 and Q2 as axioms.
Homework. show that also ∃x(∃yP(y) → P(x)) has a formal proof.
Oct 5th, 2023
More examples of informal and formal proofs. The generalization rules. Numerals.
Homework. Construct formal proofs of some (not necessarily all) formulas in Exercise 1.
Oct 3rd, 2023
A review of logical syntax: from terms to sentences and axiomatic theories. Terms, formulas, axiomatic theories. A sample theory having Q1 and Q2 as axioms.
Homework. Think about an informal proof of the sentence numbered (iii).

Arithmetics and algorithms

Please pay attention to the list of exercises.

SIS ALG110008, Zoom.

Exams (Czech)

Ke zkoušce si prosím připravte (přineste) řešení patná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. V SISu budou vypsány nějaké termíny na pokud možno všechny úterky do konce června s výjimkou týdne od 20.6. Později pokud možno i v září, ale počítejte prosím s určitou improvizací a ne s úplně každým týdnem. Všechny termíny lze využívat i jako konzultace a mailem se lze domluvit i na jiné dny než ty vypsané v SISu, většinou na Po a St navečer nebo Út celkem kdykoliv.

Course contents in Spring 2022/23 (Czech)

11. května 2023
Když p je prvočíslo a k je dělitel čísla p - 1, pak v grupě Φ(p) je přesně φ(k) prvků řádu k. Z toho mimo jiné plyne, že ve Φ(p) existují prvky maximálního možného řádu p - 1, neboli že Φ(p) je cyklická grupa.
4. května 2023
Řády prvků v grupách. Řád libovolného a ∈ Φ(n) musí být dělitelem čísla φ(n). Známé tvrzení, že polynom stupně k, který není identicky nulový, má nejvýše k různých kořenů, platí ve všech oborech integrity.
27. dubna 2023
Kryptografická metoda RSA. Mersennova čísla a Mersennova prvočísla.
20. dubna 2023
Počítání s modulárními reprezentacemi. Čínská zbytková věta.
13. dubna 2023
Umocňování xy v ℤm, chápané jako funkce tří proměnných, je polynomiálně počitatelné. Pseudoprvočísla.
30. března 2023
Bézoutova věta jako důsledek korektnosti čtyřsloupcového Eukleidova algoritmu. Některé její důsledky: ekvivalentní podmínka pro nesoudělnost nenulových čísel a a b (tj. podmínka ∀z(a ∣ bz → a ∣ z)) a fakt, že když prvočíslo je dělitelem součinu xy, musí být dělitelem některého z čísel x a y (toto ponecháno jako cvičení).
23. března 2023
Úloha určit (z a a m), zda a je v ℤm invertibilní, a také úloha nalézt inverzní prvek k invertibilnímu a jsou polynomiálně počitatelné. Nesoudělnost, prvočísla (v oborech integrity). Čtyřsloupcové rozšíření Eukleidova algoritmu.
Domácí úkol: cvičení 5 (cvičení 1-4 jsou také řešitelná nebo již vyřešená).
16. března 2023
Definice největšího společného dělitele, úloha GCD. Eukleidův algoritmus a jeho časové nároky.
9. března 2023
Eulerova grupa (nějakého přirozeného čísla). Tělesa a obory integrity. Dělitelnost v oborech integrity.
Cvičení. Dokažte, že relace asociativnosti je ekvivalence.
2. března 2023
Komutativní monoidy a komutativní (čili Abelovy) grupy. Invertibilní prvky monoidu tvoří grupu. Věta (možná Eulerova) o umocňování v konečných komutativních grupách. Okruhy a počítání s opačnými prvky v nich. Struktury ℤ, ℚ, ℤm a ℚ[x] jako příklady okruhů.
23. února 2023
Pojem polynomiálního algoritmu. Rozdíl mezi úlohami Factoring a Primes. Monoidy 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í?
16. února 2023
Několik všeobecně matematických pojmů: přirozená, celá a racionální čísla, dělení se zbytkem, relace a některé jejich vlastnosti (reflexivita, tranzitivita). Logické symboly (spojky a kvantifikátory). Úlohy a algoritmy. Úlohy Mult a Primes, a algoritmy, které je počítají. Časové nároky algoritmů. Například školní algoritmus pro úlohu Mult počítá v kvadratickém čase.

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 19th, 2023) list of exercises.

SIS ALG119007, Zoom.

Exams (Czech)

Please bring a list of 14 exercises whose solution you are able to present.

Course contents in Spring 2022/23

May 11th, 2023
Completeness of the propositional calculus GJ. Two by-products of the proof: the cut-elimination theorem and the finite model property. Kripke semantics of intuitionistic predicate logic.
May 9th, 2023
The relationship between classical and intuitionistic logic: Glivenko's theorem. The disjunction property. The calculus GJ.
May 4th, 2023
Constructing Kripke counterexamples. Every intuitionistic tautology is a (classical) tautology.
May 2nd, 2023
Kripke semantics for intuitionistic propositional logic.
Apr 27th, 2023
Essentially undecidable and essentially incomplete theories. Motivating considerations concerning intuitionistic logic.
Apr 25th, 2023
Rosser's theorem. Craig's trick.
Apr 20th, 2023
Some connections of Gödel's 2nd theorem: Hilbert's program, uniqueness of fixed points, the variety of formulas τ(z) defining the same theory.
Apr 18th, 2023
Gödel's second incompleteness theorem. Its formalization in PA.
Apr 13th, 2023
The self-reference theorem. Th(ℕ) is a non-arithmetical set. Gödel's self-referential sentence.
Apr 11th, 2023
Löb's derivability conditions. An ad hoc semantics showing that some consistency statements are provable in PA.
Apr 4th, 2023
Facts about provability (the deduction theorem etc.) that are provable in PA. The formalized completeness theorem.
Mar 30th, 2023
Formalization of provability and consistency in PA.
Mar 28th, 2023
Using balanced strings in some cases, the basic syntactic notions (variables, terms, formulas, substitutability, the substitution function etc.) can be formalized in PA.
Mar 23rd, 2023
String functions, balanced strings.
Mar 21st, 2023
Partial recursive functions are closed under primitive recursion and course-of-values recursion. An infinite subset of N is RE if and only if it is the range of some one-to-one function.
Mar 16th, 2023
Partial recursive functions are closed under composition and minimization.
Mar 14th, 2023
Some connections between RE sets and partial recursive functions: a set is a projection of a Δ0 relation (or a projection of a recursive relation) if and only if it is the domain of some partial recursive functions, and a nonempty subset of N is RE if and only if it is the range of some recursive function.
Mar 9th, 2023
Recursively enumerable sets, partially recursive and recursive functions. The collection schema (with some additions) can be used to construct an alternative axiomatization of PA.
Mar 7th, 2023
Further functions formalizable in PA: the number of bits in the binary expansion of x (its graph is Δ0(PA)) and the number of primes less than x (its graph is certainly Σ1(PA), but it is not known to be Δ0(PA)).
Mar 2nd, 2023
Exponentiation can be formalized in PA. The formula y = zx is Δ0(PA).
Feb 28th, 2023
The fact that irreducible numbers are the same as prime numbers is provable in PA. Properties of powers of two are provable in PA as well. For example, the product of any two powers of two is again a power of two.
Feb 23th, 2023
The infinitude of irreducible numbers, and also Bézout's theorem are provable in PA.
Feb 21th, 2023
The least number principle (LNP) is provable in PA. More exactly, over (Q + ∀x(x<S(x))) it is equivalent to the induction schema. However, these two schemas are not equivalent over Q itself.
Feb 16th, 2023
Peano arithmetic PA. Using the schema Ind to prove the expected properties of operations and the two order relations.
Feb 14th, 2023
Robinson arithmetic and its properties.

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 2022-23. 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í přednáška se do počtu 13 počítá trojnásobně.

Course contents in 2022/23 (Czech)

Nezávislost Paris-Harringtonova principu na PA (D. Roubínek, 2. a 9.5.)
Poslední kapitola v knize Handbook of Mathematical Logic.
Intuicionistická predikátová logika (B. Heřmanová, 3.5 týdne od 4.4.)
Sémantika intuicionistické predikátové logiky. Tři prenexní implikace, které nejsou intuicionisticky logicky platné. Schéma DNS. Chování rovnosti, mimolehlost, axiomy stability.
Kombinatorické principy nezávislé na PA (D. Roubínek, 4 týdny od 7.3.23)
Kayova teorie PA-. Ramseyova věta. Důkaz nekonečné Ramseyovy věty převedením na Königovo lemma.
Hyperprosté množiny a nezávislá axiomatizovatelnost (J. Urbánek, 5 týdnů od 22.12.)
Ekvivalentní definice hyperprosté množiny. Rekurzívně axiomatizovatelná teorie je nezávisle axiomatizovatelná, právě když má axiomatizaci { αi ; i ∈ N }, jejíž markant (tj. množina všech n takových, že αn+1 je dokazatelná z konjunkce všech αi pro i ≤ n) není hypersimple. To je právě tehdy, když každá axiomatizace má tuto vlastnost.
Aritmetická úplnost logiky dokazatelnosti (V. Švejdar, 5 týdnů od 15.11.)
Varianty axiomatizace logiky GL. Logika GLS, která není normální, je kandidátem na logiku, která axiomatizuje množinu všech ℕ-tautologií. GLS-modely. Kripkovská úplnost logiky GLS. Solovayův důkaz aritmetické úplnosti obou logik.
Metamatematika teorií množin (M. Blahynka, 3 týdny od 25.10.22)
Gödelova-Bernaysova teorie množin GB a její konečná axiomatizovatelnost. Pravdivostní relace a obsaditelná přirozená čísla. V GB není dokazatelná indukce pro všechny její formule, a je nad ZF konzervativní vůči množinovým sentencím.
Autoreference (V. Švejdar, 3 týdny)
Aritmetizace dokazatelnosti. Löbovy podmínky. Gödelova, Henkinova a Löbova autoreferenční rovnice. Přinejmenším první dvě mají jednoznačně určené řešení.

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

Další plány
Timea Cochová: něco (cokoliv) na téma Gentzen, Adam Fürstenzeller: Smorynského článek o Hilbertově programu.
L. E. J. Brouwer: Life, Art and Mysticism (Šimon Pošta, od 16.11.)
Detlefsenův článek Brouwerian intuitionism je teď volný.
Detlefsenův článek z roku 79 (Timotej Šujan, od 2.10, 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

Modified: Nov 30, 2023 21:11. These links are duplicate but can be bookmarked: Publ, Book, Mod L, Log, Chapt, Ar Alg, Incompl, IGT, Other.