It is obvious that it is wrong after substitution However, some substitution is not correct in the point of view of semantic. We have the followin definition Definition 7. If the term t contains an occurrence of some variable a(which is necessarily free in t)we say that t is substitutable for the free variable v in (v) if all occurrences of a in t remain free in p (u/t) onsager the following example Example 9. Let p(a)=((yR(, u))V((Vz)Q(a, a)) 1. Ift= f(w, u), then we have p(t)=p(a/t)=(((yR((w, u),y))V((Va)Q(f(w, u), a))) 2. If t= gy, 8(y)), it is not substitutable for a in p(a) Proposition 8. If a term s is an initial segment of a term t, sCt, thens=t Theorem 9(Unique readability for terms). Every term s is either a variable or constant symbol or of the form f(s1, in which case f, n and the si for 1 <i<n are all unique determined Proposition 10. If a formula a is an initial segment of a formula 1, a Cy, then a=? Theorem 11 (Unique readability for formulas). Each formula is a precisely one of the following components"of o as displayed in each of these formula are uniquely determine > er, the relevant forms: an atomic formula, (a B), (o,B), (a +B), (a),( aV B). Moreover, the relevant 4 Formation tree Definition 12. 1. Term formation trees are ordered, finitely branching tree T labeled with terms satisfying the following conditions (a) The leaves of T are labeled with variables of constant symbols (b) Each nonleaf node of T is labeled with a term of the form f(ti, ...,tn) (c) A node of t that is labeled with a term of the form f(t1, .. tn) has exactly n immediate successors in the tree. They are labeled in (lexicographic) order with t1,..., tn 2. A term formation tree is associated with the term with which its root node is labeled Proposition 13. Every term t has a unique formation tree associated with it Proposition 14. The ground terms are those terms whose formation trees have no variables on their leaves Definition 15. The atomic formula auxiliary formation trees are the branching trees of depth one whose root node is labeled with an atomic formula. If the root node of such a tree is labeled with an n-ary relation R(t1,., tn), then it has n immediate successor which are labeled in order with the terms tIt is obvious that it is wrong after substitution. However, some substitution is not correct in the point of view of semantic. We have the following definition. Definition 7. If the term t contains an occurrence of some variable x (which is necessarily free in t) we say that t is substitutable for the free variable v in ϕ(v) if all occurrences of x in t remain free in ϕ(v/t). Consider the following example. Example 9. Let ϕ(x) = (((∃y)R(x, y)) ∨ ((∀z)¬Q(x, z))). 1. If t = f(w, u), then we have ϕ(t) = ϕ(x/t) = (((∃y)R(f(w, u), y)) ∨ ((∀z)¬Q(f(w, u), z))). 2. If t = g(y, s(y)), it is not substitutable for x in ϕ(x). Proposition 8. If a term s is an initial segment of a term t, s ⊆ t, then s = t. Theorem 9 (Unique readability for terms). Every term s is either a variable or constant symbol or of the form f(s1, . . . , sn) in which case f, n and the si for 1 ≤ i ≤ n are all unique determined. Proposition 10. If a formula α is an initial segment of a formula γ, α ⊂ γ, then α = γ. Theorem 11 (Unique readability for formulas). Each formula φ is a precisely one of the following forms: an atomic formula, (α ∧ β),(α → β),(α ↔ β),(¬α),(α ∨ β). Moreover, the relevant ”components” of φ as displayed in each of these formula are uniquely determined. 4 Formation tree Definition 12. 1. Term formation trees are ordered, finitely branching tree T labeled with terms satisfying the following conditions: (a) The leaves of T are labeled with variables of constant symbols. (b) Each nonleaf node of T is labeled with a term of the form f(t1, . . . , tn). (c) A node of T that is labeled with a term of the form f(t1, . . . , tn) has exactly n immediate successors in the tree. They are labeled in (lexicographic) order with t1, . . . , tn. 2. A term formation tree is associated with the term with which its root node is labeled. Proposition 13. Every term t has a unique formation tree associated with it. Proposition 14. The ground terms are those terms whose formation trees have no variables on their leaves. Definition 15. The atomic formula auxiliary formation trees are the labeled , ordered, finitely branching trees of depth one whose root node is labeled with an atomic formula. If the root node of such a tree is labeled with an n-ary relation R(t1, . . . , tn), then it has n immediate successor which are labeled in order with the terms t1, . . . , tn. 4