Prove that $\text{len}(q^*) \le 3\text{len}(q) -2$

Prove by induction where q is a formula in proposition logic:

$$\text{len}(q^*) \le 3\text{len}(q) -2$$

Where the star property (*) is defined as follows:

$$\text{atom}^* = \text{atom}$$ $$(\neg(q))^*= \neg(q^*)$$ $$(w \land x)^* = \neg (\neg w^* \lor \neg x^*)$$

The function Len gives the total number of connectives + the number of proposition letters in a formula.

My proof up till now, here for atoms:

$$\text{len}(q^*) \le 3\text{len}(q) - 2$$ $$\text{len}(q) \le 3\text{len}(q) - 2$$ $$1 \le 1$$

And here for conjunction:

$$\text{len}((q \land w)^*) \le 3\text{len}(q \land w) - 2$$ $$\text{len}( \neg(\neg w^* \lor \neg x^*)) \le 3(\text{len}(q) + \text{len}(w) + 1) -2$$ $$\text{len}(w^*) + len (q^*) + 4 \le 3(\text{len}(q) + \text{len}(w) + 1) -2$$

Is this correct or sufficient? Any recommendations? I have no idea how to solve the last inequality.

Edit: As pointed out in the comments, a self contained proof would have been better than just finishing what Ferengi Godfried started and pointing out that the last part can be done in the same way. So here is a full, self-contained proof.

Answer: We have to prove by induction that for a formula $q$ in propositional logic which consists only of atoms, negation and conjunction (since the $^*$-operator is only defined for atoms, $\wedge$ and $\neg$), the following inequality holds:

$$\text{len}(q^*) \leq 3\text{len}(q) - 2\qquad (1)$$

The induction is on $\text{len}$ of the formula $q$ (i.e. on the number of connectives $\wedge$ and $\neg$ plus the number of atoms in $q$) and has three steps, the base case (where $q$ is an atom) and then two induction steps for negation and conjunction.

Atoms: According to the definition of the $^*$-operator, we have $q^* = q$ for every atom $q$. Using $\text{len}(q) = 1$ for atoms, the inequality follows straightforward:

$$\text{len}(q^*) = \text{len}(q) = 1 \leq 1 = 3\text{len}(q) - 2$$

Negation: For negation, we have $(\neg q)^* = \neg(q^*)$ for a formula $q$. Noting that

$$3\text{len}(\neg q) - 2 = 3(\text{len}(q) + 1) - 2 = 3\text{len}(q) + 1 \qquad (2)$$

we have

$$\text{len}((\neg q)^*) = \text{len}(\neg(q^*)) = \text{len}(q^*) + 1 \leq 3\text{len}(q) - 2 + 1 \leq 3\text{len}(\neg q) - 2$$

The induction hypothesis $(1)$ was used at the first inequality and $(2)$ at the second.

Conjunction: Again by definition, we have $(w \wedge x)^* = \neg(\neg w^* \vee \neg x^*)$ for formulas $w$ and $x$. Since

$$3\text{len}(w \wedge x) - 2 = 3(\text{len}(w) + \text{len}(x) + 1) - 2 = 3\text{len}(w) + 3\text{len}(x) + 1 \qquad (3)$$

and

$$\text{len}((w \wedge x)^*) = \text{len}(\neg(\neg w^* \vee \neg x^*)) = \text{len}(w^*) + \text{len}(x^*) + 4 \qquad (4)$$

we have

$$\text{len}((w \wedge x)^*) = \text{len}(w^*) + \text{len}(x^*) + 4 \leq 3\text{len}(w) - 2 + 3\text{len}(x) - 2 + 4 \leq 3\text{len}(w \wedge x) - 2$$

Again, $(4)$ was used at the first equality, the induction hypothesis $(1)$ at the first inequality, and $(3)$ at the second equality.

We have proven that the inequality holds for atoms, negation and conjunction, what means that we are finished.

• -1 a complete, self contained proof woul be fine – miracle173 Jul 9 '16 at 4:52
• @miracle173 Here you go. I couldn't understand why though, I have finished what Ferengi Godfried started for conjunction, and pointed out that the part that was left could be proved in the exact same way, a good exercise after providing the solution for conjunction. Overall, the answer got upvoted and accepted, so I guess it was ok for Ferengi Godfried, and I'm sure that he would have written a comment if he couldn't solve the last part. – user331406 Jul 9 '16 at 10:07
• Yes indeed it was already clear. Thanks for your help. – Ferengi Godfried Jul 9 '16 at 18:37
• thank you for your edit. I turned the downvote to an upvote. I have the following questions: 1. I can't see why functional completeness does matter in this proof? can you explain? 2. The proof is by induction on what? – miracle173 Jul 10 '16 at 17:26
• @user331406: 1. functional completeness does not make sense here. It is a question about formulas (true or false or undefined) and not about true sentences of propositional logic. It also does not make sense to say you have shown it for arbitrary formulas because the * function is not defined for arbitrary formulas. And if one would define it for other operators, too, functional completeness would not help to show that the inequality is true for those other operators. – miracle173 Jul 11 '16 at 4:28