**Wstęp.**
(Skończona) teoria modeli jest istotnym obszarem logiki matematycznej, który, z naszej perspektywy, stanowi fundament teorii relacyjnych baz danych.
Zajęcia będą dotyczyć wybranych tematów z klasycznej i skończonej teorii modeli, które uznałem za interesujące i/lub ważne. Skupiać się będziemy na zrozumieniu jak pokazać, że danego zapytania nie da się wyrazić w logice pierwszego rzędu oraz na klasycznych własnościach fragmentów logiki pierwszego rzędu. Wykład będzie raczej teoretyczny.
Zajęcia są przeznaczone dla studentów zainteresowanych informatyką teoretyczną i matematyką. Niemniej jednak, powinny być dostępne dla studentów po pierwszym roku studiów.
Dla studentów zainteresowanych prowadzeniem badań lub pisaniem pracy dyplomowej na pokrewne tematy, zajęcia będą dobrą okazją by coś wspólnie porobić.
**Program wykładu.**
Wykład będzie zawierał:
1. Wprowadzenie + kilka przykładów. Twierdzenie o zwartości z dowodem za pomocą twierdzenia Gödel'a. Niektóre konsekwencje twierdzenia o zwartości z zastosowaniem do niewyrażalności w FO.
2. Niektóre ważne właściwości teoretyczno-modelowe FO: interpolacja Craiga, projektowa definicjalność Betha, twierdzenie zachowania Łoś-Tarskiego, twierdzenie o zachowaniu homomorfizmu.
Trochę o niepowodzeniach powyższych twierdzeń w świecie skończonym.
3. Prawo zero-jedynkowe FO, tj. właściwość FO polegająca na tym, że prawdopodobieństwo spełnienia formuły pierwszego rzędu w losowej strukturze wynosi albo 0, albo 1. Niewyrażalność poprzez prawo zero-jedynkowe. Grafy Rado, granice Fraisse'a i trochę o omega-kategoryczności oraz kompletnych teoriach.
4. Gry Ehrenfeucht-Fraisse'a jako uniwersalna metoda wykazywania niewyrażalności w FO. Gry na porządkach liniowych, typy, równoważność back-and-forth. Dowód twierdzenia Fraisse'a. Omówimy również niektóre modyfikacje gier E-F, np. gry z kamieniami i gry MSO.
5. FO może wyrażać tylko lokalne właściwości. Lokalności Hanfa i Gaifmana, z dowodami. Zastosowania lokalności do niewyrażalności oraz konstrukcji meta-algorytmów dla zapytań z oceną parametrów stałych nad strukturami o ograniczonym stopniu.
Teoria modeli może sprawić, że formuły będą duże.
6. Logika modalna jako oswojony fragment FO. Twierdzenia charakteryzacyjne Van-Benthema i Rosena. Nieco teorii modeli logiki modalnej.
7. Logika pierwszego rzędu z niezmienniczym porządkiem, czyli kilka słów o pięknie skończonej teorii modeli. Czy istnieje logika dla PTime i jak logicy próbują wykazać, że P ≠ NP.
8. Twierdzenie Fagina, że problemy definiowalne w ESO są dokładnie tymi, które są rozstrzygalne w NP. Trochę o spektrach FO i poszukiwaniach logiki dla P.
Niektóre wykłady będą oparte na "Elements of Finite Model Theory" autorstwa Libkina (dostępne za darmo tutaj: https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf), notatkach wykładowych Martina Otto (https://www2.mathematik.tu-darmstadt.de/~otto/LEHRE/FMT16.pdf), książce "A shorter model theory" autorstwa Hedgesa i kilku najnowszych artykułach.
**Egzamin.**
Egzamin będzie ustny i wymagać będzie zaprezentowania wybranych twierdzeń z wykładu. Osoby z wysokimi ocenami z ćwiczeń będą zwolnione z egzaminu.
**Wymagania.**
Dobra ocena z logiki dla informatyków (i być może algebra), umiejętność pisania i czytania dowodów. Zacięcie teoretyczne. W razie wątpliwości napisz do mnie maila.
