Studentsky logicky seminar - drivejsi program
(Student logic seminar - past program)

Letni semestr 06/07: Teorie konecnych modelu (Finite model theory)

Pro ilustraci, prehledovy clanek R.Fagina, skripta J.Vaananena a M.Otta). Toto bylo doplneno prednaskami hostu: Neil Thapen (prednaska Resolution and pebbling games) a Pavel Pudlak (prednaska Resolution proofs and games).

Zimni semestr 07/08: Studium clanku
Dana Scott, A proof of the independence of the continuum hypothesis, Mathematical Systems Theory, 1, (1967), str.89-111.

Toto je jeden z nejkrasnejsich prehledovych clanku v matematicke logice vsech dob. Byl napsan pro matematiky bez prupravy v matematicke logice a je dostupny i matematickym zacatecnikum. Predklada dukaz, ze tzv. Hypoteza Kontinua (tez jeden ze slavnych Hilbertovych problemu) neni dokazatelna v teorii mnozin.

Letni semestr 07/08: Omezena aritmetika (Bounded arithmetic)

Omezena aritmetika je souborny nazev pro skupinu teorii (formalne podteoriich Peanovy aritmetiky). Tyto teorie matematicky podchycuji neformalni pojem "feasible reasoning", podobne jako pojmy (pravdepodobnostni) polynomialni algoritmus ci log-space algoritmus (a rada dalsich) formalizuji pojem "feasible computation". Literatura.

Paralelne s timto tematem oragizoval student p.Jan Pich dalsi studium literatury o konecne teorii modelu, zejmena skripta M.Otta - viz informace o letni semestru 06/07 vyse (ucast na tomto drivejsim seminari neni podminkou).

Zimni semestr 08/09: Booleovska slozitost (Boolean complexity)

Radu otevrenych problemu v teorii vypocteni slozitosti (vcetne tzv. P vs. NP problemu) lze redukovat na ukol dokazat vhodny spodni odhad na velikost obvodu pocitajici konkretni funkci. Potrebne odhady neumime zatim dokazat pro obecne obvody, ale pouze pro obvody splnujici dodatecna omezeni (konstatni hloubky, monotonni a pod.). Toto tema je jednou z fundamentalnich souvislosti mezi logikou a teorii vypocetni slozitosti. Literatura.

Letni semestr 08/09: Slozitost resoluce (Complexity of resolution)

Resoluce (vyrokova) R je jednoduchy a elegantni dukazovy system pro dokazovani nesplnitelnosti CNF formuli. Jeji verse jsou v zaklade (primo ci neprimo) mnoha systemu pro automaticke dokazovani.

V seminari se budeme zabyvat tzv. "dukazovou slozitosti" resoluce. Obecnym cilem dukazove slozitosti je porozumet slozitosti dukazu (merene zejmena jejich delkou) v ruznych dukazovych systemech. Delky dukazu odpovidaji casu nedeterministickych algoritmu. Dukazova slozitost je tak dalsim z temat spojujicich matematickou logiku a teorii vypocetni slozitosti.

Resoluce je jednim z nejlepe prozkoumanych systemu a lze se na ni naucit radu metod vhodnych i ke studiu silnejsich systemu.
Podivame se zejmena na nektera temata z nasledujiciho seznamu (dle casu): obecne cile dukazove slozitosti, delka, sire a prostor dukazu v R a jejich vztah, spodni a horni odhady na delky dukazu v R, tzv. feasible interpolation pro R, souvislost prostoru s oblazkovou hrou z t.konecnych modelu, kriteria pro spodni odhady v jazyce teorie modelu, ne-automatizovatelnost hledani kratkych dukazu, zesileni R: systemy R(k) a tzv. "rozsirena resoluce" ER, souvislosti s omezenou aritmetikou.
Literatura.

Zimni semestr 09/10: Teorie modelu usporadaneho telesa realnych cisel a o-minimalita (The theory of the ordered real closed field and o-minimality)

Eliminace kvatifikatoru pro RCF a jeji dusledky pro definovatelne mnoziny. O-minimalita a jeji obecne dusledky.
Literatura.
( Nektere vety jsou obtizne a museji je prednaset dva studenti soucasne.)

Host: 12. a 19.10.2009 Lou van den Dries (U. of Illinois, Urbana)

Letni semestr 09/10: Teorie modelu telesa komplexnich cisel aneb uvod do geometricke teorie modelu (The theory of the field of complex numbers and the introduction to geometric model theory)

