Citace na puvodni clanky lze najit v knize:
J.Flum - H.-D.Ebbinghaus:"Finite Model Theory", Springer, 1995.
1. prednaska:
Historicke motivace: prefixove tridy predikatovych formuli,
Trachtenbrotova veta, problem o spektru (Scholz'52/Asser'55).
Jazyk: relacni s konstantami. Priklady trid struktur: grafy
(orientovane i neorientovane), usporadani, grupy. Izomorfismus,
elementarni ekvivalence a elementarni vnoreni struktur.
Soucin a soucet struktur. Tridy struktur a globalni relace:
uzavrenost na izomorfismus.
Rozdily mezi klasickou t.modelu a t. konecnych modelu:
v. o uplnosti a v. o kompaktnosti. Dalsi priklady: Craigova
v. o interpolaci, Bethova v. o definovatelnosti, Robinsonuv
test bezespornosti sjednoceni dvou teorii (budou probrany v
5.prednasce).
DU:
(1) "Univerzalnost" grafu.
(2) Vztah izomorfismu a elementarni ekvivalence na konecnych
strukturach.
(3) Definovatelnost tridy souvislych grafu.
(4) Definovatelnost globalni relace "sude body v linearnim
usporadani".
2. prednaska
Izomorfismus a elementarni ekvivalence na konecnych strukturach,
atomicky diagram.
Kazda trida je axiomatizovatelna (nekonecnou) teorii.
Kvantifikatorovy rank qr formuli, m-ekvivalence
a postacujici podminka implikujici, ze trida konecnych struktur
neni konecne axiomatizovatelna.
Castecny izomorfismus struktur, souvislost s atomickym a s
otevrenym diagramem struktury.
Ehrenfeuchtova hra G_m(A,a,B,b); kazisvet K a duplikator D.
Vyhravajici strategie a izomorfismus struktur.
3. prednaska
Dukaz Ehrenfeuchtovy vety. Charakterizace konecne axiomatizovatelnosti
pomoci m-ekvivalence.
Priklady struktur, ktere nejsou izomorfni ale jsou
m-ekvivalentni: ruzna velka linearni usporadani, souvisle a nesouvisle
grafy (1 ci 2 cykly).
4. prednaska
Gaifmanuv graf G(A) struktury A, r-sfery ve strukture,
Hanfova veta.
Jerabkova ultraproduktova konstrukce s linearnimi
usporadanimi a se souvislymi/nesouvislymi grafy.
5. prednaska
Logika 2.radu SO, monadicka verse MSO. Souvislost neni
monadicka \Sigma^1_1, ale je SO. MSO-Ehrenfeuchtova hra MSO-G_m(A,B).
Nekonecne logiky L_{\infty,\omega} a L_{\omega_1, \omega),
a jejich ekvivalence na konecnych strukturach. Odpovidajici
Ehrenfeuchtova hra.
Logiky FO^s a nekonecne logiky s omezenym poctem promennych.
Odpovidajici Ehrenfeuchtova hra: oblazkove hry.
Logiky s kvantifikatorem pro velikost mnozin.
Neplatnost nekterych klasickych vet v konecnych modelech:
Bethova veta o definovatelnosti, Craigova veta o interpolaci,
veta, ze formule zachovavajici se do podmodelu jsou
univerzalni.
6. prednaska
Turingovy stroje, cas a prostor vypoctu. Tridy P a NP.
Konecne struktury jako vstupy do vypoctu. Kodovani vypoctu
relacemi na konecnych strukturach. Trachtenbrotova veta.
7. prednaska
Faginova veta: NP = \Sigma^1_1 definovatelne.
Znovu problem o spektru.
8. prednaska
Pevne body monotonnich operatoru, IFP (inflationary fixed
point). Priklad: komponenty souvislosti v grafu.
Logika FO[IFP] a deterministicky polynomialni cas.
Dalsi podobne operatory: PFP (partial fixed point),
TC (transitive closure), DTC (deterministic transitive
closure).
9. prednaska
AC^0 definovatelnost, preklad sentenci prvniho radu
na vyrokove formule, AC^0 posloupnosti vyrokovych
formuli.
Veta (Ajtai a Furst-Saxe-Sipser) o AC^0-nedefinovatelnosti
parity predikatu. Veta o castecnych restrikcich.
Reference na tuto vetu:
Boppana, R., a Sipser,M. (1990)
Complexity of finite functions. v: Handbook
of Theoretical Computer Science, ed.J. van Leeuwen,
str.758-804.
Uvod k 0-1 zakonum. Cisla L_n(L), L_n(K), l_n(K) a l(K).
Priklady: unarni predikat a 1 konstanta, unarni funkce,
formule 2.radu.
Pravdepodobnostni konstrukce konecne struktury. Axiom
(r+1)-rozsireni. Nekonecna spocetna nahodna struktura.
10. prednaska
0-1 zakon pro FO.
Parametricke sentence a tridy. 0-1 zakon pro parametricke tridy.
0-1 zakony pro typy izomorfismu (unlabeled). Notace
U_n(H|K), u_n(H|K), u(H|K). Rigidni struktury.
11. prednaska
Splnitelnost v konecnych strukturach. Godelova
trida prenexnich sentenci: UUE...E (U = univerzalni kvant.,
E = existencni kvant.).
Poznamka o FO^2 logice a nekolik protiprikladu.