1. The leaves are labeled with propositional letters 2. if a node o is labeled with a proposition of the form(avB),(anB),a,B)or(a+ B), its immediate successors, o0 and o 1, are labeled with a and B (in that order) if a node o is labeled with a proposition of the form(a), its unique immediate successor, g0 is labeled with a How to map a well-defined proposition to a tree? Consider the following example Example3. The formation tree of(AVB),(A∧B)→C) It is easy to draw its formation tree for this example. However, when a proposition is complicated enough, it is not easy. Just rethink your approach. We may follow the procedure of constructing a proposition from a propositional letters in a bottom-up way, even we define it in a top-down approach These two examples are specified. What about the other propositions? Given proposition, we have the following questions 1. Is there a formation tree? 2. Is it unique? It is lucky that we have the following Theorem Theorem 4. Each well-defined proposition has a unique formation tree associated with it Proof.(Sketch) 1. Existence of the formation tree by induction on depth 2. Uniqueness of the formation tree by induction on depth From now on, we sometimes call the labeled tree of a proposition associated formation tree Once we have formation tree of a proposition, we can define these following terms Definition 5. Given an associated formation tree, we have 1. The depth of a proposition is the depth of associated formation tree 2. The support of a proposition is the set of propositional letters that occur as labels of the leaves of the associated formation tree Actually, all inductive proof could be based on the depth of a proposition.1. The leaves are labeled with propositional letters. 2. if a node σ is labeled with a proposition of the form (α ∨ β),(α ∧ β),(α → β) or (α ↔ β), its immediate successors, σˆ0 and σˆ1, are labeled with α and β (in that order). 3. if a node σ is labeled with a proposition of the form (¬α), its unique immediate successor, σˆ0, is labeled with α. How to map a well-defined proposition to a tree? Consider the following example. Example 3. The formation tree of (A ∨ B),((A ∧ B) → C) . It is easy to draw its formation tree for this example. However, when a proposition is complicated enough, it is not easy. Just rethink your approach. We may follow the procedure of constructing a proposition from a propositional letters in a bottom-up way, even we define it in a top-down approach. These two examples are specified. What about the other propositions? Given proposition, we have the following questions: 1. Is there a formation tree? 2. Is it unique? It is lucky that we have the following Theorem. Theorem 4. Each well-defined proposition has a unique formation tree associated with it. Proof. (Sketch) 1. Existence of the formation tree by induction on depth. 2. Uniqueness of the formation tree by induction on depth. From now on, we sometimes call the labeled tree of a proposition associated formation tree. Once we have formation tree of a proposition, we can define these following terms. Definition 5. Given an associated formation tree, we have 1. The depth of a proposition is the depth of associated formation tree. 2. The support of a proposition is the set of propositional letters that occur as labels of the leaves of the associated formation tree. Actually, all inductive proof could be based on the depth of a proposition. 3