Proving that the recursive definition of a formula restricts what is a formula My text provides (a pretty standard, I think) recursive definition of well-formed formula:

The set of wff, denoted $\textbf{WFF}$, is the smallest set that satisfies:
  
  
*
  
*All propositional variables, $\textbf{p}$, and the propositional constants $\top,\bot$ are in $\textbf{WFF}$. These are called atomic formulas.
  
*If $A,B\in\textbf{WFF}$, then $(\neg A), (A\circ B)\in\textbf{WFF}$, where $\circ\in\{\land,\lor,\rightarrow,\equiv\}$
  

Presumably from the definition, the text relies on the fact that all formulas are strictly one of (1) atomic, (2) of the form $(\neg A)$, or of the form $(A \circ B)$ in all its proofs about formulas, and, intuitively, I can appreciate that the definition implies this. 
Here's a very simple proof, presented in the text, that $\color{red}{p\lor}$ is not a formula:

$p\lor$ is clearly not atomic.
$p\lor$ does not begin with an open parenthesis, and therefore is not of the form $(\neg A)$ or $(A\circ B)$
Therefore $p\lor\notin\textbf{WFF}$
$\square$

But doesn't it still need to be proved that all formulas are either atomic, $(\neg A)$, or $(A\circ B)$? After all, in part 2. of the definition, how do we know (beyond intuition) that $A$ cannot equal $p\lor$, and therefore $\notin\textbf{WFF}$?
Edit: I realize that "smallest set" means that we "throw away" any strings that don't satisfy the definition's criteria, but how can we be sure that in condition 2., $A$ and $B$ are not of a form different from $(\neg A)$ or $(A\circ B)$? (Even though intuitively that's rather obvious, doesn't it require an explicit proof of its own?)
 A: In this particular example, the following direct argument would work:

Assume $W$ is a set of words that satisfies your two conditions. Then $$ W' = \{w\in W\mid w\text{ does not end with }{\lor}\} $$ will also satisfy the two conditions (which can easily be checked). Therefore, if $W$ contains any word that ends with $\lor$, it will not be the smallest set that satisfies the condition, and therefore it is not $\mathbf{WFF}$. In particular, $\mathbf{WFF}$ does not contain the word $p\lor$.

In general, we can show from the smallest-set definition that $\mathbf{WFF}$ consists of exactly those words that have a finite parse tree that matches the rules, and when you have a wff, you can therefore assume that has a parse tree.
Usually, though, when reasoning about wffs you don't need to appeal to parse trees explicitly -- almost everything you'd want to prove by picking wffs apart can be phrased as  structural induction:

Suppose $\phi(w)$ is some property of strings such that
  
  
*
  
*$\phi(w)$ holds whenever $w$ is an atomic formula.
  
*Whenever $\phi(u)$ and $\phi(w)$ hold, then also $\phi((\neg w))$ and $\phi((u\circ w))$.
  
  
  Then $\phi(w)$ holds for every $w\in\mathbf{WFF}$.

This is true because $\{w\in\mathbf{WFF}\mid \phi(w)\}$ is a set that satisfies the two condition, and since $\mathbf{WFF}$ is the smallest such set, it must equal $\{w\in\mathbf{WFF}\mid \phi(w)\}$.
In particular, when you have a wff, you can assume that it has one of the forms in the definition -- because "has one of those forms" is a property that works as $\phi$ in the structural induction theorem.
A: It is because, as explicitly stated in the definition, the set WFF is the smallest set satisfying 1 and 2 (where 'smaller' is understood in terms of subsets: in this context, set $A$ is 'smaller' than set $B$ if $A$ is a strict subset of $B$)
So, if there was something $X$ in WFF  that was not either atomic or of the form $A \circ B$, then WFF would not be the smallest set satisfying 1 and 2, because if there are such elements, then out of all those, pick a smallest one (i.e with the least length/number of symbols), and that element can't possibly have been forced in the set by either 1 or 2
For example, if $p\lor$ was in the set, then $(\neg p \lor)$ would by 2 be forced in the set as well, and therefore also $(\neg p\lor \land \neg p \lor)$, etc. Now,  all these later 'larger' ones are thus all forced by the initial $p \lor$, and therefore removing any of those from the set would go against the set satisfying 1 and 2. However, the 'smallest' such 'nonsense' formula (or at least: a 'nonsense' formula such that no smaller one exists in the set) is certainly not forced by either 1 or 2, and can therefore be removed from the set without effecting the set's satisfying 1 and 2. Hence, since WFF is the smallest set satisfying 1 and 2, it cannot contain such a smallest formula that is not atomic or of the form $(A \circ B)$.
A: The definition of $\textbf{WFF}$ given is just one example of many that are stated in terms of "the smallest set" that satisfies some property, but they are better understood as giving a recursive construction for the desired set. More precisely, the construction is given by stages. In stage $1$ we are given a set of atomic formulas. In stage $n$ we construct those formulas produced using all previous stages using the given operations. The final set $\textbf{WFF}$ is the disjoint union of the sets of all the stages.
For example, $\;p\;$ is given in stage $1$, $\;(\neg p)\;$ is produced in stage $2$, $\;(q\to(\neg p))\;$ is produced in stage $3$, and so on. This  constructive building up approach is in contrast to a cutting down approach where we have to assume that there exists a smallest set with a certain property.
A: Using the constructive approach as suggested by Somos, we can take a step back and make an algorithm for any member of WFF.

