Gaifman's theorem

The set of Gaifman is a set of the mathematical logic . It states that all the sentences of first order predicate logic in finite, relational structures can in a certain sense only make local statements. The sentence goes back to Haim Gaifman and dates from 1981.

introduction

Let it be a relational language of first order predicate logic. Relational means that the signature only consists of a finite number of relation symbols. Models or structures of this language are called structures. An important example is where is a two-digit relation symbol. A structure is then a set with a two-digit relation on as an interpretation of . Such structures are nothing more than graphs , meaning that the nodes are connected by an edge. ${\displaystyle L_{I}^{\sigma }}$ ${\displaystyle \sigma }$ ${\displaystyle \sigma }$ ${\displaystyle \sigma =\{R\}}$ ${\displaystyle R}$ ${\displaystyle \{R\}}$ ${\displaystyle G}$ ${\displaystyle R^{G}}$ ${\displaystyle G}$ ${\displaystyle R}$ ${\displaystyle R^{G}(a,b)}$ ${\displaystyle a,b\in G}$

The idea of ​​using the shortest paths between nodes as distances in graphs is transferred to general finite structures with universe and interpretation by going over to the so-called Gaifman graph . This graph has the node set and two different nodes are connected by an edge if and only if there is a relation with arity and elements with and , where the interpretation of is below . In short, they are connected by an edge if they are related to each other. The distance is then the length of a shortest path from to in the Gaifman graph. Using this distance, one can then define the r -ball um for and as follows : ${\displaystyle \sigma }$ ${\displaystyle {\mathfrak {A}}=(A,I)}$ ${\displaystyle A}$ ${\displaystyle I}$ ${\displaystyle G({\mathfrak {A}})}$ ${\displaystyle A}$ ${\displaystyle a,b\in A}$ ${\displaystyle R\in \sigma }$ ${\displaystyle s(R)}$ ${\displaystyle a_{1},\ldots ,a_{s(R)}\in A}$ ${\displaystyle R^{\mathfrak {A}}(a_{1},\ldots ,a_{s(R)})}$ ${\displaystyle a,b\in \{a_{1},\ldots ,a_{s(R)}\}}$ ${\displaystyle R^{\mathfrak {A}}}$ ${\displaystyle R}$ ${\displaystyle I}$ ${\displaystyle a,b\in A}$ ${\displaystyle d(a,b)}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle {\vec {a}}:=(a_{1},\ldots ,a_{n})\in A^{n}}$ ${\displaystyle r\in \mathbb {N} _{0}}$ ${\displaystyle {\vec {a}}}$

${\displaystyle B_{r}^{\mathfrak {A}}({\vec {a}}):=\{a\in A|\,\min _{i=1,\ldots ,n}d(a_{i},a)\leq r\}=\bigcup _{i=1}^{n}\{a\in A|\,d(a_{i},a)\leq r\}\subset A}$.

Note that neither the distance , nor the comparison , nor the natural number r are part of . Nevertheless, one can talk about the distance and the r -balls. More precisely there are formulas with ${\displaystyle d}$ ${\displaystyle \leq }$ ${\displaystyle L_{I}^{\sigma }}$ ${\displaystyle L_{I}^{\sigma }}$ ${\displaystyle \sigma }$ ${\displaystyle \delta _{r}(x,y)}$

${\displaystyle d(a,b)\leq r\quad \iff \quad {\mathfrak {A}}\vDash \delta _{r}(a,b)}$.

These are defined recursively as follows:

${\displaystyle \delta _{0}(x,y)\quad :=\quad x=y}$   d. H. Nodes with distance 0 are the same.

${\displaystyle \delta _{r+1}(x,y)\quad :=\quad \delta _{r}(x,y)\,\lor \,\exists z(\delta _{r}(x,z)\land (\bigvee _{R\in \sigma }\exists z_{1}\ldots \exists z_{s(R)}(Rz_{1}\ldots z_{s(R)}\land \bigvee _{1\leq i,j\leq s(R)}(z_{i}=z\land z_{j}=y))))}$

Because of the presupposed finiteness of , these are actually formulas. The definition of the edge relation in the Gaifman graph shows that they do what is required. So you also have ${\displaystyle \sigma }$ ${\displaystyle L_{I}^{\sigma }}$

${\displaystyle d(a,b)>r\quad \iff \quad {\mathfrak {A}}\vDash \neg \delta _{r}(a,b)}$.

Define for variables ${\displaystyle {\vec {x}}:=x_{1},\ldots ,x_{n}}$

${\displaystyle \delta _{r}^{n}({\vec {x}},y):=\delta _{r}(x_{1},y)\lor \ldots \lor \delta _{r}(x_{n},y)}$.

Apparently applies

${\displaystyle b\in B_{r}^{\mathfrak {A}}({\vec {a}})\quad \iff \quad {\mathfrak {A}}\vDash \delta _{r}^{n}({\vec {a}},b)}$,

