I have to prove that in a formation sequence of a formula F, all formulas that appear are sub-formulas of F. The proof that the text (Boolos, Computability and Logic) suggests is by induction on complexity. The method is defined in two steps in the same text as:
Base Step: Prove that atomic formulas have the property.
Induction Step: Prove that if a more complex formula is formed by applying a logical operator to a simpler formula or formulas, then, assuming (as induction hypothesis) that the simpler formula or formulas have the property, so does the more complex formula.
So the property to be proven can be expressed as this:
P: If a formula $\alpha$ is an instance on a formation sequence of a formula F, then $\alpha$ is a sub-formula of F.
(1.0) Atomic formulas have the property, as any atomic formula A on a formation sequence of a formula F is also a sub-formula of F.
But the induction step certainly can't hold, for example in:
(Aa $\land$ Bb) $\rightarrow$ Cc
members of the formation sequence are Aa, Bb, Cc, Aa $\land$ Bb and (Aa $\land$ Bb) $\rightarrow$ Cc. Any of these formulas have the property P, but certainly Cc $\land$ Aa does not, as many other examples.
I've tried instead to make my way to the proof through another start. It "feels" like the same method, and looks similar but "inversed".
Thm. $(1.1)$ F itself appears in the formation sequence, and is a subformula of F. Hence satisfies P
Thm. $(1.2)$ Let A be a formula. If A appears in the formation sequence and it is a sub-formula of F, then it is atomic (satisfies P by (1.0)) or is obtained by some earlier formulas G and H in the sequence by negation, conjunction, disjunction, or universal or existential quantification. Hence G and H are in the sequence, and are sub-formulas of F (that's the way sub-formulas are defined), so G and H satisfy P.
Therefore (1.1) and (1.2) are true in any formation sequence in which 𝐹 is a subformula of F.
For all F, F is a sub-formula of F.
all A in any formation sequence of a formula F is a sub-formula of F.
Now, as I see the method again, it seems that it has to be redefined as the following:
Base Step: Prove that a formula has the property.
Induction Step: Prove that if a more simple formula is formed by extracting a logical operator to a more complex formula, then, assuming (as induction hypothesis) that the more complex formula has the property, so does the more simple formula.
To finish and go to the point, my question is the following:
Is the proof given a proof by induction on complexity, on the way mentioned (does the proof satisfy the method?), or is it a semantic proof?