Locality (logic)

from Wikipedia, the free encyclopedia

Locality is a term from mathematical logic that can be used to show the limits of the expressiveness of certain logics. The basic idea is that certain logics such as first-order predicate logic can only describe local properties of structures , but other properties of such structures do not have this property of locality, so the latter cannot be formulated in this logic. A distinction is made between two types of locality, the hemp locality named after William Hanf and the Gaifman locality named after Haim Gaifman .

introduction

We consider finite structures like those of a graph . A graph consists of a finite set and a two-digit relation on this set. The existence of the relation means that there is an edge from to . The letter E is reminiscent of the English word edge for edge. So that graphs can in predicate logic of first order describing the signature of only the relation is so . We now ask the question, which properties of graphs can be expressed in first-order predicate logic. A simple example is:

  • “The graph is complete ” is expressed by
.

The investigation of paths in a graph is more interesting :

  • "There is a path from after length " is expressed by
  • "There is a path from after length " is expressed by
  • "There is a path from after length " is expressed by
  • "There is a path from after length " is expressed by

By continuing this chain in an obvious way, one obtains for each fixed one an expression which expresses the existence of a path from to length . There are no expressions of first-order predicate logic for other properties:

  • "There is a way from to ":?
  • "The graph is connected ":?

If one could express the existence of a path from to by an expression , then it would express the context. This does not seem to want to succeed, since one would have to allow paths of ever greater length and ultimately an infinitely long OR link. For any graph there can in fact be no -theorem that expresses the relationship. To see this, we expand the language by two constants and consider the infinite number of sentences

.

Every finite subset of these propositions contains only finitely many propositions of the form and therefore no propositions with a suitable, finite one . Therefore, this finite subset can be satisfied by the cyclic graph , if one interprets and through opposite points. According to the compactness theorem , the entirety of the above theorems would then be satisfiable and one would get a graph which is because of connected and has no path of finite length from to . This contradiction shows that there cannot be a sentence that expresses the context.

The application of the compactness theorem is unsatisfactory in this line of argument, because for this one must also allow infinite models. Since, as is well known, the finiteness of a model cannot be formulated in first-order predicate logic, it cannot be ruled out that there could be a proposition that expresses the relationship for finite graphs. To show that this is also not possible, we consider lengths of paths between two points as a notion of distance. This means that in a certain environment of lies. It now seems to be the case that expressions cannot, in principle, distinguish between points at arbitrarily large distances, i.e. are only capable of making local statements. The specification of these considerations leads to the locality concepts presented below, with which, among other things, the non-formulability of the relationship in the first-order predicate logic can be shown.

Properties of structures

As is well known, a structure for a signature consists of a set , the so-called universe of the structure, and an interpretation of each symbol . A k-place relation symbol is assigned a subset , that is, a k-place relation over the universe. If, as in the introduction above , there is a two-digit relation , a structure is nothing more than a graph. An isomorphism between structures is a bijective mapping between the underlying universes that preserves the interpretations of the structure. In the case of graphs, i.e. structures and , this simply means that the mapping, for example , is bijective, always follows from and that the same applies to the inverse mapping . If the structure has a constant symbol, for example , which is interpreted by or in the structures , then the preservation of the structure means nothing other than .

In the following, we are interested in k-ary properties that are invariant under isomorphisms. Such a property, also known as a query, assigns a subset to every structure , so that for every isomorphism it holds that .

An example of a 2-digit property of graphs is the transitive envelope , which assigns its transitive envelope to the edge relation .

For one sets . There are then only two possibilities for a 0-digit property, or what can then be interpreted as false or true . Instead of 0-digit properties, one speaks of Boolean properties. A typical example is the relationship between graphs: A graph has this property or not and this property is retained in the case of isomorphism.

If a logical expression with free variables is through

Given a k -place property, is the set of all tuples for which the expression in the structure becomes true. In the case of k = 0 this is again to be interpreted as false or true , then the property is defined by a sentence as a logical expression and instead of being written one also writes .

In the following the question arises as to which such properties cannot be defined by expressions of certain logics. This describes the limits of the expressiveness of such logics.

Gaifman graph

We consider signatures that only consist of relations, so-called relational signatures. Functions can be understood with their function graphs and thus also as relations, but with an arity increased by 1, constants can often be viewed as single-element, single-digit relations. In order to get the distance concept mentioned above, we assign a graph , the so-called Gaifman graph, to each structure of a relational signature . Its points are the elements from the associated universe . Two different points and are connected by an edge if and only if they are related to each other, more precisely if there is an n -digit and with and . It is the interpretation of the structure .

In the definition given in, all pairs are added to the Gaifman graph, which means that equality is treated like the other relations. As a result, a loop hangs at every point on the graph . The definition used here from the textbook by Ebbinghaus and Flum given below excludes exactly that, the Gaifman graph should be loop-free. This is irrelevant for the concept of distance to be introduced here.

If, for example, consists of a two-digit relation <and is , where the relation is interpreted as the usual size relation between natural numbers, then the complete graph is with points , because two different elements are related with respect to <, i.e. are comparable in size.

Another example is with a two-digit relation , so that every finite structure is a directed graph. The Gaifman graph is then the associated undirected, loop-free graph. This example is prototypical for the following considerations.

Spheres in Gaifman graphs

Since we have assigned its Gaifman graph to each structure , we can speak of the distance between two elements of the associated universe , we set

  = Length of a shortest path from to in ,

if the points are connected by a path at all, otherwise the distance is infinite. In particular we can speak of -spheres with respect to a tuple :

.