We can start with a counter C equal to 0.
If the current symbol is a propositional variable, then we decrease C by 1.
If the current symbol is $\lnot$, then we rewrite the counter.
If the current symbol is '(', then we increase the counter by 1.
If the current symbol is ')', then we decrease the counter by 1.
Finally, if the current symbol is a member of ∘, then we increase the counter by 1.

For ($\lnot$A), the sequence of the values of the counter is
[0, 1, 1, 0, -1].
    (  ¬  A   )

For any propositional variable, the sequence of the values of the counter is 
[0, -1].
     A

For (A∘B), the sequence of the values of the counter is 
[0, 1, 0, 1, 0, -1].
    (  A  ∘  B   )

Any member of WFF which satisfies that algorithm will have one propositional variable, the value of C will start as 0, end with -1, and only have -1 as it's final value.
Now the above algorithm is adequate to determine what is and what is not a member of **WFF*.  The following lemma builds towards a proof of adequacy.

Lemma: Each formula F produced from the constructive process will have C start as 0, end with -1, and F will have at least one propositional variable.
Proof: That any formula at stage 1 has C start as 0 and end with -1 is indicated above.  That any such F has at least one propositional variable follows from the nature of the constructive process.  
Induction step: Now, we'll assume that all stage n formulas satisfy this lemma.  For a
  stage (n + 1) formula, we either have a formula A of stage n which
  is inside of ($\lnot$A) or two formulas A and B of stage n inside of
  (A∘B).  If the former, then the sequence of the values of the counter
  is [1, 1, {...}, one less than the final value {...}], where {...} is the
  sequence of the values of the counter for A.  But, the sequence of
  values of C in {...} took in a number and produced one less than that
  number by the inductive assumption.  Thus, it follows that the sequence of the values of the
  counter once the algorithm has gone through all value changes that happen in {...} is (1, 1, 0, -1).  For a formula of the type (A∘B) the
  sequence of the values of the counter is [1, {...}, one more than the
  value of C at the end of {...}, !...!, one less than the value of C at
  the end of !...!].  But again, the values of {...} start with some
  number and produce a number one less than that number, and !...!
  effects the same decrease in value.  Thus, the sequence of values when
  each of {...} and !...! terminate is [1, 0, 1, 0, -1].  So, assuming
  that this theorem holds for stage n, it will hold at the stage (n+1). 
  Therefore, each formula produced from the constructive process will
  have C start as 0 and end with -1 and have at least one propositional
  variable.

That -1 only appears at the end of the algorithm also gets guaranteed by the base case, and an inductive step where sequences of values for {...} and !...! refer back to the base case.
So, let's say that we suppose that some $\alpha$ has a form different from ($\lnot$A) or (A∘B).  We then apply the above algorithm to that $\alpha$.  But, if we built up the formula in stages from this definition as we have supposed, then the sequence of values of C for $\alpha$ will either have -1 as some value of C before it's last value, or C will be something other than -1 as it's last value.  But, by the algorithm, that shows that $\alpha$ is not a member of WFF.
