Induction on complexity, upside down?

Question

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?

Answer 1

The formation sequence of $(Aa ∧ Bb) → Cc$ will be :

$Aa, Bb, Cc, (Aa ∧ Bb) \ [\text { from 1st and 2nd terms of the sequence }], (Aa ∧ Bb) → Cc \ [\text { from 4th and 3nd terms of the sequence }].$

$Cc ∧ Aa$ is not part of this formation sequence.

Obviously, also $Aa, Bb, Cc, (Aa ∧ Bb), (Cc ∧ Aa), (Aa ∧ Bb) → Cc$ is a formation sequence; we can say that it is not the "minimal" one, because it has unnecessary formulas.

But what we are asked to prove is not that the formation sequence must contain only subformulas of the last formula $F$, but that "every subformula of $F$ must appear".

---

We have that :

a formation sequence is a sequence of formulas in which each formula either is atomic, or is obtained by some earlier formula(s) in the sequence by negation, conjunction, disjunction, or universal or existential quantification. A formation sequence for a formula $F$ is just a formation sequence whose last formula is $F$.

It may be useful to define $\text {Sub}(F)$ as the set of subformulas of $F$.

Another way of wxpressing the sought property is that :

Let $G$ be a subformula of $F$. Show that $G$ occurs in each formation sequence of $F$.

The proof by induction on "complexity" of $F$ must run as follows :

(i) Base case : $F$ is atomic, i.e. $A^1(v_0)$, or $=(t_1,t_2)$.

But we know that every formation sequence must end with $F$.

Thus the only subformula $G$ of $F$ is $F$ itself, and it will for sure appear in any formation sequence (also those with "garbage", i.e. with unnecessary formulas) because the formation sequence must end with the formula $F$ (i.e. $G$).

(ii) Induction step : two subcases, for $\lnot$ and $\lor$ (or any other binary connective).

Consider the $\lor$ case : we have that $F$ is $(F_1 \lor F_2)$ and we must consider the induction hypothesis : for both formulas $F_1$ and $F_2$ the property that their respective subformulas must appear in each formation sequences (ending respectivey with $F_1$ and $F_2$) must hold.

We have to consider that the formula $F$ have only one new subfomula with respect to the "sum" of the subformulas of $F_1$ and $F_2$: $(F_1 \lor F_2)$ itself [i.e. $\text {Sub}(F)= \text {Sub}(F_1) \cup \text {Sub}(F_2) \cup \{ (F_1 \lor F_2) \}$].

Again, if $(F_1 \lor F_2)$ is the last formula of the formation sequence, $F_1$ and $F_2$ must apper in the sequence [each formula either is atomic, or is obtained by some earlier formula(s) in the sequence by negation, conjunction, disjunction, etc.]

Thus all t,he part of the sequence ending with $F_1$ is a formations equence for $F_1$ (and the same for $F_2$).

By induction hypothesis, due to the fact that the $F_i$ have "lower" complexity with respect to $F$, their subsformulas must appear in the formation sequence.

And thus, the formation sequence of $F$ must contain all subformulas of $F_1$ and all subformulas of $F_2$ and $(F_1 \lor F_2)$.