0
$\begingroup$

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

  • 0
    @Johann: Your induction hypothesis is incorrect as stated: since $A'\in\mathrm{subf}(A')$, you do't want to conclude that $B\in\mathrm{subf}(A')$ implies $\mathrm{rank}(B)\lt\mathrm{rank}(A')$. You need "$B\in\mathrm{subf}(A')\text{ and }B\neq A'". (And in my experience, it's better to state the induction hypothesis as an "IF `xxx` THEN `yyy`" rather than as "`yyy` for `xxx`." Less chance of an error, and clearer that we are assuming an implication, not a "fact".2012-04-27

1 Answers 1

2

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.