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