Formation sequence for a logic formula I will start with some definitions from An Introduction to Mathematical Logic and Type Theory: To Truth through Proof by Peter B. Andrews then give the exercise that I am working along with my attempt at a proof. My actual question will be at the bottom, if you wish to skip ahead.
Definitions:

(1) The set of wffs is the intersection of all sets $\mathscr{S}$ of formulas such that:
(i) $\mathbf{p} \in \mathscr{S}$ for each propositional variable $\mathbf{p}$.
(ii) For each formula $\mathbf{A}$ if $\mathbf{A} \in \mathscr{S}$, then $\mathord{\sim} \mathbf{A} \in \mathscr{S}$.
(iii) For all formulas $\mathbf{A}$ and $\mathscr{B}$, if $\mathbf{A} \in \mathscr{S}$ and $\mathbf{B} \in \mathscr{S}$, then $\left[\mathbf{A} \lor \mathbf{B} \right] \in \mathscr{S}$.
(2) A wff is a member of the set of wffs.

Theorems:

1000 Principle of Induction on the Construction of a Wff. Let $\mathscr{R}$ be a property of formulas, and let $\mathscr{R}(\mathbf{A})$ mean that $\mathbf{A}$ has property $\mathscr{R}$. Suppose
(1) $\mathscr{R}(\mathbf{q})$ for each propositional variable $\mathbf{q}$.
(2) Whenever $\mathscr{R}(\mathbf{A})$, then $\mathscr{R}(\mathord{\sim} \mathbf{A})$.
(3) Whenever $\mathscr{R}(\mathbf{A})$ and $\mathscr{R}(\mathbf{B})$, then $\mathscr{R}([\mathbf{A} \lor \mathbf{B}])$.
Then every wff has property $\mathscr{R}$.

Exercise:

A formation sequence for a formula $\mathbf{Y}$ is a finite sequence $\mathbf{Y}_1, ..., \mathbf{Y}_m$ of formulas such that $\mathbf{Y}_m$ is $\mathbf{Y}$ and for each $i$ ($1 \le i \le m$), one of the following conditions holds:
(a) $\mathbf{Y}_i$ is a propositional variable;
(b) there is $j < i$ such that $\mathbf{Y}_i$ is $\sim \mathbf{Y}_j$;
(c) there are indices $j < i$ and $k < i$ such that $\mathbf{Y}_i$ is $\left[ \mathbf{Y}_j \lor \mathbf{Y}_k \right]$.
Prove that a formula $\mathbf{Y}$ is well-formed iff it has a formation sequence. (Hint: Metatheorem 1000 may be useful.)

Partial Proof:
Suppose $\mathbf{Y}$ is a wff. If $\mathbf{Y} = \mathbf{p}$ for some proprositional variable $\mathbf{p}$ then $\mathbf{Y}_1 = \mathbf{p}$ is a formation sequence for $\mathbf{Y}$. Now assume that formulas $\mathbf{A}$ and $\mathbf{B}$ have formation sequences $\mathbf{A}_1, ..., \mathbf{A}_m$ and $\mathbf{B}_1, ..., \mathbf{B}_n$, respectively. If $\mathbf{Y} = \mathord{\sim}\mathbf{A}$ then $\mathbf{A}_1, ..., \mathbf{A}_m, \mathbf{Y}$ is a formation sequence for $\mathbf{Y}$. If $\mathbf{Y} = \left[ \mathbf{A} \lor \mathbf{B} \right]$ then $\mathbf{A}_1, ..., \mathbf{A}_m, \mathbf{B}_1, ..., \mathbf{B}_n, \mathbf{Y}$ is a formation sequence for $\mathbf{Y}$. By Metatheorem 1000, we can conclude that $\mathbf{Y}$ has a formation sequence.
Question:
Now I am stuck on the proof in the other direction. I know I need to start with "Suppose $\mathbf{Y}$ is a formula with a formation sequence $\mathbf{Y}_1, ..., \mathbf{Y}_m$." I think I need to continue from there with "Let $\mathscr{S}$ be a set of formulas satisfying conditions (i), (ii), and (iii) of the definition of the set of wffs." Now I need to show that $\mathbf{Y} \in \mathscr{S}$. I believe I need to do this by induction. I can see the idea in my head, but I am having trouble formulating it on paper (or on screen, as the case may be). I can start with a base case: "If $\mathbf{Y} = \mathbf{Y}_m = \mathbf{p}$ for some propositional variable $\mathbf{p}$, then $\mathbf{Y} \in \mathscr{S}$." The next case to consider is "If $\mathbf{Y} = \mathbf{Y}_m = \mathord{\sim} \mathbf{Y}_j$ for some $j < m$..." then what? I haven't stated a clear inductive hypothesis, and that's where I'm truly stuck. Should I proceed by induction on $m$, the length of the formation sequence for $\mathbf{Y}$? Or should I use structural induction similar to what I did for the first half of the proof?
Any pointers here would be greatly appreciated. Thanks.
 A: Hint: Prove the result by (strong) induction on the length of the formation sequence. So we suppose the result is true for any formula in a formation sequence of length $\lt n$, and show the result holds for any formula in a formation sequence of length $n$. 
More precisely, we want to show  (by the aforementioned induction) that the collection of end formulas of our sequence of length $n$ is closed under (i),(ii), and (iii), and is therefore an element of any set $\mathscr{S}$ in the definition of the set of wffs. Once one decides what has to be done, the actual details more or less write themselves. 
A: I don't think your partial proof works. You tacitly assume that because $\mathbf Y$ is a wff must be either a propositional variable, a negation, or a disjunction -- and that is true, but it is also essentially what you're trying to prove in this step, so assuming it just creates a circular argument where you're not actually proving anything.
You have the right intuition about wffs, but at this step the definition you have to work with is the one you quote, and only that. What you're proving in the exercise is essentially that the definition does produce the set that you already have an intuition about. (I imagine that your intuition is actually better captured by the "formation sequence" concept than by the actual definition your text has selected).
What you should be doing in that step is something like: Let $\mathscr F$ be the set of all symbol strings that have a formation sequence. Prove that $\mathscr F$ satisfies the conditions for being one of the $\mathscr S$s being intersected in definition 1. Then, since a wff $\mathbf Y$ is by definition a member of the intersection, it is also a member of $\mathscr F$, and so $\mathbf Y$ must have a formation sequence.
In the other direction, consider an arbitrary $\mathscr S$ from the definition, and an arbitrary formation sequence. Prove that every formula in the sequence is in $\mathscr S$, by long induction on its position in the sequence. Since $\mathscr S$ and the formation sequence were both arbitary, this proves that every $\mathbf Y$ that has a formation sequence is in every $\mathscr S$, and therefore also in the intersection of the $\mathscr S$s -- so it is a wff.

Later in the course you will (probably; I don't have your book) notice a similar situation with the definitions of what the set of theorems in a theory is. The set of logical consequences of a collection of axioms can be defined either as the intersection of all sets $\mathscr R$ of wffs such that $\mathscr R$ contains the axioms and is closed under rules of inference, or as the set of wffs that have formal proofs. And the relation between those two definitions is exactly the same as the relation between the two characterizations of "well-formed formula" you're proving to be equivalent here.
