Finite Model Theory

---

Finite Model Theory studies the expressivity of logics on finite models.

Model theory has its origins in computer science where most objects of interest are finite.

A lot of tools (like compactness) have an inherent “infiniteness” about them which makes then useless, or at least very hard to use for finite models, hence unique tools need to be developed for finite model theory.

---

Notes

EF Games

• Connectivity is not FO Definable
• Connectivity is not FO definable for Finite Graphs
• Ehrenfeucht-Fraïssé Game
  • Partial Isomorphism
  • Rank-k Types (FO)
  • Ehrenfeucht-Fraïssé Theorem
  • Ehrenfeucht-Fraïssé Games Proof
• Even is not FO-definable for Linear Orders

Locality Theorems

• Locality
  • Gaifman Graph
  • Neighborhood
  • Local Equivalence
  • Isomorphism Types of Models
  • Hanf-Locality
    • Graph Connectivity is not Hanf-Local
    • Local Equivalence Lemma
    • FO Queries are Hanf Local
  • Gaifman-Locality
    • Hanf-local Queries are Gaifman-local
• Bounded Number of Degrees Property
  • Degree of a Structure
  • Gaifman-Locality implies BNDP
  • Bijective Ehrenfeucht-Fraïssé Game
    • Lemma for BEF Games
• Gaifman Theorem
• Threshold Equivalence
  • Lemma for Threshold Equivalence
• Extending FO
• Invariant Queries
• Order Invariant FO’
  • Even Atoms in Boolean Algebras
    • Definablity of Even Atoms

Descriptive Complexity of FO

• Encoding Finite Model
• Complexity of FO
  • Data Complexity of a Logic
  • Expression Complexity of a Logic
  • Combined Complexity of a Logic
• Boolean Circuits
  • AC0
  • FO(All)
  • FO(All) is in AC0
• FO(+, *)
  • BIT is expressible in FO(+, *)
  • + is epxressible in FO(BIT, <)

Second Order Logic

• Second Order Logic
• Fragments of Second Order Logic
  • Monadic Second Order Logic
• Ehrenfeucht-Fraïssé Game for MSO
  • Rank-k m,l Types MSO
  • Even is not MSO-expressible
  • Even is (MSO + <)-expressible
• l,k Ajtai-Fagin Game for EMSO
• Connectivity is not EMSO definable but is AMSO
• Strings in Logic
  • MSO formulas on Infinite Words accept Omega Regular Languages
  • MSO on Finite Words accept Regular Languages
  • FO on Finite Words accepts Star Free Languages

Tree Automata

• Ranked Trees in Logic
  • Ranked Tree Automata
• Unranked Trees in Logic
  • Unraked Tree Automata
• Trees (Automata Theory)
• Regular Tree Languages

Descriptive Complexity of MSO

• Encoding Finite Model (Same as FO)
• MSO has Problems in each PH level
• Complexity of MSO
• Complexity of MSO over Bounded Tree-Width Structures
  • Tree Decomposition
    • Tree Decomposition Lemma 1
    • Tree Decomposition of k-connected Graphs
  • Tree Width
  • Small Tree Decomposition
    • Small Tree Decompositions are Small
    • Tree Decomposition and Size of the Tree

Turing Machine Encodings

• Finitely Satisfiable and Valid Sentences
• Trakhtenbrot’s Theorem
  • Trakhtenbrot’s Encoding of Turing Machine
  • Decidability of Finitely Satisfiability and Validity
• Fagin’s Theorem
  • Logic L capturing the complexity class K

Fixed Point Logics

• Fixed Point Logics
  • Monotone, Inflationary and Inductive Functions
  • Fixed Points
  • Expressing Transitive Closure with Fixed Points
  • Monotonicity is Undecidable
  • Positive Formulas
  • Examples
    • Acyclicity of Graphs
    • Arithmetic Operators
    • Games of Graphs with Fixed Points
• Simultaneous Fixed Points
  • LFPsimult = LFP
• Stages
  • Stage Comparisons
• Gurevich-Shelah’s Theorem
• Immerman–Vardi’s Theorem

Counting Logics

• FO with Counting
  • Examples of FO(Cnt)
• FO with Infinitary Connectives
• L_infty,omega star : ${\mathcal{L}}_{\infty \omega }^{\ast }$
• Game for Counting Logic
• Counting and Locality
• Complexity of FO(Cnt)All
• Order Invariant FO(Cnt) is not Gaifman Local

Finite Variable Logics

• Paths on Graphs and Finite Variable Logics
• Finite Variable Logics
• Fixed Point Logics are subsumed by Finite Variable Logics
• Pebble Games

---

MOCs

• Logic
• Complexity Theory
• Logic, Automata and Games

---

Practical Information

• Professor: Narayan Kumar
• Timings: 9:10 am on Tue and Thu
• Location: LH1

---

References