Sylabus and reference k prednasce
Teorie konecnych modelu

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.