Some questions about first-order logic (arising from a book by Raymond M Smullyan) Recently, I got confused when reading a book about first order logic written by Raymond M smullyan.
Chapter 1 page 9:When introducing the notion "Formation tree", smullyan define a formation tree for a formula X as an ordered dyadic tree whose points are occurrences of formulas.
1.the origin point be occurrence of X
2.each end point is an occurrence of propositional variable
3.each simple point is of the form ~Y and has an occurrence of Y as its sole successor
4.each junction point is of the form X b Y and has occurrences of X Y as respective left and right successors.
The question is, what is the precise definition of "occurrence"of formula? 
I have ever tried to understand the notion "Formation tree" as an ordered dyadic tree together with one function from the set of all points in the tree into the set of all subformulas of X , such that we make an assignment for each point in the tree, And the pair (tree together the function) should obey above conditions.But it might seems too complicated.I feel confused.....
Another question (page 10) : How to proof that any interpretation v0 of E can be extended to unique Boolean v valuation of E? Raymond have mentioned that"verified by induction on the degree of X".I don't know the exact process... 
hope for your help.
 A: (1) Consider this simple formation tree for the wff $(P \land P)$:

$$(P \land P)$$
$$ \diagup \quad \diagdown$$
$$ P \quad\quad\quad P$$

What do we have at the two lower nodes? One and the same formula $P$? Well, no, not literally, for that is one thing, and there are two things at the lower nodes. Better then: two different tokens or instances of the same type of formula. Or in a different jargon, two different occurrences of the formula[-type] $P$.
Now that informal explanation is surely all you need. Of course, you can go fancy and give an alternative story where we think of the nodes of the tree as abstract elements in a poset whose order relation makes it tree like,  and then we have a function that decorates the nodes by mapping each element to some member of the set of wff-types of the relevant language, as you suggest. But this is unnecessarily complicated. As Smullyan describes it the nodes of the tree can be thought of as themselves occurrences of formulas. Why not?
(2) It will be a standard course-of-values induction on the complexity of the wff (i.e. the number of connectives). Assume that an interpretation of atoms extends to a unique Boolean valuation of wffs of up to complexity $n$. Then what about a wff of complexity $n + 1$? It must be a negation of a wff of complexity $n$, or a conjunction/disjunction/condition of two wffs of complexity no more that $n$. Show the the unique Boolean valuation of  wffs of up to complexity $n$ extends in one an only one way to cover these various kinds of wff of complexity $n + 1$ ... [If that is still too mysterious, consult some other textbook[s] where this is spelt out in detail.]
