Complete First-Order Axiomatization of Finite or Infinite M-extended Trees
Khalil Djelloul, Thi-Bich-Hanh Dao · 2006
Abstract. We present in this paper an axiomatization of the structure of finite or infinite M-extended trees. This structure is an intuitive combination of the structure of finite or infinite trees with another structure M and expresses semantically an extension to trees of the model M. Having a structure M = (DM, FM, RM), we define the structure of finite or infinite M-extended trees ExtM = (D, F, R) whose domain D consists of trees labelled by elements of DM ∪ F, where F is an infinite set of function symbols containing FM and another infinite set of function symbols disjoint from FM. For each n-ary function symbol f ∈ F, the operation f(a1,.., an) is evaluated in M and produces an element of DM if f ∈ FM and all the ai are elements of DM, or is a tree whose root is labelled by f and whose immediate children are a1,.., an otherwise. The set of relations R contains RM and another relation which distinguishes the elements of DM from the others. Using a first-order axiomatization T of M, we give a first-order axiomatization T of the structure ExtM and show that if T is flexible then T is complete. The flexible theories are particular theories whose function and relation symbols have some elegant properties which enable us to handle formulae more easily. 1