Formation tree Definition(Top-down) A formation tree is a finite tree T of binary sequences whose nodes are all labeled with propositions. The labeling satisfies the following conditions o The leaves are labeled with propositional letters O if a node o is labeled with a proposition of the form (aVβ),(aA3),(a→B)or(a分B),its immediate successors o0 and o 1 are labeled with a and B(in that order) O if a node o is labeled with a proposition of the form Ga), its unique immediate successor, 00, is labeled withFormation Tree . Definition (Top-down) . . A formation tree is a finite tree T of binary sequences whose nodes are all labeled with propositions. The labeling satisfies the following conditions: 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 α. Yi Li (Fudan University) Discrete Mathematics(II) March 26, 2013 9 / 20