Toto je zaklad moderni teorie modelu. Eliminace kvatifikatoru pro ACF a jeji dusledky pro definovatelne mnoziny. Minimalita a jeji obecne dusledky. Pregeometrie a geometrie minimalnich struktur. Literatura.

Zimni semestr 10/11: NP vyhledavaci problemy (NP search problems)

NP vyhledavaci problem je dan polynomialne rozhodnutelnou relaci R(x,y), ktera ma tu vlastnost, ze pro kazde x existuje y (delky polynomialne omezene v delce x) t.z. plati R(x, y), tzv. reseni pro x. Ukolem je ze vstupu x nejake reseni y spocitat. Rada prirozenych uloh v diskretni matematice ma tuto formu.

Slozitost NP vyhledavacich problemu je mozne porovnat s pouzitim pojmu polynomialni simulace. Rada problemu a vzajemnem vztahu ruznych prirozenych NP vyhledavacich problemu je otevrena a napr. neni znamo, jestli existuje uplny problem.

NP vyhledavaci problemy hraji i vyznamnou roli v logice (omezena aritmetika a dukazova slozitost).

Hoste:
Neil Thapen: Game induction search problems (25.11.2010)
Pavel Pudlak: Feasible incompleteness thesis (sekce 3), ( 9.12.2010)

Literatura.

