Induction without integers (aka Structural Induction) While composing the following question, I had an "ah-ha" moment. I still want to post the question along with my answer to show what I have learned. Any comments or additional answers will be greatly appreciated.
Recently I encountered a theorem in An Introcution to Mathematical Logic and Type Theory: To Truth through Proof by Peter B. Andrews where the author states that it can be used in inductive proofs without using integers. The theorem is stated as

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}$.

I am quite familiar with mathematical induction on integers. Mine typically take the following form:

Blah, blah, blah. Therefore, the statement holds for $n=1$.
Now assume that the statement is true for some integer $n$. Now consider the statement for $n+1$. Yadda, yadda, yadda (eventually transforming the statement for $n+1$ into a statement involving $n$). Therefore, the statement holds for $n+1$.

I'm also comfortable with using strong induction:

Blah, blah, blah. Therefore the statement holds for $n=1$.
Now assume that the statement is true for all integers $k$ such that $1 \le k \le n$ for some integer $n$. Now consider the statement for $n+1$. Yadda, yadda, yadda (eventually transforming the statement for $n+1$ into a statement involving integers $k$ between $1$ and $n$). Therefore, the statement holds for $n+1$.

One example where I would use this is in graph theory to prove a statement about trees. I proceed by induction on the number of vertices in a tree. This maps the object of interest (a tree) to the integers.
When I tried to apply the theorem about wffs, I got stuck how to proceed. How do I apply this theorem to a proof?
 A: $\def\p{{\mathscr R}}$If you are uncomfortable with the idea of doing induction directly on the structure, or if you want to reduce the question to one of induction on the integers, you can proceed by induction on the size of the WFF, for some suitable definition of "size". One typical definition is that the size of the WFF is the number of logical operators it contains.
Then to prove that $\p(W)$ holds for every WFF $W$, you proceed as follows:

*

*Show that $\p(W)$ holds for each $W$ of the smallest possible size. (1, if you are counting atoms, or 0, if you are counting operators.)

*Show that if $\p(W)$ holds for all $W$ of size less than $n$, then it must hold for all $W$ of size $n$, as follows: Let $W$ be a WFF of size $n$.  Then it must have the form $\sim A$ for some wff $A$ of size $n-1$, or the form $A\oplus B$ for some operator $\oplus$ and some wffs $A$ and $B$ each of size at most $n-1$. Fill in the inductive argument for the two or more cases.

Formulated in this way, the induction is just a regular strong induction on integers, where instead of proving the statement "$\p(W)$ holds for all wffs $W$", you reformulate it as "For all numbers $n$, $\p(W)$ holds for each wff of size $n$".
But this sort of transformation should not really be necessary.  The induction principle can be stated more generally.  Suppose $S$ is any set, and $\prec$ is a well-founded order on $S$; this means that every subset of $S$ is either empty, or contains a $\prec$-minimal element, which is an element $m\in S$ such that no other element $m'\in S$ has $m'\prec m$.
A typical example would be that wffs can be ordered by an ordering that says that $a\prec b$ whenever $a$ is a subformula of $b$.  For example, $(x\land  y)$ is a subformula of $\lnot(x\land y)\lor z$, so $(x\land  y)\prec \lnot(x\land y)\lor z$.
The ordering $\prec$ need not be total, which means that it is possible that none of $a\prec b, a=b, $ and $b\prec a$ need be true. For the $\prec$ of the previous paragraph, we have neither $a\land b \prec a\lor b$ nor $a\lor b \prec a\land b$. That is quite all right.
Then you can use well-founded induction as follows:

*

*Let $F$ be the set of wffs for which $\p$ is false. Suppose $F$ is nonempty. Then by the well-foundedness of $\prec$, the set $F$ has a $\prec$-minimal element $m$.

*Show that $m$ cannot have any subformulas, as follows:  Using some properties of $\p$, show that $\p$ must fail for one of the subformulas of $m$.  (This will depend on the details of $\p$ itself.)  But then this subformula of $m$ would be an element of $F$, which would contradict the hypothesis that $m$ was $\prec$-minimal in $F$.

*So $m$ has no subformulas. Rule out this case using some property of $\p$.

This rules out the possibility that $F$ actually contains a $\prec$-minimal element $m$, and the only remaining possibility is that $F$ is empty, and so $\p$ holds for every wff.
Ordinary induction is a special case of well-founded induction which uses the well-founded relation $\lt$ on the natural numbers. The well-foundedness of $\lt$ is equivalent to the so-called well-ordering principle of the natural numbers, which states that every subset of $\Bbb N$ either contains a $\lt$-minimal element, or is empty.
A: I will give a generalized answer here. I have another question about the exercise on which I have been using this theorem, so hopefully that will serve as an example when I post it later.
The key to applying the Principle of Induction on the Construction of a Wff is in breaking down its logical structure. We start with a property $\mathscr{R}$ of formulas and then want to prove that every wff has the property $\mathscr{R}$. To do so, we just need to check each of the three conditions:

(1) $\mathscr{R}(\mathbf{q})$ for each propositional variable $\mathbf{q}$.

This is the base case for the induction. We just need to verify that every propositional variable has the property $\mathscr{R}$.

(2) Whenever $\mathscr{R}(\mathbf{A})$, then $\mathscr{R}(\mathord{\sim} \mathbf{A})$.

This is where I stumbled at first. However, after further consideration, I realized this is an implication, similar to the one we use for typical induction on the integers. To apply this condition, we need to assume that some formula $\mathbf{A}$ has property $\mathscr{R}$ then show that $~ \mathord{\sim} \mathbf{A}$ has property $\mathscr{R}$.

(3) Whenever $\mathscr{R}(\mathbf{A})$ and $\mathscr{R}(\mathbf{B})$, then $\mathscr{R}([\mathbf{A} \lor \mathbf{B}])$.

This is basically the same as above. The implication means that I have to assume that $\mathscr{R}(\mathbf{A})$ and $\mathscr{R}(\mathbf{B})$ and prove that $\mathscr{R}([\mathbf{A} \lor \mathbf{B}])$.
I will post another question that applies this theorm and makes the above comments a little more concrete with an example.
Added:
A more concrete example of an application of structural induction can be found in this question.
