An improved lower bound for the elementary theories of trees

Abstract

The first-order theories of finite and rational, constructor and feature trees possess complete axiomatizations and are decidable by quantifier elimination [15, 13, 14, 5, 10, 3, 20, 4, 2]. By using the uniform inseparability lower bounds techniques due to Compton and Henson [6], based on representing large binary relations by means of short formulas manipulating with high trees, we prove that all the above theories, as well as all their subtheories, are non-elementary in the sense of Kalmar, i.e., cannot be decided within time bounded by a k-story exponential function exp k (n) for any fixed k. Moreover, for some constant d>0 these decision problems require nondeterministic time exceeding exp∞ (⌊dn⌋) infinitely often.