Locality : A useful notion for proving inexpressibility in Finite Model Theory

This thesis discusses the notion of locality used in finite model theory to obtain results about the expressive power of first order logic. It turns out that the most commonly used Ehrenfeucht-Fraïssé games are also applicable over finite structures. However, we analyze with an example the need for simpler tools for finite structures due to the complex combinatorial arguments required while using EF-games. We argue that locality is such a tool, although the gap between games and locality is quite narrow as the latter is in fact based on the former. Intuitively speaking: locality of FO implies that in order to check the satisfiability of a FO formula over a finite structure, it is enough to look at a small portion of the universe (which will be called the neighborhood of a point). We discuss two commonly known notions of locality given by William Hanf and Haim Gaifman. We provide the original results of the authors and then their modified versions suitable for finite structures. We then show that first order logic over any relational vocabulary has both of these locality properties. In order to grasp the idea of locality we also include examples wherever required. Towards the end of the thesis we also discuss deficiencies and limitations of the two types of locality and possible solutions to overcome them. In the last section we also discuss locality of order-invariant first order formulas