Axiomatization of the elementary theory of finite root systems

Abstract

A root system is a partially ordered set (poset) in which the set of successors of every element is linearly ordered, and above each element there exists a maximal one. We refer to a root system with a maximum as a cotree. In the literature, the terms forests and trees sometimes denote root systems and cotrees, respectively, but can also refer to their respective order duals. These tree-like structures are ubiquitous across various branches of mathematics. Central problems in set theory revolve around a special class of forests in which the set of predecessors of every node is well-ordered (see, e.g., [Jec71]). One of the five main systems in reverse mathematics also relates to trees through theWeak K¨onig’s Lemma (see, e.g., [Sim09, Chapter 4]). On the other hand, modal logic has the tree model property, under which every satisfiable modal formula is satisfied in a tree (see, e.g., [BRV01, Sections 1,2]). Trees also play a fundamental role in computability theory, for instance through König’s Lemma (see, e.g., [Soa16, Part II]), in automata theory (see, e.g., [KN01]), and in linguistics (see, e.g., [BPMMV94]). Moreover, a foundational result for this work is Rabin’s celebrated Tree Theorem (see [Rab69]), which establishes the decidability of the monadic second order theory of the two successor functions, S2S. This theorem is central to decidability theory because it implies the decidability of the elementary theory of several classes of structures, including trees, root systems, and their finite members. For the basics of monadic second order logic, we refer the reader to Section 2.4. For further details on the decidability of the monadic second order theory of S2S and related structures, see [Rab69], [KN01], and [Gur17].