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 following 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 lu) if all occurrences of a in t remain ee in ((u onsider tne Example 9. Let p(a)=(((yR(a, u))V((Vz)Q(a, a)) 1.Ift= f(w, u), then we have p(t)=p(a/t)=(((yR((w, u), y))V((Vz)Q(f(w, u), a))) 2. Ift= g(y, s()), it is not substitutable for in p(a) Proposition 8. If a term s is an initial segment of a term t, s Ct, then s=t Theorem 9(Unique readability for terms). Every term s is either a variable or constant symb or of the form f(s1, .. Sn)in which case f, n and the si for 1<isn are all unique determined Proposition 10. If a formula a is an initial segment of a formula 1, a C?, then a=? Theorem 11 (Unique readability for formulas ). Each formula o is a precisely one of the following forms: an atomic formula,(aAB),o,B),a+ B), a),(aV B. Moreover, the relevant components"of o 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 condition (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,...,t, 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 th e root node 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 tu, .. tnIt 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