# Let $\alpha\in \text{FORM}$. If $\beta \in Sub( \alpha) \implies \beta$ shows up in every formation chain of $\alpha$.

Warning: I'm translating from spanish so probably many terms may sound unfamiliar.

Warning 2: I'm probably going to link this question from many others I ask so I don't copy and paste these definitions all the time.

Let $$\alpha\in \text{FORM}$$. If $$\beta \in Sub( \alpha) \implies \beta$$ shows up in every formation chain of $$\alpha$$.

A formation chain (fc) of a formula $$\alpha$$ is a sequence $$X_1,X_2,...,X_n= \alpha$$ (a fc whose last element is $$\alpha$$ is called a $$\alpha$$-fc.), such that every element in the sequence have the form:

(1) $$X_i=p$$ for some variable $$p$$.

(2) $$X_i=(X_j \star X_k), 1\leq j,k (star means "and", "or" or "implies).

(3): $$X_i=\neg X_j, j

I also have a theorem that says:

$$\alpha \in \text{FORM} \iff \exists$$ a $$X_1,X_2,...,X_n=\alpha$$ f.c.

I think I have to use induction on either the complexity of $$\alpha$$ or the length of the fc, but I have no idea how.

We'll ignore the inappropriate "Warning 2" in a charitable way ....

Assume a subformula is a segment of a formula which is itself a formula.

Let $X_1, X_2, \ldots X_n$ be a formation chain for $\alpha$, and let $\beta$ be a subformula of $\alpha$. Let $X_b$ be the first member of the chain that has $\beta$ as a subformula. There must be a first such member, since at least $X_n$ has $\beta$ as a subformula. [Comment: we are at this point using the Least Number Principle, which is equivalent to induction -- an induction, in this case, over the length of the formation chain, as predicted.]

It is enough to show that $X_b$ must be $\beta$ (a wff counts as a subformula of itself).

We proceed by reductio.

Suppose $X_b$ isn't $\beta$, then it has to be a more complex formula with the wff $\beta$ as a part. But then $X_b$ must be either $\neg X_a$ or $( X_a \star X_{a'})$, for $a, a' < b$.

In the first case, by hypothesis $X_a$ doesn't have the wff $\beta$ as part, so neither does $\neg X_a$, i.e. $X_b$. Contradiction.

In the second case, by hypothesis neither $X_a$ nor $X_{a'}$ has the wff $\beta$ as a part, so [K] neither does $( X_a \star X_{a'})$, i.e. $X_b$. Contradiction.

So we are done -- assuming you have a proof of [K] already to hand, i.e. a proof that if $(X_a \star X_{a'})$ has the wff $\beta$ as a part, so does at least one of $X_a, X_{a'}$. That follows because a bracket counting argument shows that no subformula other the whole of $(X_a \star X_{a'})$ can also include that very same occurrence of the main connective $\star$.