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

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.