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 '14 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$ – Garth Marenghi Apr 7 '14 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 '14 at 20:31

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$ – Garth Marenghi Apr 7 '14 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 '14 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$ – Garth Marenghi Apr 7 '14 at 20:43
  • $\begingroup$ @GarthMarenghi Glad I could help. These tricks come with experience. $\endgroup$ – Git Gud Apr 7 '14 at 20:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.