Transforming structures by set interpretations

TL;DR

This paper introduces finite sets interpretations, a new way to transform relational structures using WMSO formulas, and explores their expressive power on infinite deterministic trees, impacting automatic structures.

Contribution

It defines finite sets interpretations and analyzes their expressive power on infinite trees, linking decidability properties of WMSO and first-order theories.

Findings

Finite sets interpretations transform structures into new structures with finite set domains.

They preserve decidability from WMSO theories to first-order theories.

Results apply to automatic and tree-automatic structures.

Abstract

We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.