# Proving that a Tree Language is not First-Order Definable

## TL;DR

This paper investigates the algebraic properties of tree languages that are not definable by first-order logic with ancestor predicate, providing recursive proofs of nondefinability and extending algebraic concepts.

## Contribution

It introduces a recursive proof method for non-definability of tree languages and extends algebraic notions like aperiodicity within forest algebra frameworks.

## Key findings

- Recursive proofs exist for all non-definable languages.
- Extended algebraic structures generalize existing notions like aperiodicity.
- A new algebra of mappings aids in analyzing non-definability.

## Abstract

We explore from an algebraic viewpoint the properties of the tree languages definable with a first-order formula involving the ancestor predicate, using the description of these languages as those recognized by iterated block products of forest algebras defined from finite counter monoids. Proofs of nondefinability are infinite sequences of sets of forests, one for each level of the hierarchy of quantification levels that defines the corresponding variety of languages. The forests at a given level are built recursively by inserting forests from previous level at the ports of a suitable set of multicontexts. We show that a recursive proof exists for the syntactic algebra of every non-definable language. We also investigate certain types of uniform recursive proofs. For this purpose, we define from a forest algebra an algebra of mappings and an extended algebra, which we also use to redefine the notion of aperiodicity in a way that generalizes the existing ones.