Extension of First-Order Theories into Trees

Abstract. We present in this paper an automatic way to combine any first-order theory T with the theory of finite or infinite trees. First of all, we present a new class of theories that we call zero-infinite-decomposable and show that every decomposable theory T accepts a decision procedure in the form of six rewriting rules which for every first order proposition give either true or false in T. We present then the axiomatization T ∗ of the extension of T into trees and show that if T is flexible then its extension into trees T ∗ is zero-infinite-decomposable and thus complete. The flexible theories are theories having elegant properties which enable us to eliminate quantifiers in particular cases.