Definition 16. The atomic formula formation trees are the finitely branching, labeled, ordered trees gotten from the auxiliary trees by attaching at each leaf labeled with a term the rest of the formation tree associated with t. Such a tree is associated with the atomic formula with which its root is labeled Proposition 17. Every atomic formula is associated with a unique formation tree Definition 18. The formula auxiliary formation trees are the labeled, ordered, binary branching trees T such that 1. The leaves of f are labeled with atomic formulas 2. If o is a nonleaf node of T with one immediate successor oo labeled writh a formula then g is labeled with mp, 3up, or Vup for some variable v 3. If o is a nonleaf node with two immediate successors, o A0 and o A l labeled with formulas sp and y, then g is labeled withφ∧v,φ∨v,φ→v,φ分v Definition 19. 1. The formula formation trees are the ordered, labeled trees gotten from the auciliary ones by attaching to each leaf labeled with an atomic formula the rest of its associated formation tree. Each such tree is again associated with the formula with which its root is 2. The depth of a formula is the depth of the associated auxiliary formation tree. Proposition 20. Every formula is associated with a unique(auxiliary) formation tree Proposition 21. The subformulas of a formula o are the labels of the nodes of the auciliary formation tree associated with Proposition 22. 1. The occurrences of a variable v in a formula p are in one-one correspon dence with the leaves of the associated formation tree that are labeled with v. We may also refer to the appropriate leaf labeled with v as the occurrence of v in 2. An occurrence of the variable v in p is bound if there is a formula o beginning with((vu)or(v) which is the label of a node above the corresponding leaf of the formation tree for p labeled th u Proposition 23. If p is a formula and v a variable, then (u/t)is the formula associated with e formation tree gotten by replacing each leaf in the tree for o u which is labeled with a free occurrence of v with the formation tree associated with t and propagating this change through the Proposition 24. The term t is substitutable for v in o(u) if all occurrences of a in t remain free in (t),i. e, any leaf in the formation tree for t which is a free occurrence of a variable a remains in every location in which it appears in the formation tree described in Definition 3.8 5 Parsing algorithm With help of formation tree, we could parse a formula in a relative way. As the definition is an expansion of definition of proposition by introducing variable, function, predicates, and quantifiersDefinition 16. The atomic formula formation trees are the finitely branching, labeled, ordered trees gotten from the auxiliary trees by attaching at each leaf labeled with a term the rest of the formation tree associated with t. Such a tree is associated with the atomic formula with which its root is labeled. Proposition 17. Every atomic formula is associated with a unique formation tree. Definition 18. The formula auxiliary formation trees are the labeled, ordered, binary branching trees T such that 1. The leaves of T are labeled with atomic formulas. 2. If σ is a nonleaf node of T with one immediate successor σ ∧ 0 labeled with a formula φ, then σ is labeled with ¬φ, ∃vφ, or ∀vφ for some variable v. 3. If σ is a nonleaf node with two immediate successors, σ ∧ 0 and σ ∧ 1 labeled with formulas φ and ψ, then σ is labeled with φ ∧ ψ, φ ∨ ψ, φ → ψ, φ ↔ ψ. Definition 19. 1. The formula formation trees are the ordered, labeled trees gotten from the auxiliary ones by attaching to each leaf labeled with an atomic formula the rest of its associated formation tree. Each such tree is again associated with the formula with which its root is labeled. 2. The depth of a formula is the depth of the associated auxiliary formation tree. Proposition 20. Every formula is associated with a unique(auxiliary) formation tree. Proposition 21. The subformulas of a formula φ are the labels of the nodes of the auxiliary formation tree associated with φ. Proposition 22. 1. The occurrences of a variable v in a formula φ are in one-one correspon￾dence with the leaves of the associated formation tree that are labeled with v. We may also refer to the appropriate leaf labeled with v as the occurrence of v in φ. 2. An occurrence of the variable v in φ is bound if there is a formula ϕ beginning with ((∀v) or ((∃v) which is the label of a node above the corresponding leaf of the formation tree for φ labeled with v. Proposition 23. If φ is a formula and v a variable, then φ(v/t) is the formula associated with the formation tree gotten by replacing each leaf in the tree for φ(v) which is labeled with a free occurrence of v with the formation tree associated with t and propagating this change through the tree. Proposition 24. The term t is substitutable for v in φ(v) if all occurrences of x in t remain free in φ(t), i.e., any leaf in the formation tree for t which is a free occurrence of a variable x remains in every location in which it appears in the formation tree described in Definition 3.8. 5 Parsing Algorithm With help of formation tree, we could parse a formula in a relative way. As the definition is an expansion of definition of proposition by introducing variable, function, predicates, and quantifiers. 5