If a formula $\varphi$ is independent of $p$, there is some $\varphi' \sim \varphi$ where $p$ does not occur in $\varphi'$

Show that if a formula $\varphi$ is independent of a propositional symbol $p$, then there exists a formula $\varphi'$ such that $\varphi' \sim \varphi$ and $$VOC(\varphi') = VOC(\varphi)\setminus \{ p\}$$ where $VOC(\psi)$ is the set of all propositional symbols that occur in $\psi$.

We say that a formula $\varphi$ is independent of a symbol $p$ is for every valuation $v$ we have that: $$[[\varphi]]^{v[p/\bot]} = [[\varphi]]^{v[p/\top]} = [[\varphi]]^v$$ that is, $[[\varphi]]^v$ does not depend on whether $v(p)=0$ or $v(p)=1$.

I am having some trouble trying prove this but I came up with a "possible proof" by induction.

For the base case, if $\varphi = \top$, then $VOC(\varphi) = VOC(\top) = 0$, and we can take $\varphi' = \varphi$ since $\varphi$ does not depend on any $p$. If $\varphi = \bot$ we can do just the same thing. Again, if $\varphi = p$, $\varphi$ depends on $p$ the hypothesis $\varphi$ does not depend on $p$ doesn't apply. Finally, if $\varphi = q$ and $q \neq p$, we can take $\varphi' = \varphi$.

Now, assume that $\varphi = \neg \psi$ and that $\varphi$ is independent of $p$. Then we must have that $\psi$ is independent of $p$ as well, and by induction hypothesis there is some $\psi' \sim \psi$ such that $VOC(\psi')=VOC(\psi) \setminus \{ p\}$. Then we take $\varphi ' = \neg \psi '$. This works, since $$VOC(\varphi) = VOC(\psi)$$ and $$VOC(\varphi') = VOC(\psi') = VOC(\psi) \setminus \{ p \} = VOC(\varphi) \setminus \{ p \}$$ Now, if $\varphi = \psi_2 \square \psi_2$ where $\square \in \{ \land, \lor, \rightarrow, \leftrightarrow \}$ and $\varphi$ is independent of $p$, then $\psi_1$ and $\psi_2$ must be independent of $p$. By induction hypothesis, there are some $\psi_1' \sim \psi_1$ and $\psi_2' \sim \psi_2$ such that $$VOC(\psi_1') = VOC(\psi_1)\setminus \{p\}$$ and $$VOC(\psi_2') = VOC(\psi_2) \setminus \{ p \}$$ In that case, we take $\varphi' = \psi_1' \square \psi_2'$ and check that it works. Since $$VOC(\varphi) = VOC(\psi_1) \cup VOC(\psi_2)$$ we have that \begin{align*} VOC(\varphi') &= VOC(\psi_1') \cup VOC(\psi_2') = \left( VOC(\psi_1) \setminus \{p \} \right) \cup \left( VOC(\psi_2) \setminus \{p \}\right)\\ & = \left( VOC(\psi_1) \cup VOC(\psi_2) \right) \setminus \{ p \}\\ & = VOC(\varphi) \setminus \{ p \} \end{align*} which ends the proof.

I would really thank someone who could point me out if I made any mistakes here and help me with a correct proof of the statement. Thank you in advance!

• Comment: for the base case, you cannot say $\varphi'=\varphi$ in case $\varphi=p$, because it is not true that $VOC(\varphi')=VOC(\varphi) \setminus \{ p \}$. The property simply hold because in case $\varphi=p$ the condition "$\varphi$ independent of $p$ does not apply. The reasoning must be "reused" for the missing case: $\varphi=q$ with $q \ne p$. – Mauro ALLEGRANZA Jun 20 '17 at 11:22
• @MauroALLEGRANZA Thank you! I've edited the post accordingly. – user313212 Jun 20 '17 at 12:08

It is not clear why, if $\varphi = \neg \psi$ is independent of $p$, $\psi$ is independent of $p$ as well. This is not trivial.

More pressingly: for the case where $\varphi = \varphi_1 * \varphi_2$ with $*$ any binary operator, you cannot say that if $\varphi$ is independent of $p$, then $\varphi_1$ and $\varphi_2$ are independent of $p$ as well. For example, take $\varphi = p \lor \neg p$. Then $\varphi$ is independent of $p$, but $p$ and $\neg p$ clearly are not!

This basically blocks the very induction you are trying to use, so I wouldn't use induction for this one at all. Instead:

To obtain $\varphi'$, replace all occurrences of $p$ in $\varphi$ with $\top$ (if you are allowed such a symbol as a statement (not a truth-value)), or $q \lor \neg q$ for some other variable $q$, for then we have for any $v$ that: $$[[\varphi']]^v=[[\varphi]]^{v[p/\top]} = [[\varphi]]^v$$

and clearly: $$VOC(\varphi') = VOC(\varphi) \setminus \{ p \}$$

• Thank you! I understand it now. For the $\neg$ case, I did the following. Suppose $\psi$ is not independent of $p$. Then there must be some valuation $v_0$ such that $[[\psi]]^{v_0[p/\bot]} \neq [[\psi]]^{v_0[p/\top]}$. But in that case: $$[[\neg \psi]]^{v_0[p/\bot]} = v_{\neg} \left( [[\psi]]^{v_0[p/\bot]} \right) \neq v_{\neg} \left( [[\psi]]^{v_0[p/\top]} \right) = [[\neg \psi]]^{v_0[p/\top]}$$ which contradicts the hypothesis that $\neg \psi$ is independent of $p$. Would this work? – user313212 Jun 20 '17 at 16:41
• Mmm and I can see in your example $\varphi_1 \lor \varphi_2$ how to construct $\varphi'$ to the first case, which is what I did. But I still don't know what my $\varphi'$ would be in the last two... – user313212 Jun 20 '17 at 16:51
• @user313212 OK, I figured that would follow fairly easily, so I didn;t even try to figure that out ... but maybe not! Let me think about this ... (nice problem by the way!!) – Bram28 Jun 20 '17 at 17:02
• @user313212 OK, I can already see that I didn't cover the cases for $\varphi_1 \lor \varphi_2$ correctly: If $\varphi_1$ is always true no matter the value of $p$, then the same is true for $\varphi$ as a whole, even if $\varphi_2$ is dependent on $p$ .... This also suggests that you really need to consider all binary operators separately :( .... [more thinking] ... – Bram28 Jun 20 '17 at 17:06
• @user313212 Yep! Indeed not as easy as I thought ... I did just give a nice inductive proof for your other question though .... :) .. but back to this one .. – Bram28 Jun 20 '17 at 17:12

Any propositional formula is equivalent to the disjunction of the conjunction of propositional variables or their negation. That is just look at the truth table and take the disjunction of the assignments which make the formula true. In case it is independent of $p$ they will now cancel out, for example

$$(q\wedge p)\vee(q\wedge \neg p)\equiv q.$$

• Thank you! But it seems difficult to generalize your argument for any formula. Also, I need to prove what you said that any formula is equivalent to the disjunction of the conjunction of propositional variables or their negation. But is there any flaw on my inductive proof? – user313212 Jun 20 '17 at 11:12