On n-Syntactic Equational Theories
We define the n-syntactic theories as a natural extension of the syntactic theories. A n-syntactic theory is an equational theory which admits a finite presentation in which every proof can be performed with at most n applications of an axiom at the root, but no finite presentation in which every proof can be performed with at most n − 1 applications of an axiom at the root. The n-syntactic theories inherit the good properties of the syntactic theories for solving the word problem, or matching or unification problems. We show that for any integer n ≥ 1, there exists a n-syntactic theory.