Proponowany przedmiot jest kontynuacją Logiki dla Informatyków przeznaczoną dla studentów zainteresowanych teorią informatyki. Celem jego jest rozszerzenie podstaw wiedzy z zakresu logiki matematycznej i dziedzin pokrewnych o narzędzia potrzebne do zaawansowanych studiów w obszarach związanych z logiką i weryfikacją czy teorią języków programowania, bez wchodzenia w tematykę ściśle badawczą. W tym celu będziemy koncentrować się na podstawowych zagadnieniach trzech aspektów logiki matematycznej: algebry uniwersalnej, teorii dowodu i podstawach semantyki logik, z naciskiem na perspektywę i użyteczność w informatyce (w odróżnieniu od perspektyw matematycznej czy filozoficznej).
Przedmiot polecamy dla zainteresowanych studentów wyższych lat studiów I stopnia (_dobra_ ocena z LdI silnie wskazana); w szczególnych przypadkach może też być właściwy dla studentów II stopnia pragnących wyrównać pewne braki materiału (tu konkretne zasady do ustalenia w porozumieniu z dyrekcją — FS).
#### Program
1. Algebra Uniwersalna
1. Elementy teorii porządku. Kraty i punkty stałe.
2. Sygnatury i struktury
2. Homomorfizmy i kongruencje
3. Termy i algebry termów
4. Definiowalność równościowa
5. Teorie równościowe. Twierdzenie Birkhoffa
6. Algebry wolne i indukcja
7. Algebra a wiązanie zmiennych (?)
2. Teoria dowodu
1. Dowody jako obiekty
2. Dedukcja naturalna
3. Rachunek sekwentów
4. Dopuszczalność cięcia i normalizacja
5. Przypisanie termów i postaci kanoniczne (?)
6. Kwantyfikacja
7. Logiki substrukturalne (?)
3. Podstawy semantyki logik
1. Modele rachunku zdań. Poprawność i pełność.
2. Intuicjonizm i klasycyzm. Algebry Heytinga i algebry Boole'a.
3. Modele logiki pierwszego rzędu: interpretacja kwantyfikatorów.
4. Twierdzenie Skolema-Löwenheima
5. Twierdzenia Gödla i niezupełność arytmetyki
