Logi s Capturing Lo al Properties

Well-known theorems of Hanf and Gaifman establishing lo ality of rst-order denable properties have been used in many appli ations. These theorems were re ently generalized to other logi s, whi h led to new appli ations in des riptive omplexity and database theory. However, a logi al hara terization of lo al properties that orrespond to Hanf's and Gaifman's theorems is still la king. Su h a hara terization only exists for stru tures of bounded valen e. In this paper, we give logi al hara terizations of lo al properties behind Hanf's and Gaifman's theorems. We rst deal with an innitary logi with ounting terms and quantiers that is known to apture Hanf-lo ality on stru tures of bounded valen e. We show that testing isomorphism of neighborhoods an be added to it without violating Hanf-lo ality, while in reasing its expressive power. We then show that adding lo al se ond-order quanti ation to it aptures pre isely all Hanf-lo al properties. To apture Gaifman-lo ality, one must also add a (potentially innite) ase statement. We further show that the hierar hy based on the number of variants in the ase statement is stri t