Since the distance can only assume integer values ​​or , it is sufficient to consider integer radii . The basic idea is to examine how far certain logical sentences of the logic under consideration extend with regard to this distance, which is specified below as hemp locality or Gaifman locality. For this reason we want to consider the relative structure on the spheres. Since we only have relations and no functions, this is simply the restriction of the relations . There are two things to keep in mind.

If the signature contains constants , it is not sufficient to regard these as single-digit, single-element relations, since the restriction to a subset of , i.e. the average with this subset, can be empty. However, substructures are required to contain the constants as well. In this case one has to go through the above definition

replace. This only turns out to be a technical addition to these considerations.

The points in the vicinity in the Gaifman graph are shown in green.

Second, we want to keep an eye on the centers to which distances are measured. To do this, we carry out a suitable constant expansion, that is, we add new constants , which are to be interpreted, and set .

At any -ball order we define the limited structure by

  • The universe is .
  • Every k -place relation is interpreted as.
  • Each constant is interpreted as.

Two structures with universes and and given tuples are called -equivalent, in characters

,

if there is a bijection , so that for each

.

Here stands for the vector extended by, that is , if , and exactly the same . The isomorphic relationship relates to -structures, so it is especially and . It is not required that a corresponding restriction of should be an isomorphism, but only that there should be some isomorphism between the -structures, but this applies because of the constants to be taken into account .

For there are no given tuples and . In this case, you simply write what it is the existence of a bijective mapping with all means.

Hemp locality

A -digit property of relational -structures is called hemp-local , if it exists, so that the following applies:

Are and structures, , with , as follows .

The smallest for which this applies is called the rank of the hemp locality and is denoted by. stands for the English term hemp local rank .

Two structures already agree with regard to the property if they agree with regard to all -balls of their Gaifman graphs.

Gaifman locality

A -digit property of relational -structures is called Gaifman-local if there is such that the following applies:

Is a structure and with follow as .

The smallest for which this applies is called the rank of the Gaifman locality and is denoted by.

Gaifman locality is the weaker term, the relationship exists . Note that gaifman locality refers to one structure, while hemp locality compares two structures.

Applications

In the applications it is first demonstrated that all properties defined by certain logical expressions are local to Hanf or Gaifman, but that certain properties do not meet this locality condition. It then follows that such a logical expression cannot describe what marks a limit of the expressiveness of the logic under consideration.

First order predicate logic locality

If one denotes with all logical expressions of the first-order predicate logic whose quantifiers have a nesting depth of at most , then applies

for all properties that can be defined by an expression.

FO stands as an abbreviation for the English term first order logic . Since every first-order predicate logic expression is an expression for some , all properties defined by first-order predicate logic expressions are hemp-local.

The graphs with environments shown in green , each in red

Relationship between graphs

Let it be the Boolean property of a graph, i.e. a structure, to be connected. In order to show that correlation cannot be formulated in the first order predicate logic even for graphs presupposed as finite, it suffices to show that hemp is not local. If hemp was local, for example with , then select and consider the cyclic graph with nodes and the graph that consists of the disjoint union of two cyclic graphs with each node. The Gaifman graphs of these structures are the graph itself. In each of these graphs , there is a -ball choice of a chain length with the center , and which are isomorphous with each other as a graph with all the given center. Each bijection (both graphs have nodes) therefore shows and follows from the assumed hemp locality . But that cannot be, because it is connected, but not.

Transitive envelope

Gaifman graph G for the successor relation , those shown in green and are the same as sets.

Now describe the transitive envelope of a -structure, that is, is the set of all pairs such that there are and with for all and . In order to show that the transitive envelope cannot be described by an expression of the first order predicate logic, it suffices to show that it is not Gaifman-local. If Gaifman were local, for example with , consider a chain with as a structure . Chain means that the relation is interpreted as. The transitive envelope of this relation is then nothing other than the natural order . The Gaifman graph is a linear graph of length . Based on the choice of , you can choose two nodes that are at the distance from the edges and the distance from each other . Then and both consist of two disjoint substrings of length with centers . It follows from this and from the assumed Gaifman locality would result . But that cannot be true , because of the relations and is exactly one true.

More logics

In the light of the above examples, the question arises whether there are extensions of the first-order predicate logic for which each expression also defines a local property. Such extensions would still not be expressive enough to describe graph connections or the transitive envelope in finite structures.

The universe of a finite structure can always be assumed to be linearly ordered. This order is denoted by <, it is not part of the signature. It can be shown that there are properties that are independent of this order, but that they can be described using this order. The set of these properties is called , that is , it is expanded by <and one then restricts oneself to properties that do not depend on <, which is indicated by the index inv (invariant). This gives a really larger set of properties (Gurewich's theorem) and it can be shown that every property is Gaifman-local (Grohe-Schwentick theorem).

Certain expressions of infinitary logics , which are expanded to include counting options, can also be detected as local to hemp or gaifman.

See also

Individual evidence

  1. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , definition 2.7
  2. Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory , Springer-Verlag 1999, ISBN 3-540-28787-6 , chapter 2.4
  3. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag 2004, ISBN 3-540-21202-7 , definition 4.1
  4. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , definition 4.2
  5. Grädel, Kolaitis, Libkin, Marx, Spencer, Vardi, Venema, Weinstein: Finite Model Theory and Its Applications , Springer-Verlag (2007), ISBN 978-3-540-00428-8 , definition 2.3.24, here has different the universe .
  6. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , definition 4.6
  7. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , definition 4.7
  8. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 4.11
  9. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 4.12
  10. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , page 48
  11. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , page 49
  12. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 5.2
  13. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 5.8
  14. ^ Leonid Libkin: Elements of Finite Model Theory , Springer-Verlag (2004), ISBN 3-540-21202-7 , Theorem 8.4