Introduction
About me
Associate professor at the Department of Logic,
College of Arts ("Faculty of Arts"), Charles University in PragueFilozofická fakulta UK,
Palachovo nám. 2, 11638 Praha 1.
Courses Computability (an introduction to recursive functions),
Classical Logic II (with an emphasis on incompleteness and undecidability),
and some others related to metamathematics or to algorithms.
Research interests
Interpretability of axiomatic theories, arithmetization, related modal logics, algorithmic aspects
of non-classical logics.
Experience and education
During 1982-90 worked as a software developer for an industrial company ČKD Polovodiče.
Participation in writing a control system for PDP-11 computers.
The system was designed by Jan Pavelka*)Accidentally
the same Jan Pavelka who, a few years before turning into a respected software developer,
wrote innovative papers about fuzzy logics., and was successfully applied in
several branches of industry like steel rolling or international transport of natural gas.
Ph.D. in mathematical logic, Ph.D. study in the Institute of Mathematics of the Academy of Sciences
of the Czech Republic.
Dissertation Self-Reference and Modal Logic, 1982,
supervisor Petr Hájek. Graduated in mathematics from Charles University, 1978,
master's thesis Degrees of Interpretability.
Office info, events, miscellaneous updates
Office hours Thu 15:00, or by appointment.
For more info please see the image above, or the web of the
department.
Nabídka témat bakalářských a diplomových prací:
TemataPraci13.pdf
Publications
BibTeX file
BibTeX entries can be taken from sv.bib. Note that the file
contains a preamble with some strings and macros.
Book
- Logika: neúplnost, složitost a nutnost
(Logic: Incompleteness, Complexity, and Necessity),
Academia Praha, 2002.
464 pages,
section 5.2 about Gödel-Dummett fuzzy logic was written by Petr Hájek. See the
"Book" tab above.
Some workshop or conference presentations
-
Logika, Gödel, neúplnost (Logic, Gödel, Incompleteness).
A talk at Friday meetings of Sysifos,
February 23th, 2018. A videorecord created by Ludvík Hájek is available on
YouTube.
-
Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and
Incompleteness). A talk at Hvězdárna and planetárium Brno (Brno Observatory and Planetarium),
March 9th, 2017. A videorecord created by Josef Forman is available on
YouTube.
-
Rosser Sentences and Rosser Logics.
A talk at the Prague gathering of logicians,
Jan 2017.
-
On Purely implicational Fragments of Intuitionistic
Propositional Logic. A talk at the Logica '11 International Conference,
Hejnice, Czech Republic, June 2011. [pdf4]
Papers
- Do We Need Recursion? In I. Sedlár and M. Blicha, eds.,
The Logica Yearbook 2019,
pp. 193–204. College Publications, London, 2020. [pdf][talk]
- Modern Czech Logic:
Vopěnka and Hájek, History and Background. Journal of Applied Logics — IfCoLoG Journal
of Logics and their Applications, 5(6):1261–1271, 2018. [pdf]
- Předmluva: o logice 20. století (Preface: On the 20th Century Logic).
In L. Dostálová, ed., Kurt Gödel: úplnost a neúplnost (Kurt Gödel: Completeness and Incompleteness),
pp. 13–53. OPS in collaboration with University of West Bohemia Publishing,
Plzeň, 2015. ISBN 978-80-87269-39-8. In Czech. [pdf]
- On Strong Fragments of Peano Arithmetic.
In P. Arazim and M. Dančák, eds.,
The Logica Yearbook 2014,
pp. 281–291. College Publications, London, 2015. [pdf][talk]
- Výuka logiky bez logických pojmů (Teaching logic without the use
of logical notions). In L. Dostálová and K. Šebela, eds.,
Organon VII — Nihil novi, pp. 49–57. University of West Bohemia Publishing,
Plzeň, 2011. ISBN 978-80-261-0035-5. In Czech.
[pdf][pdf2]
- Infinite natural numbers: an unwanted phenomenon, or a useful concept?
In M. Peliš and V. Punčochář, eds.,
The Logica Yearbook 2010,
pp. 283–294. College Publications, London, 2011. [pdf][pdf2][talk]
- Decision Problems of Some Intermediate Logics and Their Fragments. In M. Peliš, ed.,
The Logica Yearbook 2009,
pp. 297–307. College Publications, London, 2010. [pdf][pdf2][talk]
- Relatives of Robinson Arithmetic. In M. Peliš, ed.,
The Logica Yearbook 2008,
pp. 253–263. College Publications, London, 2009. [pdf][pdf2][talk]
-
On Interpretability in the Theory of Concatenation.
Notre Dame Journal of Formal Logic, 50(1):87–95, 2009.
[pdf][pdf2]
- Weak Theories and Essential Incompleteness. In M. Peliš, ed.,
The Logica Yearbook 2007, pp. 213–224. Filosofia, Praha, 2008.
[pdf][pdf2][talk]
-
An Interpretation of Robinson Arithmetic in its Grzegorczyk's Weaker Variant.
Fundamenta Informaticae, 81(1–3):347–354, 2007.
[pdf][pdf2]
- Gödel-Dummett Predicate Logics and Axioms of Prenexability.
In O. Tomala and R. Honzík, eds.,
The Logica Yearbook 2006, pp. 251–260. Filosofia, Praha, 2007.
[pdf][pdf2][talk]
- On Modal Systems with Rosser Modalities. In M. Bílková and O. Tomala, eds.,
The Logica Yearbook 2005, pp. 203–214. Filosofia, Praha, 2006.
[pdf][pdf2][talk]
-
On Sequent Calculi for
Intuitionistic Propositional Logic.
Comm. Math. Univ. Carolinae, 47(1):159–173, 2006.
[pdf][pdf2]
-
With Blanka Kozlíkova, On
Interplay of Quantifiers in Gödel-Dummett Fuzzy Logics.
Archive for Math. Logic, 45(5):569–580, 2006.
[pdf][pdf2]
-
Note on
Inter-Expressibility of Logical Connectives in Finitely-Valued Gödel-Dummett Logics.
Soft
Computing, 10(7):629–630, 2006.
[pdf][pdf2]
-
Gödlov prvi izrek o nepolnosti.
Obzornik za matematiko in fyziko, 51(4):113–121, 2004.
-
The limit lemma
in fragments of arithmetic. Comm.
Math. Univ. Carolinae, 44(3):565–568, 2003.
[pdf][pdf2]
-
A
note on arithmetical completeness of theories with Rosser modalities.
In K. Bendová and P. Jirků, eds., Miscellanea logica V,
pp. 123–132. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
-
On
structural proofs of Gödel First Incompleteness Theorem.
In K. Bendová and P. Jirků, eds., Miscellanea logica V,
pp. 115–122. Karolinum, Praha, 2003. ISBN 80-246-0799-9.
-
The decision problem of
provability logic with only one atom.
Archive for Math. Logic, 42(8):763–768, 2003.
Errata: The final paragraph, just before the list of references, contains an unpleasant
misprint: 'added in January 2002', should be 'added in January 2003'. My apologies!
[pdf][pdf2]
-
On the polynomial-space
completeness of intuitionistic propositional logic.
Archive for Math. Logic, 42(7):711–716, 2003.
[pdf][pdf2]
-
With K. Bendová,
On Inter-Expressibility
of Logical Connectives in Gödel Fuzzy Logic.
Soft
Computing, 4(2):103–105, 2000.
[pdf][pdf2]
-
On Provability Logic.
Nordic
Journal of Philosophical Logic, 4(2):95–116, 2000.
[pdf][pdf2]
-
Arithmetical
Classification of the Set of All Provably Recursive Functions.
Comm. Math. Univ. Carolinae, 40(4):631–634, 1999.
[pdf][pdf2]
-
Poznamka
o vztahu vyplyvani v klasicke predikatove logice (A Note on
the Consequence Relation in Classical Predicate Logic). In
P. Jirků and V. Švejdar, eds., Miscellanea
Logica II. Karolinum, Praha, 1999. In Czech.
-
Logika
v aritmetice. In P. Jirků and V. Švejdar, eds.,
Miscellanea Logica I. Karolinum, Praha, 1998. In Czech.
-
With P. Hájek, Matematicka logika (Mathematical Logic).
Praha, November 1994. Lecture notes, electronic version only, in Czech.
-
Some Independence Results in Interpretability Logic.
Studia Logica, 50(1):29–38, 1991.
- With P. Hájek,
A Note on the Normal Form of Closed Formulas
of Interpretability Logic. Studia Logica, 50(1):25–28, 1991.
-
Modal Analysis of Generalized Rosser Sentences. J. Symb. Logic, 48(4):986–999, 1983.
[JSTOR]
-
A Sentence that is Difficult to Interpret.
Comm. Math. Univ. Carolinae,
22(4):661–666, 1981.
-
Degrees of Interpretability.
Comm. Math. Univ. Carolinae,
19(4):789–813, 1978.
Logic: Incompleteness, Complexity, and Necessity (Academia, 2002)
I do not think logic is a field where people are taught how to think logically.
Instead, I consider it a theory about deductive thinking for people who already
are able to think logically, usually because they have some experience with
academic mathematics.
My ambition was to have more than a list of definitions, theorems, and proofs; I am
trying to include comments and explanations, and I believe that the reader should be led
from some questions to some solutions.
I am grateful to Petr Hájek, who was my teacher and who gave one of the initial
impulses for writing this book. He actually wrote only a small part of the text, but
much larger part and perhaps everything was inspired by him.
As a result of an agreement with the Academia publishing company,
a pdf version of the book is now available
(full text!) for study purposes (only!). When downloading the file, it is recommended
to download also Errata
and save both files to the same folder on local computer. That will activate the links
in the text marked by big red 'E'.
Redistribution and modifications of the file are not allowed! Printing of
(any part of) the document is not allowed!
Po domluvě s nakladatelstvím Academia je nyní
plný text knihy ve formátu pdf
přístupný pro studium (pouze!). Při kopírování souboru na lokální
počítač je doporučeno stáhnout také Errata
a umístit oba soubory do téže složky. Soubor nesmí být dále šířen
ani nesmí být modifikován! Žádná jeho část nesmí být tištěna!
Click on the blue word 'Academia' on the first page of the book to obtain
further information about their bookstores and other books they publish.
Comments and additions to Errata are welcome.
Modal and non-classical logics
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
Exercises
Please pay attention to the list of exercises.
Here are the same exercises in English.
Exams
For the exam please prepare a list of twenty-one exercises that you can solve.
Exercise 22 (provability in Q) can be counted three times.
Course contents in Fall 2023/24
- Dec 21th, 2023
- A consequence of the above theorem is that the collection of Δ1 sets
is closed under Boolean operations and bounded quantification. Also, all projections of
Δ1 sets are RE. Both Dom(f) and Rng(f)
of a partial recursive f are RE. In fact, a set is RE if and
only if it is the domain of some partial recursive function. This claim is known as the projection theorem.
The graph of a recursive f must be Δ1.
For each pair A and B of RE sets there exist RE sets
X and Y such that
X ∪ Y = A ∪ B,
X ∩ Y = ∅,
A – B ⊆ X
and B – A ⊆ Y. Two sets
A and B are
recursively separable if there exists a recursive set D such that
A ⊆ D
and D ∩ B = ∅.
Any two disjoint Π1 sets are recursively separable. This is an easy consequence
of the just mentioned theorem.
However, there exist RE sets A and B that are disjoint
and recursively inseparable. This fact will be useful in the proof of (a variant of) the incompleteness theorem.
- Dec 19th, 2023
- Further official definition: a set is Δ1, i.e. recursive, if it is both
Σ1 and Π1. A function f of
q variables is partial recursive if Graph(f), i.e. f taken as a set
of (q + 1)-tuples, is RE. A function f of
q variables is recursive if it is partial recursive and total (its domain Dom(f)
equals Nq). The collection of Σ1 sets is closed under
∃, &, ∨ and bounded quantification. The collection of Π1 sets is closed
under ∀, &, ∨ and bounded quantification.
- Dec 14th, 2023
- A theory T is recursively axiomatizable if it is equivalent to a theory S such
that S is a recursive set. If T is recursively axiomatizable, then Thm(T), i.e.
the set of all sentences φ such
that T ⊢ φ, is recursively
enumerable. Indeed, T ⊢ φ is equivalent
to ∃dProofT(φ,d) where
ProofT(φ,d) is the condition "d is a proof
of φ in T", and we expect that (once we state a definition) this
condition is recursive. A theory T is decidable if Thm(T) is recursive. Post's theorem
is also one of the expected facts since if both A
and Nq – A are RE, then we
can specify an informal but obviously correct algorithm that decides the membership to A.
Now finally the definition: a set is RE if it is the projection of some
Δ0 relation, i.e. if it is definable in ℕ by a formula of the
form ∃vφ(v,x)
where φ ∈ Δ0.
A set is Π1 if it is definable in ℕ by a formula of the
form ∀vφ(v,x)
where φ ∈ Δ0.
- Dec 12th, 2023
- A subset of a domain whose elements can be written as strings (finite sequences of symbols)
is a decision problem. A decision problem is in fact a set of questions called instances.
It may or may not be algorithmically decidable (recursive). By definition, something is an algorithm if
it can be formalized in a fixed computational model. A string can be coded by a natural number. A natural
way of coding is to consider individual symbols digits in B-ary notation where B is a sufficiently big
number (B = 128 certainly suffices). Thanks to coding we can postulate that
a decision problem is a subset of the set Nq for some q.
When speaking about decision problems, we alternate between set theoretic terminology where we have
intersections, complements etc., and logical terminology where we have conjunctions, negations etc.
A set-theoretic name for existential quantification is projection. A set is recursively enumerable
(RE) if it is the projection of a recursive sets. An example of an RE set
is the set of all sentences provable in Q.
- Dec 7th, 2023
- The Σ-completeness theorem: a Σ-sentence (both assumptions are crucial) valid
in ℕ is provable in Q. The claim that a Δ0-sentence is never independent
of Q is an easy consequence of this theorem, but it actually acted as one step in its proof.
- Dec 5th, 2023
- Quantifier elimination can be used to characterize sets definable in a structure (that admits
quantifier elimination). Bounded formulas, i.e. Δ0-formulas, of the arithmetic language. Many useful
properties of natural numbers (concerning divisibility, primes, powers of two) can be expressed via
Δ0-formulas. The collection of sets and relations definable in ℕ by
Δ0-formulas is denoted by Δ0. Or
by Δ0 with ℕ in the superscript.
- 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
Exercises (updated May 19, 2024).
Exams (Czech)
Ke zkoušce si prosím připravte (přineste) řešení cvičení 8 a dalších libovolně zvolených
třinácti cvičení (i s vysvětlením matematického či algoritmického pozadí). Zkouška pak pokračuje prodiskutováním
některého důkazu. Kromě termínů vypsaných v SISu se lze domluvit i na jinou dobu, ale ve středu obvykle mohu
až tak od 17h, a v pátek pouze ráno a pouze možná. Všechny termíny lze využívat i jako konzultace.
Course contents in Spring 2023/24 (Czech)
- 14. května 2024
- Chybějící část důkazu z minulé přednášky: když m je prvočíslo a a∈Φ(m)
má řád k, pak každý prvek b řádu k se rovná
některému ai pro i<k. Avšak když i je soudělné
s k, pak ai nemá řád k. Takže počet prvků řádu k
je nejvýše φ(k).
- 7. května 2024
- Několik poznatků, které se skládají na tvrzení, že když m je prvočíslo a k je dělitel
čísla m - 1, pak v grupě Φ(m) je
přesně φ(k) prvků řádu k. Toto bylo téměř ale ne zcela dokončeno.
Dokončení a vysvětlení, jak na základě těchto úvah definovat certifikát pro prvočíslo, je (kromě konzultace
na jakékoliv téma), plánem na Út 14.5.
- 25. dubna 2024
- Mersennova čísla a Mersennova prvočísla. Výsledek Franka Colea z roku 1903, že jedním z dělitelů
čísla 267 - 1 je 193 707 721,
umožňuje neformálně vysvětlit, co je třída NP. Úloha U je ve třídě NP, jestliže pro ni lze
definovat krátká data (certifikát), která když jsou pro daný vstup x předložena, lze z nich a
z x polynomiálním algoritmem potvrdit, že x ∈ U.
Jinými slovy, úlohy ve třídě NP jsou úlohy s efektivní verifikovatelností pozitivních instancí.
Certifikát pro složené číslo větší než 2 je přirozené definovat jako (některý) dělitel onoho čísla.
Takže množina všech složených čísel větších než 2 je úlohou ve třídě NP.
Třída P všech polynomiálně rozhodnutelných úloh je podtřídou třídy NP.
Řády prvků v grupách. Řád libovolného prvku grupy Φ(m) musí být dělitelem
čísla φ(m). Úvahy o řádech směřují k výsledku, že i množina všech prvočísel je
úlohou ve třídě NP. Což je (na rozdíl od celkem nedávného silnějšího výsledku, že množina všech prvočísel je
dokonce úlohou ve třídě P) fakt na školní úrovni celkem dosažitelný.
- 23. dubna 2024
- Výpočet čísla φ(m) na základě seznamu prvočísel v prvočíselném rozkladu čísla m.
Šifrovací metoda RSA. K jejímu prolomení by stačil polynomiální algoritmus pro nalezení prvočíselného
rozkladu. Stačil by i algoritmus pro výpočet funkce φ, ale ani jeden z takovýchto algoritmů není
znám (protože pravděpodobně neexistuje).
- 16. dubna 2024
- Důkaz čínské zbytkové věty. Počítání s modulárními reprezentacemi. Pseudoprvočísla.
Cvičení. Ověřte pomocí počítání s modulárními reprezentacemi, že 567 je pseudoprvočíslo.
Číslo 641, které pravděpodobně bylo zmíněno v přednášce, pseudoprvočíslem není (protože je to prvočíslo).
Ale s užitím faktu, že v ℤ43 platí 214 = 1,
by šlo ověřit, že 645 je pseudoprvočíslo.
- 9. dubna 2024
- Nejen určování invertibility v ℤm a výpočet inverzního prvku jsou
polynomiálně počitatelné. Také pro umocňování, tj. pro výpočet
funkce [m,x,z] ↦ Mod(zx,m)
existuje polynomiální algoritmus. Eulerova grupa a Eulerova funkce. Eulerova věta: pro libovolné m
a libovolné x∈Φ(m)
platí xφ(m) = 1. V tomto tvaru
ji budeme potřebovat, ale přehlednější důkaz má trochu obecnější verze: v komutativní grupě s n prvky
umocnění libovolného prvku na n-tou dá jedničku čili neutrální prvek té grupy. Modulární reprezentace.
- 2. dubna 2024
- Dva důsledky Bézoutovy věty, tj. dvě tvrzení dokazatelná v teorii, jejímiž axiomy jsou Bézoutova věta
a axiomy obory integrity: ekvivalentní podmínka pro nesoudělnost a fakt, že každé ireducibilní číslo je
prvočíslem. To druhé je domácí úkol kontrolovaný (až) u zkoušky. Eukleidův algoritmus lze užít k rozhodnování
o invertibilitě v ℤm. Jeho čtyřsloupcovou variantu lze užít k výpočtu
inverzního prvku. Když m je prvočíslo, pak ℤm je těleso.
Není-li m prvočíslo, pak ℤm není ani obor integrity.
- 26. března 2024
- V libovolném oboru integrity platí, že každé prvočíslo je ireducibilní. Rozšířený (čtyřsloupcový)
Eukleidův algoritmus. Z něj (z jeho analýzy) plyne Bézoutova věta pro strukturu celých čísel:
ke každé dvojici a a b existuje dvojice x a y taková, že
ax + by je společným dělitelem (je jasné, že největším
společným dělitelem) čísel a a b.
- 19. března 2024
- ℤ a ℚ[x] jako příklady oborů integrity. Také každé těleso je oborem integrity.
Nenulovým prvkem lze v oboru integrity krátit. Dělitelnost v oborech integrity: asociované prvky, dělitelé jedničky,
nesoudělnost, největší společný dělitel. Prvky x a y jsou spolu asociované, právě když
x ∣ y a y ∣ x.
- 12. března 2024
- Definice okruhu a příklady: ℚ, ℤ, ℤm a ℚ[x].
Invertibilní prvky komutativního monoidu tvoří pod-monoid, který je grupou. V případě (multiplikativní
části) okruhu ℤm se tato grupa nazývá Eulerovou grupou čísla m
a značí se Φ(m). Například nosná množina grupy Φ(15) je {1,2,4,7,8,11,13,14}.
- 5. března 2024
- Eukleidův algoritmus pracuje v polynomiálním čase. Monoidy a inverzní a invertibilní prvky v nich.
Cvičení. Je-li na množině {0,. .,14}
operace ∗ definována předpisem x∗y = Mod(xy,15),
které prvky jsou invertibilní? Uvažujte (nekomutativní) monoid všech funkcí
z tříprvkové množiny {a,b,c} do sebe.
Je funkce {[a,a],[b,a],[c,b]} invertibilní?
Je {[a,c],[b,a],[c,b]} invertibilní?
- 27. února 2024
- Vlastnosti relací obecně, vlastnosti relace dělitelnosti. Na
∀x(x ∣ 0)
a ∀x∀y∀z(x ∣ y → (x ∣ y+z ≡ x ∣ z)) lze založit ověření,
že Eukleidův algoritmus správně počítá úlohu GCD, tj. že k libovolným dvěma
číslům nalezne jejich největšího společného dělitele. Ale lze uvažovat i opačným směrem a z korektnosti
Eukleidova algoritmu odvodit čistě matematický poznatek: ke každým dvěma číslům existuje jejich
společný dělitel, který je dělitelný všemi jejich (ostatními) společnými děliteli.
- 20. února 2024
- Úloha a algoritmus jako základní pojmy teoretické informatiky. Časové nároky
algoritmů. Školní algoritmus pro úlohu Mult pracuje v kvadratickém čase,
školní algoritmus pro sčítání dokonce v lineárním čase. Pro algoritmy, které pracují v linárním,
kvadratickém, kubickém atd. čase máme souhrnný název polynomiální algoritmy. Úlohou, pro
kterou polynomiální algoritmus neexistuje, je pravděpodobně Factoring, čili
úloha nalézt prvočíselný rozklad daného čísla. Ale dokázané to není, nalezení důkazu je otevřeným
problémem. Dva algoritmy, který bychom dostali modifikací těch algoritmů pro
úlohu Primes, které byly uvedeny v přednášce, pracují v exponenciálním čase,
takže polynomiální rozhodně nejsou.
Huge number calculator
The calculator BNCalc.pdf is implemented
as a (set of scripts behind a) pdf document and can be used for operating with
really huge integers. Note that there are some undocumented key combinations
that make it easier to repeat the given operation.
The "result" text field in the "Factoring" page, marked by an arrow in this
image, accepts Shift‑M (or Shift‑B with the same
meaning).
Also, the result text field on the preceding page accepts Shift‑M and Shift‑B.
Incompleteness and Gödel Theorems
Here is an (updated May 2nd, 2024) list
of exercises.
Exams (Czech)
Please be ready to discuss any of the 14 exercises. However, the exam requirements end with the proof
of Löb's theorem. Further consultation and exam days (other than given in SIS) are possible.
Course contents in Spring 2023/24
- May 16th, 2024
- Solovay's completeness theorem for GL: a modal formula A is provable in GL
if and only if it is a PA-tautology. We did not discuss the completeness of another logic,
sometimes denoted by GLS. It is complete with respect to ℕ-tautologies, and the
proof is very similar and is also contained in Solovay's paper.
- May 14th, 2024
- Soundness of GL w.r.t. Kripke semantics (finished). The proofs of completeness and of finite
model property are skipped. However, they have a clear consequence: GL is decidable. A plan for
the next talk is Solovay's arithmetic completeness proof: a finite Kripke counterexample for
a modal formula A can be converted to an arithmetic counterexample, i.e. to an arithmetic
valuation ∗ such that PA ⊬ A∗.
- May 7th, 2024
- Two variants of the substitution theorem are provable in K4. An application of GL in
metamathematics: a solution of a Gödelian self-reference equation (like Gödel's, Henkin's
or Löb's sentence) is uniquely determined. A sentence is obtained by Gödelian self-reference
if the claim it says about itself can be expressed using the formula Prπ(x),
which can be nested, parameters, and nothing else. However, a general unique solvability theorem
is not true. This is clear from some exercises. Kripke semantics for GL: it is sound w.r.t. the
class of all transitive and reversely well-founded frames (to be finished). Some connections of
reverse well-foundedness and irreflexivity: a well-founded frame is irreflexive, and a finite
transitive and irreflexive frame is reversely well-founded.
- May 5th, 2024
- Logic GL can be defined by two equivalent ways, as the extension of K4 by Löb's rule, or
the extension of K4 by Löb's axiom scheme. The latter is preferable in the literature.
- May 2nd, 2024
- An alternative proof of Löb's theorem. Modal formulas, PA-tautologies and ℕ-tautologies.
Modal logics K and K4. Löb's rule and Löb's axiom scheme.
- Apr 25th, 2024
- As we know, if T and τ(z) are as usual, then (T+Con(τ))
can prove the unprovability of the sentence Con(τ). However, (T+Con(τ))
cannot prove the independence of the sentence Con(τ). This is an example on the situation where
Gödel's second theorem works as a technical tool used in some proof. Henkin's question concerning a self-referential
sentence asserting its own provability. Löb's solution: all such sentences are provable.
- Apr 23rd, 2024
- Some connections to Gödel's second theorem. First, Paris and Harrington and some other authors
exhibited sentences that are independent of PA and speak about numbers, not about formalized logic.
There is a link from these results to Gentzen who considered the question what arithmetic axioms,
if added to PA, make it possible to prove the consistency of PA. Second, reasoning about self-referential
sentences can be simulated in modal logic, and modal logic even has some applications in that reasoning.
And third, most philosophers agree that Gödel's result in fact refutes Hilbert's program, but the
opposite opinion and further considerations are still possible. While PA cannot prove its own
consistency, some consistency proofs in PA are possible. For example,
PA ⊢ Con(∅).
- Apr 18th, 2024
- Gödel's second incompleteness theorem. It is often cited as follows: no sufficiently strong recursively
axiomatized theory can prove its own consistency. More exactly, if τ(z) is Σ
and defines T (in which case T must be recursively axiomatizable), and T
is consistent, then T ⊬ Con(τ). In particular,
PA ⊬ Con(π) where π is the natural definition of PA in ℕ.
- Apr 16th, 2024
- The self-reference theorem. Formalized Σ-completeness theorem. Gödel's self-referential
sentence asserting its own unprovability.
- Apr 11th, 2024
- The formulas Prτ(x) and Con(τ). Facts about formalized
provability and formalized consistency provable in PA. Löb's derivability conditions.
- Apr 9th, 2024
- Formulas describing further syntactic notions. They can be used to write down a
formula Proofτ(x,w) containing a formula τ(z)
as a subformula. If τ(z) is Σ or Δ0, then
Proofτ(x,w) is PA-equivalent to a Σ1-formula (that is,
is Σ1(PA)), or is Δ0 respectively. If τ(z)
defines T, then Proofτ(x,w) defines the set of all
pairs [φ,m] such that m is a proof of φ in T.
- Apr 4th, 2024
- String functions in PA. Formulas Var(v) and Term(t). They express the property
"the number v is a variable" and "the number t is a term",
respectively, in the arithmetic language. Writing down the former
is straightforward (using Euclidean division and the exponential function), but defining terms
involves speaking about balanced strings and quasiterms. Both formulas are Δ0.
- Apr 2nd, 2024
- Formalization in arithmetic (arithmetization) of a notion involves finding a formula that defines
the notion in ℕ and proving in PA that the notion, if described by that formula, has
the expected properties. Notions formalizable in PA include primes (irreducibles), powers of two, Euclidean
division and the function NPB. Most of these notion are formalizable already in IΔ0.
The exponential function is formalizable, but the
sentence ∀x∃y(y=2x) is not provable
in IΔ0. It is not known whether the fact that there are infinitely many primes is
provable in IΔ0. If two formulas define the same set in ℕ, then they
are (of course) Th(ℕ)-equivalent, but they may be PA-inequivalent.
- Mar 26th, 2024
- Euclidean division in PA. The claim that there are infinitely many irreducible numbers (before we
prove that being irreducible is the same as being prime, we distinguish between the two notions) is expressible
in the arithmetic language. In fact the classical (Euclid's) proof is formalizable in PA, but is seems
adequate to avoid speaking about the factorial function and about the prime factorization of a number.
The fact that every nonzero number is the product of some irreducible numbers is objectionable since it is
an infinite disjunction and thus it is problematic to consider it a sentence.
- Mar 21st, 2024
- The relationship between the schemas LNP and Ind. A model showing that they are
not equivalent over Q.
- Mar 19th, 2024
- Peano arithmetic PA and provability in it: both operations are commutative and associative,
· is distributive over +, both cancellation rules hold, the strict order is transitive, irreflexive
and linear, the unstrict order relates to the strict order as expected, and also the interaction of the
order relations and the operations is as expected.
Homework. Using the fact that a consistent decidable theory has a complete decidable extension
show that a theory T is essentially undecidable (in the sense that every consistent
extension of T is undecidable) if and only if T is essentially incomplete
(in the sense that every recursively axiomatizable extension of T is incomplete).
- Mar 14th, 2024
- A finally finished full proof of Rosser's theorem: if T is any consistent recursively
axiomatizable extension of Q, then T is incomplete (if fact, already some
Σ1-sentences are independent) and undecidable (more than that, Thm(T)
and Ref(T) are recursively inseparable RE sets).
- Mar 12th, 2024
- An addendum to Gödel's 1st theorem: if T satisfies the assumptions, then
Thm(T) is Σ1-complete (in the sense that every RE set
is m-reducible to it). So it is one of the algorithmically most complicated RE sets. A finite
extension of a decidable theory must again be decidable. From this it follows that the set of all
logically valid arithmetic formulas is not decidable. Thus predicate logic is not decidable in general.
However, there are some special cases that are decidable. For example, if the language consists of
only finitely many unary predicate symbols. Rosser's theorem (to be finished or repeated): the
claim of Gödel's 1st theorem remains true if Σ1-soundness is replaced by mere
consistency.
- Mar 7th, 2024
- Since every RE set is m-reducible to Th(ℕ) and sets
in RE – Π1 exist, Th(ℕ)
is not Π1. Since the arithmetic hierarchy does not collapse
(sets in Σn – Πn
exist for every nonzero n), this argument can be repeated at every level n≠0:
Th(ℕ) is not Πn. The whole fact is cited as Tarski's theorem
on the undefinability of truth: arithmetic truth (the set of all formulas valid in ℕ)
is not arithmetical (is not in the union of all Πn, which equals the
union of all Σn; or put otherwise, no formula defines it in ℕ).
Gödel's 1st incompleteness theorem: if T is a Σ1-sound extension of Q,
then T is undecidable (and thus) incomplete. There exist independent sentences that are
as simple as Σ1 (or Π1).
- Mar 5th, 2024
- We know that if T is recursively axiomatizable, then Thm(T) is RE.
Craig's theorem (known as Craig's trick) says that the opposite is also true: if Thm(T)
is RE, then there exists a recursive is S equivalent to T.
If is T is recursively axiomatizable and complete, then it is decidable.
Therefore, SUCC, DNO and other theories from the Fall semester are decidable. All their models
(like ω + (ω* + ω) · ω)
are decidable structures. Any finite structure for a finite language is decidable.
If A ∈ RE – Δ1
and φ(x) is a Σ1-formula that defines it, then the equivalence
∀n(n∈A ⇔ φ(\bar{n})∈Th(ℕ)) shows that A ≤m Th(ℕ).
Thus ℕ is an undecidable structure.
- Feb 29th, 2024
- Course-of-values recursion and some examples on its use. (i) Hofstadter's function is recursive.
(ii) For every recursive function g of one variable such that Rng(g) is infinite
there exists a one-to-one recursive function f having the same range. This fact is
a key step in proving a characterization of RE subsets of N: a
set A ⊆ N is RE if and only if it is finite or
it is the range of some one-to-one recursive function. (iii) The set of all terms (in the arithmetic
language) is recursive. From this it is possible to continue to other syntactic notions (formulas,
free and bound variables etc.) and conclude that if T is recursive or RE,
then the binary relation "d is a proof of φ in T"
is recursive or RE respectively.
- Feb 27th, 2024
- A set A ⊆ N is m-reducible to a
set B ⊆ N, which we denote
by A ≤m B, if there exists a recursive
function f such that
∀n(n∈A ⇔ f(n)∈B).
If A ≤m B and B
is Σ1 (or Π1, or Δ1), then
A is Σ1 (or Π1, or Δ1
respectively). The function computing the number of primes less than n is clearly recursive, but it is not
known whether its graph is Δ0.
- Feb 22th, 2024
- The graphs of the
functions [x,z] ↦ zx
and [x] ↦ NPB(x) are Δ0-definable.
A function derived from a (partial) recursive function via primitive recursion must again be (partial)
recursive.
- Feb 20th, 2024
- The graph of the functions Div and Mod are Δ0-definable. Also the graph of the
function [x,z] ↦ zx is
Δ0-definable (to be finished).
Chapters in Classical Logic
About
A seminar partly based on students' presentations, devoted to various
topics in metamathematics, non-classical logics, and proof theory.
The topics usually include: Provability Logic,
independence of the Paris-Harrington combinatorial
principle over Peano arithmetic,
relations between ZF, GB and the Kelly-Morse set theories,
upper and lower bounds for cut-elimination in
classical predicate logic, decision procedures
for intuitionistic propositional logic.
Here is the list of topics (in Czech) in the academic year 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
- Smorynského článek Hilbert's Programme (Adam Fürstenzeller, od 14.12., 2 přednášky)
- Abstrakt (poskytnutý přednášejícím): Smoryńského článek popisuje situaci, ve které se matematika jako
vědecká disciplína ocitla na začátku dvacátého století. Mezi matematiky se vedly diskuse týkající se
formulování samotných základů této vědní disciplíny. Jednou z teorií byl intuicionismus, za jehož
zakladatele se považuje L. E. J. Brouwer, který ve své disertaci (1907) zformuloval základní myšlenky
tohoto směru. Intuicionisté odmítali aktuální nekonečno a využívání aristotelské logiky, zejména zákonu
vyloučení třetího, pro nekonečné objekty. Dalším rozšířeným směrem byl formalismus v čele s Davidem
Hilbertem. Hlavní myšlenkou formalismu je budování bezesporných axiomatických teorií — sad axiomů,
které úplně popisují danou matematickou teorii (věty a axiomy jsou pravdivé, když nejsou ve sporu se svými
důsledky — nemusí se nutně jednat o “evidentní” pravdy).
Názorová rozepře mezi Hilbertem a Brouwerem
je ústředním tématem celého článku. Smoryński důkladně popisuje jak osobní vztah hlavních dvou protagonistů,
tak i ohlasy, které jejich práce vyvolaly. Počátkem dvacátých let získává Brouwer nové stoupence. Jedním
z nich byl také H. Weyl, jehož přednáška z roku 1920 přiměla Hilberta znovu se plně věnovat práci
v oblasti základů matematiky. Společně se svými stoupenci se snaží dokázat bezespornost aritmetiky
(v širším smyslu, zahrnujícím i analýzu a teorii množin) — tzv. Hilbertův program. Ideový spor
mezi Hilbertem a Brouwerem se postupně přesouvá i do osobní roviny. Jeho vrcholem je vyloučení Brouwera
z Matematische Annalen, které inicioval Hilbert.
V průběhu dvacátých let 20. století předkládá
Hilbert rozpracované důkazy Ackermanna a Von Neumanna a zdá se, že důkaz bezespornosti aritmetiky a s ním
i dokončení Hilbertova programu je na dosah ruky. Zvrat však přináší rok 1931 a Gödelovy věty o neúplnosti.
V první z nich Gödel dokázal, že každá bezesporná rekurzivně axiomatizovatelná teorie obsahující aritmetiku
je neúplná (existuje v ní nezávislé tvrzení) a tím prokázal neuskutečnitelnost Hilbertova programu.
- Eckart Menzler-Trott: Logic's Lost Genius — The Life of Gerhard Gentzen (Timea Cochová, od 30.11., 2 přednášky)
- Zaoberali sme sa životným príbehom matematika a logika Dr. habil. Gerharda Gentzena. Od detstva, cez
štúdium a prácu až po jeho tragickú smrť v Prahe. Nahliadli sme k jeho práci a komunikácii
s matematikmi vtedajšej doby, ako boli napríklad Hilbert a Bernays. Z oficiálnych dokumentov,
spovedí blízkych, pracovných a osobných listov sa dozvedáme o jeho charaktere a sledovali sme rozvoj jeho
nápadov a práce. Taktiež sme si priblížili ako vyzerala veda a hlavne matematika a logika v nacistickom
Nemecku a v zvyšku sveta.
Ukážky niektorých listov a dokumentov:
PDF1,
PDF2.
- L. E. J. Brouwer: Life, Art and Mysticism (Šimon Pošta, 23.11., 1 přednáška)
- Brouwerův výchozí bod Smutného světa, role člověka jako individua a jako člena kolektivu, zásadnost
karmického řádu a jeho prohlédnutí skrze přivrácení se k sobě, druhy řečí, pravd a jejich vztah
k vědám, speciálně k logice a matematice. K tomu podrobnější
shrnutí.
- Detlefsenův článek z roku 79 (Timotej Šujan, od 2.11, 1.5 přednášky)
- Abstrakt (poskytnutý přednášejícím): Detlefsen v první části článku kritizuje takovou skeptickou
interpretaci (SI) Gödelovy druhé věty (G2), která by se snažila dojít ke skeptickému závěru, že víru
v konzistenci teorie T nelze odůvodnit důkazem sentence Con(T). Tvrdí, že tento
závěr z G2 žádným zřejmým způsobem neplyne, a tedy je potřeba dokázat určité pomocné předpoklady
SUP1 a SUP2. Následně se snaží ukázat, že platnost SUP1 vyvrací původní SI —
v jeho argumentu jsou ústřední pojmy jako reflexivní teorie
či (jeho vlastní pojem) epistemicky kompaktní teorie. V druhé části článku se snaží upravit SI tak,
aby unikla ze spárů jeho kritiky, avšak následně i takovou upravenou SI odmítá jako nepodloženou.
V třetí části krátce odmítá jako nepodloženou Resnikovu interpretaci G2 v kontextu
“nejsilnějšího/nejsložitějšího systému, který jsme ještě ochotní vážně zkoumat”, a to i kvůli
nejasnému popisu takového systému. V závěrečné části se pak snaží zachránit Hilbertův program tak, že
představuje tzv. omezené ω-pravidlo, které je dle něj v souladu s finitními metodami, které
Hilbertův program vyžaduje, a tvrdí, že např. Con(PA) je dokazatelné z PA+(ω-pravidlo).
- Gödelův článek z roku 1931 (L. Clowez, od 19.10., 2.5 přednášky)
- Kódování logické syntaxe, které je založeno na prvočíselných rozkladech přirozených čísel.
Definice kalkulu poměrně podobná dnešní definici kalkulu hilbertovského. Gödel pracuje s axiomatickou
teorií, která odráží takzvanou teorii typů. Viditelný rozdíl vůči dnešním přístupům je to, že nepracuje
s nějakým předem fixovaným jazykem. Pouze trvá na tom, že k dispozici jsou symboly pro nulu a následnickou
funkci. Článek pracuje s “rekurzívními” funkcemi, ale definici se shoduje s tím, čemu
se dnes říká primitivně rekurzívní funkce (dnes víme, že rekurzívní funkce lze ztotožnit s funkcemi
algoritmicky počitatelnými a je jich víc než primitivně rekurzívních). Jako celkem věrohodná tedy vypadá
historická hypotéza, že kromě vět o neúplnosti je článek důležitý také tím, že v něm byly zavedeny
primitivně rekurzívní funkce.
- Dnešní pohled na Gödelovy věty (V. Švejdar, 2 týdny)
- Trochu životopisných údajů ke Gödelovi. Ingredience důkazu jeho vět o neúplnosti: kódování syntaxe,
numerály, definovatelné množiny, Σ-formule a věta o Σ-úplnosti, predikát dokazatelnosti, věta
o autoreferenci.
Other activities
TeX/LaTeX, pdf, ...
FBUsersSetup
The Firebird SQL server comes with a command line utility
gsec
for manipulating database users. Using it, one can add, delete, or modify server's
users, where a modification practically means a password change.
FBUsersSetup.exe is written as an Inno Setup Windows
installer*)Unlike normal installers, it does not
write anything to the registry and does not leave any trace on your computer. So no
deinstallation is provided/needed.
and it basically is a gui wrapper for the gsec
utility.
As such, it has little additional functionality in comparison to gsec
.
However, it is easy to use, it can modify users on any computer in or outside the local network,
it never gets confused if there are parallel instances of Firebird running on the local computer,
and it can detect the properties of the local Firebird(s).
The utility is rather self-explanatory, the essential dialog pages being
- the selection
of a db server
On the local computer, TIGER, there are two parallel instances of Firebird.
One communicates through the standard port 3050, the other through port fb25 that translates
to 3060 in the services
file. The user can click on one of them in the listbox,
or say something else. Assume that, since he wants to modify users on the computer JUPITER where
Firebird communicates through port 3060, he deleted the text "TIGER" in the upper text field
and typed "JUPITER/3060" instead. In the two bottom text fields he has to specify the admin login.
In most cases, the admin would be SYSDBA. However, in Firebird 2.0 and later any user can
change his own password.
, and then
- a user action
The version of Firebird addressed as JUPITER/3060 is 2.5.2. Besides SYSDBA, there
are three other database users on that server. Since database user's first and last names are hardly ever needed,
FBUsersSetup somewhat misuses these data and codes the current time into them: JOSEPH and VIOLA
were inserted on Apr 14th, 2013. JASMIN was not inserted using FBUsersSetup and so her
first and last names are unknown. A new database user ADAM is now about to be inserted.
on that server.
DBUSubst
The utility DBUSubst.exe
can substitute one Firebird database user for
another. A substitution of user M for existing user D in a database
means that M becomes an owner of all database objects that user D owned,
he inherits all privileges that were granted to D, and he becomes a grantor
of all privileges that D granted. After being substituted out, user D
grants and is granted nothing, and owns no database object. If D was
an owner of a database then M becomes a new database owner.
Thus user substitution is a more general operation than database
ownership change.
Similarly as FBUsersSetup, DBUSubst.exe is written as a (harmless for
your computer) Inno Setup Windows installer. It basically is a wrapper for
the isql
command line utility and
some sql scripts. The scripts are available in DBUSubst.zip.
They are documented and thus contain a detailed information about the
substitution process. The document DBUSubst.pdf
contains some introductory information about the user privileges and some Firebird internals.
Two essential dialog pages of DBUSubst.exe are
- the database connection
Our database zoodata.fdb resides on a computer orel where
(the relevant instance of) Firebird communicates thru port 3060;
orel can be a computer in the local network or a
computer visible on internet. Of course, if it is not the local computer
on which DBUSubst is run, the browse button cannot be used; the path to zoodata.fdb
has to be typed.
When developing the database, we accessed it as a user LION.
This user is an owner of the database.
We also have another user VISITOR who is designed to have some restricted
access. Now when the database is about to be
deployed, it appears that the name LION was not wisely selected and that the
owner name should be ZOODBA. So we are about to substitute ZOODBA for LION.
ZOODBA already exists on the server in question, i.e. orel/3060.
with the NEW user's login, and then
- the login of
the dead
user
Since we were allowed to proceed to this dialog window, the login of
ZOODBA was verified against Firebird on orel/3060. It was also detected
that the version of this Firebird server is 2.5.1 and that the owner
of the database is LION, see the blue text labels in the bottom.
We are now selecting LION as the user who will be substituted by ZOODBA,
and we have to specify his password. The password of VISITOR is immaterial
for the current substitution process since VISITOR is not
a grantor of anything. However, if there were other users who
granted something to LION, further dialog windows asking about their
passwords would follow.
, i.e. the user who is to disappear.