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.