Logics capturing local properties

Abstract. Well-known theorems of Hanf's and Gaifman's establishing locality of rst-order denable properties have been used in many appli-cations. These theorems were recently generalized to other logics, which led to new applications in descriptive complexity and database theory. However, a logical characterization of local properties that correspond to Hanf's and Gaifman's theorems, is still lacking. Such a characterization only exists for structures of bounded valence. In this paper, we give logical characterizations of local properties behind Hanf's and Gaifman's theorems. We rst deal with an innitary logic with counting terms and quantiers, that is known to capture Hanf-locality on structures of bounded valence. We show that testing iso-morphism of neighborhoods can be added to it without violating Hanf-locality, while increasing its expressive power. We then show that adding local second-order quantication to it captures precisely all Hanf-local properties. To capture Gaifman-locality, one must also add a (potentially in nite) case statement. We further show that the hierarchy based on the number of variants in the case statement is strict.