Letni semestr 10/11: Gödelovy vety a slozitost (Godel's theorems and complexity)

Gödelovy vety o neuplnosti jsou fundamentalnim poznatkem o zakladech matematiky a mely a maji radu konkretnich dusledku v matematicke logice a v informatice. Existuji i jejich kvantitativni verse, ktere misto o existenci ci neexistenci dukazu hovori o existenci ci neexistenci dukazu nejak omezene velikosti.

Formalni dukazy jsou uzce svazany s vypocty a tak neni prekvapenim, ze tyto kvantitativni verse jsou relevantni pro teorii vypocetni slozitosti. Jedna plausibilni (ale dosud nedokazana) kvantitativni verse druhe Gödelovy vety o neuplnosti implikuje, ze tridy vypocetni slozitosti P a NP jsou ruzne (to je fundamentalni otevreny problem).

Literatura.

Zimni semestr 11/12: Open problems in logic & complexity

This semester the seminar was a part of the programme of the Special semester in Logic & Complexity that run from 19.September until 18.December. It was open to all students even if they did not took part in other special semester activities. Program.

Letni semester 11/12: -

Seminar se tento semestr nekonal - byl jsem v Cambridge.

Zimni semester 12/13: Nestandardni modely aritmetiky (Nonstandard models of arithmetic)

Jednou ze zakladnich vlastnosti logiky prvniho radu (predikatove logiky) je kompaktnost, jejimz dusledkem je existence tzv. nestandardnich modelu. Obecne se takovym modelem mysli kazdy model nejake teorie, ktery se lisi od jejich "zamyslenych" standardnich modelu. Napr. teorie konecnych teles ma i nekonecny model - nekonecne teleso, teorie usporadaneho telesa realnych cisel ma i model s infinitesimalne malymi cisly (to je zaklad tzv. nestandardni analyzy) a teorie usporadaneho okruhu celych cisel (tzv. aritmetika) ma i model s nekonecne velkymi cisly.

Prave na priklade aritmetiky lze demonstrovat radu vlastnosti techto nestandardnich modelu, zpusoby jejich konstrukci a jejich vyuziti v matematicke logice. I jen zakladni poneti o strukture techto modelu umoznuje lepe chapat radu pokrocilejsich temat ze vsech oblasti matematicke logiky.

Literatura.

Letni semestr 12/13: pokracovani tematu ze zimniho semestru (a continuation from the Winter semester)

Winter semester 13/14: Second order arithmetic

First order arithmetic studies the structure of natural numbers with the usual arithmetic operations in the context of first-order logic. One can talk about sets of numbers only as long as they are definable. A prominent theory used in this context is Peano arithmetic PA. It is mutually interpretable with the theory of finite sets.

Second order arithmetic approaches the structure of natural numbers together with the class of sets of natural numbers. One can talk directly about sets and, for example, quantify them in formulas. A prominent theory used in this context is Z_2 going back to Hilbert - Bernays. It lies somewhere between the theory of finite sets and set theory ZFC and a lot of mathematics can be formalized in it.

It has also several natural subtheories and H.Friedman showed that many basic theorems of various fields of mathematics are logically equivalent to one of just five such subsystems (this is called reverse mathematics).

The aim of the seminar was to learn some of the topics involved. We used S.Simpson's book "Subsystems of second order arithmetic".

Summer semester 13/14: Limits of finite structures

Model theory knows several constructions of infinite structures that can be interpreted as limits of classes of finite structures (e.g. ultraproducts, compactness arguments, non-standard analysis, amalgamation constructions, versions of forcing, asymptotic classes, pseudofinite structures, robust classes, etc.). These constructions are relevant to core parts of model theory as well as to its applications (e.g. the currently popular notion of "limits of graphs").

Obviously, we were not able to get to all topics listed on the literature page. We first read Vaananen's notes on pseudofinite structures and then parts of Goldbring's lecture notes on nonstandard analysis, including Chpts.15 and 16 on measure theory (Loeb's measure in particular) and a proof Szemeredi's regularity lemma using it. Finally we went through a nonstandard approach to the construction of Lovasz-Szegedy's limits of graph sequences, following Elek-Szegedy's paper (with some simplifications using facts well-known in nonstandard analysis).

Winter semester 14/15: Geometric model theory

At the heart of Geometric model theory lies the fact that the relation of definability (or some related notion) in certain first-order structures has formal properties analogous to various dependence relations (linear, algebraic,...) in geometry. Geometric approach can be then used to study, construct and classify first-order structures or, on the other hand, to make various geometric situations amenable to model-theoretic methods. This is the basis of some of the most remarkable applications of model theory during the last twenty years.

Our aim was to learn the basics on which one can base a later study of more advanced topics. During the winter semester we worked through the first four chapters of Zilber's notes "Elements of geometric stability theory" (see the literature page).

Summer semester 14/15: Geometric model theory

Continuation from the winter semester: we read some more from Zilber's notes and then most of Scanlon's survey article "Diophantine geometry from model theory" 5(available via the literature page).

Winter semester 2015/16:

The seminar had a form of a reading group run by Igor Carboni Oliveira, a postdoctoral visitor from Columbia University. Information about papers covered is at Igor's seminar web page.

Summer semester 2015/16: Feasible complexity theory

Run by Igor C. Oliveira as a reading group (texts studied are listed there).

Winter semester 2016/17: Infinitary methods in complexity theory

Run by Michal Garlik and Igor C. Oliveira: topics and relevant literature studied.

Summer semester 2016/17: Models of bounded arithmetic

This was a follow-up on the previous semester: topics.

Winter semester 2017/18: Games in logic

A number of topics in mathematical logic can be conveniently introduced and studied using the language of game theory. Examples are: the Ehrenfeucht-Fraisse game related to elementary equivalence of structures or a game underlying Robinson's model-theoretic forcing, various games related to provability and validity in classical and non-classical logics, to witnessing of quantifiers and to complexity of proofs, set-theoretic games related to descriptive set theory, to large cardinals or to the axiom of determinacy, etc. Further examples offers Stanford encyclopedia of philosophy.

During the semester we studied the Student-Teacher game and Herbrand's theorem in universal theories, the determinacy of finite and infinite games and the axiom of determinacy, Conway's game and surreal numbers, Karchmer-Wigerson game and communication complexity, and Hintikka games and linguistic. Neil Thapen visited the seminar and gave a talk on a prover-adversary game and propositional resolution. Literature.

Summer semester 2017/18: Finite Model Theory

We looked at some very basic facts of finite model theory - model theory restricted to finite structures. This is a topic related also to combinatorics and complexity theory. From the texts listed in the Literature we used mostly Vaananen's lecture notes.

Winter semester 2018/19: Logic and Computational Complexity

Many central notions and problems of computational complexity theory have their origins in mathematical logic. We looked at some basic examples (see the literature page).

Summer semester 2018/19:
Dana Scott, A proof of the independence of the continuum hypothesis, Mathematical Systems Theory, 1, (1967), str.89-111.
See the literature page for the pdf and some notes.

This is one of the most beautiful expository papers in mathematical logic ever written. It aims at mathematicians without any mathematical logic background and it discusses a fundamental mathematical problem and deep ideas that went into answering it.

Winter semester 2019/20: Peano Arithmetic

This is a central theory of mathematical logic and in its study basic notions and results from many parts of mathematical logic are used (proof theory and Godel's theorems, recursion theory and definability, set theory and model theory and models of PA, etc.). PA can be studied at an introductory level but it can also lead to advanced topics. Knowing PA to some extent is a prerequisite for understanding a number of logic areas.
Literature and some notes.

Summer semester 2019/20

The original plan was to study Bounded arithmetic. This is a collective name for a class of theories, subtheories of Peano arithmetic. These theories are mathematical models of the informal notion of "feasible reasoning", similarly as notions like (probabilistic) p-time algorithms or log-space algorithms (and some other computational models) formalize the notion of "feasible computation".

However, the corona-virus break interfered and we changed the topic to "Pigeonhole principle in bounded arithmetic" which we studied by working through a series of problems. PHP was equally stimulating for this part of mathematics as was Continuum Hypothesis for set theory, and there are still some outstanding open problems.

Winter semester 2020/21: Topics in Boolean complexity

Boolean complexity is concerned with the question how hard it is to define various Boolean functions by propositional formulas or circuits (or other devices) and, in particular, how large these need to be. The fundamental problem (linked with such notorious problems as is the P vs. NP problem) is to exhibit an explicit Boolean function which is hard to define.

We looked at some basic background and then at few topics that have a common facet with logic or are relevant in proof complexity. Meetings were via zoom due to the ongoing coronavirus pandemic. The particular topics and talk sequence page.

Summer semester 2020/21: Games in Logic

A number of topics in mathematical logic can be treated using the framework of game theory. Examples are: the Ehrenfeucht-Fraisse game related to elementary equivalence of structures or a game underlying Robinson's model-theoretic forcing, various games related to provability and validity in classical and non-classical logics, to witnessing of quantifiers and to complexity of proofs, set-theoretic games related to descriptive set theory, to large cardinals or to the axiom of determinacy, etc. Further examples offers Stanford encyclopedia of philosophy.

Actual topics studied are on the lecture page, that also offers links to relevant literature and slides used during the talks.
The seminar was still online via zoom, thanks to the corona-virus.

Winter and summer semesters 2021/22: Modern formalization of mathematics

All contemporary mathematics can be formalized in set theory (extended by some axioms in few exceptional cases) and, in fact, large parts in much weaker formal theories. It can be thus reduced, at least in principle, to manipulations with finite strings of symbols according to few mechanical rules which a computer can learn. A natural question is then whether one can use computers to find proofs of statements of interest or perhaps even to find interesting theorems on its own. However, automatization of mathematics runs into obstacles presented by some fundamental theorems of mathematical logic (e.g. the algorithmic unsolvability of the Entscheidungsproblem) and by some fundamental conjectures of complexity theory (e.g. that P differs from NP).

A more modest goal is to use a formalization to verify existing proofs. History of mathematics knows many famous theorems with original incorrect proofs as well as many famous people making errors. During the last half a century some parts of mathematics became so technically involved that many proofs and constructions are not really properly checked, and a number of people are getting worried about this situation. More about this topic can be found in papers

J.Avigad and J,Harrison, Formally verified mathematics, Communications of the ACM, April 2014, Vol. 57 No. 4, Pages 66-75, (online or pdf)

J.Avigad, The mechanization of mathematics, Notices of the AMS, 65(06):681-690, 2018 (pdf).

This year we looked at the formalization that is used in the formal verification Xena project and tried to understand how it works and how it relates to the usual formalization using first-order logic and set theory. We studied the textbook "Theorem Proving in Lean", complementing this by presentations about type theory and formal logic - all these sources (as well as slides of talks) are at the
Sources, schedule and slides page.

Both semesters of 2022/23: Proof theory basics

Proof theory is one of classical areas of mathematical logic originating from D.Hilbert's work on the foundations of mathematics and featuring such basic topics as Herbrand's theorem, Godel's Incompleteness Theorems, Gentzen's sequent calculus and natural deduction, ordinal analysis of proofs, non-classical logics, etc. It is also the area of mathematical logic which has most applications in CS and these connections stimulate many of recent developments.

Winter semester 2023/24: Formal proofs and their lengths

I had (a form of) a sabbatical and the seminar was run by my students Ondra Jezil and Mykyta Narusevych.
A link to their site with all relevant info:

https://yellowinastrip.github.io/student-logic-seminar/archive/winter23-24/index.html/

Summer semester 2023/24: Bounded arithmetic and witnessing theorems

Ondra and Mykyta continued to organize the seminar:
https://yellowinastrip.github.io/student-logic-seminar/archive/summer23-24/index.html