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
    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$.2012-04-27
  • 0
    What does "rank" mean here?2012-04-27
  • 0
    @ArturoMagidin: Please see my attempt in my original question post.
    @Chris Eagle: I'll add the definition to my original question post.
    2012-04-27
  • 0
    @Johann: You cannot ping two people in the same comment.2012-04-27
  • 0
    @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.2012-04-27
  • 0
    @Johann: And in order to prove that, you might want to remember/state explicitly your definition of "subformula"!2012-04-27
  • 0
    @ArturoMagidin: Thanks for your help. Updated my original question post. Still looks a little bit faulty..2012-04-27
  • 0
    @Johann: To answer your question: (i) You need to make the **induction** explicit: assume the result holds for all formulas of rank strictly smaller than $A$; since $\mathrm{rank}(C)\lt \mathrm{rank}(A)$, you can apply the assumption to $B$ when $B\in\mathrm{subf}(C)$. Similarly in the second step; but you can make that second step shorter and clearer: if $B\in\mathrm{subf}(C)$, then since $\mathrm{rank}(C)\lt\mathrm{rank}(A)$, by the induction hypothesis you have $\mathrm{rank}(B)\leq \mathrm{rank}(C) \lt\mathrm{rank}(A)$. Etc.2012-04-27
  • 0
    @ArturoMagidin: Thank's again for your help. I tried to explicitly state the induction now. I hope it's better now. I wonder if I can do the base case for atoms since they don't have strict subformulaes at all. Do I need a base case where there exist stric subformulaes?2012-04-27
  • 0
    @Johann: Of course you can do the base for atoms. You *must* do the base for atoms, otherwise you aren't proving anything. And yes, the result is true for atoms "by vacuity": the premise of the implication ("if $B$ is a strict subformula") is always false, so the implication is in fact true.2012-04-27
  • 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