I have two inductively defined operations:

  1. $\text{bin}$

    base case:

    If $p$ is a propositional letter, then $\text{bin}(p) = 0$

    inductive step

    $\text{bin}(\neg \phi) = \text{bin} (\phi)$

    $\text{bin}(\phi \wedge \psi) = \text{bin}(\phi) + \text{bin}(\psi) + 1$

    $\text{bin}(\phi \vee \psi) = \text{bin}(\phi) + \text{bin}(\psi) + 1$

    $\text{bin}(\phi \rightarrow \psi) = \text{bin}(\phi) + \text{bin}(\psi) + 1$

    $\text{bin}(\phi \leftrightarrow \psi) = \text{bin}(\phi) + \text{bin}(\psi) + 1$

  2. $S$, which is defined as

    $S(p) = \emptyset$

    $S(\neg \phi) = S(\phi)$

    $S(\phi \square \psi) = S(\phi) \cup S(\psi) \cup \{\phi, \psi\}$ where $\square$ can be $\wedge, \vee, \rightarrow or\leftrightarrow$

The inductive proof I have to give: Let bin($\phi$) be equal to the number of binary connectives in $\phi$, and |V| the number of elements of the set V.

Prove with induction that the following inequality holds for every propositional formula $\phi$: |S($\phi$)| $\leq$ 2 $\cdot$ bin($\phi$).

For the base case, I have the following:

Base case:

If $\phi$ is an atomic propositional formula, then bin($\phi$) = 0 and |S($\phi$)| = |$\emptyset$| = 0, and so |S($\phi$)| $\leq$ 2 $\cdot$ bin($\phi$) holds.

Inductive step:

I have no idea how to tackle this, but I have to prove for negation and for the binary connectives.

I would say I would start with:

"Assume the inductive hypothesis is true, i.e., |S($\phi$)| $\leq$ 2 $\cdot$ bin($\phi$) is true", or, maybe better, "Assume the property holds for formulas $\phi$ and $\psi$"

Then, case negation: S($\neg \phi$) = S($ \phi$) and bin($\neg \phi$) = bin($ \phi$), and therefor the property holds for $\neg \phi$

Then, case conjunction: bin($\phi \wedge \psi$) = bin($\phi$) + bin($\psi$) + 1, and S($\phi \wedge \psi$) = S($\phi$) $\cup$ S($\psi$) $\cup$ {$\phi$, $\psi$}.

Now, what I think I see is that with the operation bin 1 gets added, and with S *two* elements are added to the set. I just don't know how to formulate this nicely.

  • $\begingroup$ I'm not sure, but I think the induction tag does not fit the kind of induction you're doing here. It seems to be used only for mathematical induction and transfinite induction. $\endgroup$
    – Git Gud
    Apr 7, 2014 at 19:57
  • $\begingroup$ @git-gud I'm not a native English speaker, I was actually looking for something along the lines of "inductive proof" but could not find it. I took induction instead since the proof is done with induction. $\endgroup$ Apr 7, 2014 at 20:28
  • $\begingroup$ There are different kinds of induction. The one used in here one of them, and it is induction, just not the kind the tag is for, I think. $\endgroup$
    – Git Gud
    Apr 7, 2014 at 20:31

1 Answer 1


I'm not sure I understand what you want, but here it goes: suppose that $\left|S(\phi)\right|\leq 2\text{bin}\left(\phi\right)$ and $\left|S(\psi)\right|\leq 2\text{bin}\left(\psi\right)$ both hold. Let $\square$ denote an arbitrary binary connective.

The goal is to prove that $\left|S\left(\phi \square \psi\right)\right|\leq 2\text{bin}\left(\phi \square \psi\right)$. Note the following: $$\begin{align} \left|S\left(\phi \square \psi\right)\right|&=\left|S(\phi)+S(\psi)+\{\phi, \psi\}\right| &\text{Definition of }S\\ &\leq \left|S(\phi)\right|+\left|S(\psi)\right|+\left|\{\phi, \psi\}\right| &\text{Inclusion Exclusion Principle}\\ &\leq 2\text{bin}\left(\phi\right)+2\text{bin}\left(\psi\right)+2 &\text{Inductive Hypothesis}\\ &=2\left(\text{bin}\left(\phi\right)+\text{bin}\left(\psi\right)+1\right) &\text{Distributitivy of} + \text{over}\cdot\\ &=2\left(\text{bin}\left(\phi \square \psi\right)\right)&\text{Part 1}. \end{align}$$

This concludes the induction.

  • $\begingroup$ The goal was to prove that the property $\left|S(\phi)\right|\leq 2 \cdot \text{bin}\left(\phi\right)$ holds. So I had to do it for the base case, and then for the inductive step where I show negation and the cases for binary operators. I think as far I can see that you got that right. $\endgroup$ Apr 7, 2014 at 20:21
  • $\begingroup$ @GarthMarenghi Yes, that's what I interpreted. You did the base case and the negation, I did the rest. $\endgroup$
    – Git Gud
    Apr 7, 2014 at 20:21
  • $\begingroup$ well, I also had the idea for the binary connectives, but I have a hard time putting these ideas to paper. E.g.: the third and and fourth lines of your proof (inclusion exclusion using that to get from = to <= and the inductive hypothesis with the + 2 on the end), I would not have been able to come up with that. $\endgroup$ Apr 7, 2014 at 20:43
  • $\begingroup$ @GarthMarenghi Glad I could help. These tricks come with experience. $\endgroup$
    – Git Gud
    Apr 7, 2014 at 20:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .