rank of subformulae

How to show that the rank of a strict subformulae is strictly less than the rank of the formula in propositional logic?

I can "see" that it is true, but how to strictly show it?

I don't now how to apply the induction principle to show this.

The definition of rank is

• $\mathrm{rank}(A) = 0$ if $A \in \mathrm{ATM}$
• $\mathrm{rank}(\lnot A) = \mathrm{rank}(A) + 1$
• $\mathrm{rank}(A \circ B) = \max(\mathrm{rank}(A),\mathrm{rank}(B)) +1$

Let $A \in \mathrm{PROP}$ and $B \in \mathrm{subf}(A)$ but $A \neq B$, then $\mathrm{rank}(B) < \mathrm{rank}(A)$.

Proof:

Let $A \in \mathrm{PROP}$. Induction on $\mathrm{rank}(A)$.

Base case.

$\mathrm{rank}(A) = 0$. Then $A \in \mathrm{ATM}$ and there's no strict subformulae of $A$. Done here.

Assumption.

$\mathrm{rank}(B) < \mathrm{rank}(A')$ for $A' \in \mathrm{PROP}$, $\mathrm{rank}(A') < \mathrm{rank}(A)$ and $B \in \mathrm{subf}(A')$.

Conclusion.

If $A = \lnot C$ for some $C \in \mathrm{PROP}$, then $\mathrm{subf}(A) = {A} \cup \mathrm{subf}(C)$. Since $A \neq B$ should hold on, it's $B \in \mathrm{subf}(C)$.
If either $B = C$ or $B \in \mathrm{subf}(C)$ by assumption and definition of $\mathrm{rank}$ it holds that $\mathrm{rank}(B) \leq \mathrm{rank}(C) < \mathrm{rank}(A) = \mathrm{rank}(C) +1$.

If $A = C \circ D$ for some $C,D \in \mathrm{PROP}$, then $\mathrm{subf}(A) = {A} \cup \mathrm{subf}(C) \cup \mathrm{subf}(D)$. Since $A \neq B$ should hold on, it's $B \in \mathrm{subf}(C) \cup \mathrm{subf}(D)$.
If $B = C$, $B = D$, $B \in \mathrm{subf}(C)$ or $B \in \mathrm{subf}(D)$ by assumption and definition of $\mathrm{rank}$ it holds that $\mathrm{rank}(B) \leq \max(\mathrm{rank}(C),\mathrm{rank}(D)) < \mathrm{rank}(A) = \max(\mathrm{rank}(C),\mathrm{rank}(D))+1$.

-
Show it is true for atoms; then show that if it is true for formulas $P$ and $Q$, then it is true for $\neg P$, $P\land Q$, $P\lor Q$, and $P\to Q$. – Arturo Magidin Apr 27 '12 at 15:53
What does "rank" mean here? – Chris Eagle Apr 27 '12 at 15:57
@ArturoMagidin: Please see my attempt in my original question post.<br>@Chris Eagle: I'll add the definition to my original question post. – Johann Jokum Apr 27 '12 at 16:02
@Johann: You cannot ping two people in the same comment. – Arturo Magidin Apr 27 '12 at 16:10
@Johann: Prove that if $A=B\circ C$ and $D$ is a subformula of $A$, then either $D=B$, $D=C$, or $D$ is a subformula of either $B$ or $C$. Then use induction by assuming the conclusion holds for $B$ and for $C$ already. – Arturo Magidin Apr 27 '12 at 16:10

The problem right now is that you are actually trying to do an induction argument without saying you are doing an induction argument. That's why it seems like you are using the proposition to prove the proposition.

In order to make the induction come to the fore and clarify the argument, you should make that induction explicit:

You prove the result for atoms, which are the only formulas of rank $1$.

For the next step, assume that the result holds for all formulas of rank strictly less than $n$, and assume that $\mathrm{rank}(A)=n$.

If $A=\neg C$, then $\mathrm{rank}(A) = \mathrm{rank}(C)+1$, so we know (by the induction hypothesis) that the proposition holds for $C$. Since $B\in\mathrm{subf}(C)$, then either $B=C$ (and then $\mathrm{rank}(B)=\mathrm{rank}(C)\lt\mathrm{rank}(A)$) or else $B$ is a strict subformula of $C$ and so, by the induction hypothesis, $\mathrm{rank}(B)\lt\mathrm{rank}(C)\lt\mathrm{rank}(A)$, so $\mathrm{rank}(B)\lt\mathrm{rank}(A)$, as desired.

A similar argument works with $A=C\circ D$: we know that $\mathrm{rank}(C),\mathrm{rank}(D)\leq\max(\mathrm{rank}(C),\mathrm{rank}(D))\lt\mathrm{rank}(A)$, so the induction hypothesis applies to both $C$ and $D$. If $B\in\mathrm{subf}(C)$, then either $B=C$ or $\mathrm{rank}(B)\lt\mathrm{rank}(C)$ by the induction hypothesis applied to $C$; and similarly if $B\in\mathrm{subf}(D)$. Thus, if the proposition holds for all formulas of rank less than the rank of $A$, then it holds for $A$.

Inductively, this proves the proposition for all formulas.

-