that means one can also talk about the r balls in . ${\displaystyle L_{I}^{\sigma }}$

Local sentences

We will essentially define local formulas in that they are restricted to r -spheres in a sense to be specified here . First, we explain the relativization of a formula by restricting the quantifiers that appear in using the above accordingly, that is, we set recursively ${\displaystyle \varphi ^{B_{r}({\vec {x}})}({\vec {x}},{\vec {y}})}$ ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$ ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$ ${\displaystyle \delta _{r}^{n}}$

${\displaystyle \varphi ^{B_{r}({\vec {x}})}:=\varphi }$if is atomic. ${\displaystyle \varphi }$

${\displaystyle (\neg \varphi )^{B_{r}({\vec {x}})}:=\neg (\varphi ^{B_{r}({\vec {x}})})}$

${\displaystyle (\varphi \land \psi )^{B_{r}({\vec {x}})}:=\varphi ^{B_{r}({\vec {x}})}\land \psi ^{B_{r}({\vec {x}})}}$   and accordingly for . ${\displaystyle \lor ,\rightarrow ,\leftrightarrow }$

${\displaystyle (\exists z\varphi )^{B_{r}({\vec {x}})}:=\exists z(\delta _{r}^{n}({\vec {x}},z)\land \varphi ^{B_{r}({\vec {x}})})}$

${\displaystyle (\forall z\varphi )^{B_{r}({\vec {x}})}:=\forall z(\delta _{r}^{n}({\vec {x}},z)\rightarrow \varphi ^{B_{r}({\vec {x}})})}$

This is a recursive definition about the formula structure of the first-order predicate logic. The right-hand side of these definitions always use relativizations of already explained and more simply structured formulas.

The definitions are apparently designed so that

${\displaystyle {\mathfrak {A}}\vDash \varphi ^{B_{r}({\vec {x}})}({\vec {a}},{\vec {b}})\quad \iff \quad B_{r}({\vec {a}})\vDash \varphi ({\vec {a}},{\vec {b}})}$,

that is, satisfies the relativized formula if and only if the r -ball is a model for . ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle B_{r}({\vec {a}})}$ ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$

A formula is now called a local base formula if it has the shape

${\displaystyle \exists x_{1}\ldots \exists x_{n}\bigwedge _{1\leq i<j\leq n}(\neg \delta _{2r}(x_{i},x_{j})\land \varphi ^{B_{r}(x_{i})}(x_{i}))}$

has, where is a first order formula. This formula expresses that there are elements in every model that have a distance so that the r -spheres do not intersect, and that the property described by is local, more precisely that the r -sphere around each Element is a model for this property. ${\displaystyle \varphi =\varphi (x)}$ ${\displaystyle {\mathfrak {A}}=(A,I)}$ ${\displaystyle a_{1},\ldots ,a_{n}\in A}$ ${\displaystyle >2r}$ ${\displaystyle a_{i}}$ ${\displaystyle \varphi }$

After all, a formula is called local if it is a Boolean combination of local base formulas, that is, if it is composed of local base formulas. ${\displaystyle \neg ,\land ,\lor ,\rightarrow ,\leftrightarrow }$

Formulation of the sentence

Gaifman's theorem is:

If there is a finite relational signature, then every sentence in finite models is logically equivalent to a local sentence. ${\displaystyle \sigma }$ ${\displaystyle L_{I}^{\sigma }}$

Remarks

If the quantifier rank of the set , i.e. the maximum nesting depth of existential and universal quantifiers in this set is maximum , then the r -balls of the local basis sets appearing in Gaifman's theorem can also be chosen. ${\displaystyle L_{I}^{\sigma }}$ ${\displaystyle \leq k}$ ${\displaystyle k}$ ${\displaystyle r\leq 7^{k}}$

More generally, any first-level formula with free variables is logically equivalent to a Boolean combination of formulas of the form and local sentences. ${\displaystyle \varphi ^{B_{r}({\vec {x}})}}$

The Gaifman locality of the first-order predicate logic results from Gaifman's theorem . However, the estimate for the smallest that can be chosen for the local basis clauses in Gaifman's theorem is weaker than the estimates given in the textbook by Leonid Libkin given below or in the article on Gaifman locality . ${\displaystyle 7^{k}}$ ${\displaystyle r}$

Individual evidence

1. ^ Haim Gaifman: On local and non-local properties , Proceedings Herbrand Symposium, Logic Colloquium ´81, North Holland Verlag (1982)
2. ↑ Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory , Springer-Verlag 1999, ISBN 3-540-28787-6 , page 31
3. ↑ Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory , Springer-Verlag 1999, ISBN 3-540-28787-6 , sentence 2.5.1. Gaifman's theorem
4. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 4.22