Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees

TL;DR

This paper provides complete axiomatizations for various monadic second-order and fixed-point logics on finite trees, enabling formal proof of properties like reachability in structures such as XML documents and parse trees.

Contribution

It introduces the first complete axiomatizations for MSO, FO(TC1), and FO(LFP1) on finite trees, advancing formal logical understanding of these structures.

Findings

Axiomatizations are complete for finite trees.

Valid formulas on all finite trees are provable.

Logics are non-recursively axiomatizable on arbitrary structures.

Abstract

We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.