propositional formulas: how to find the equivalence of two linked formulas?

Question

Most of the time, the equivalence between two formulas is shown when they are just a refactoring form of each other, e.g., is it equal

$(p \rightarrow q) \equiv (\neg p \vee q)$

In this example, both formulas have the same variable names.

My question is: if

$ \phi_a = (m \wedge p) \vee (m \wedge q)$ ,

$\phi_b = (x \vee y) \wedge z$ ,

knowing that $\phi_c = (p \leftrightarrow x) \wedge (q \leftrightarrow y)\wedge (m \leftrightarrow z)$

How to cheeck whether $\phi_a \equiv \phi_b$ ?

One way that I am trying is to substitute the variables from $\phi_c$ to either $\phi_a$ or to $\phi_b$. But, does it make sense if I try simply $\phi_a \wedge \phi_b \wedge \phi_c$ ? When I am trying this in a solver, it is generating the same set of models with $\phi_a$ and $\phi_b$, just twice longer (including the variables from both formulas).

So, am I acting correctly? If not, what I should do?

Answer 1

Yes, you have the right idea. The relevant equivalence is:

Substitution Equivalence

Where $S(\phi)$ is some formula that contains formula $\phi$ as a component part (possibly multiple times), and where $S(\psi)$ is the sentence that results from replacing any of the formulas $\phi$ with formula $\psi$, then:

$S(\phi) \land (\phi \leftrightarrow \psi) \Leftrightarrow S(\psi) \land (\phi \leftrightarrow \psi)$

So in your case, you can start with $\phi_a \land \phi_c$ and then proceed as follows:

$\phi_a \land \phi_c =$

$((m \land p) \lor (m \land q)) \land ((p \leftrightarrow x) \land (q \leftrightarrow y) \land (m \leftrightarrow z)) \Leftrightarrow$

$((m \land (p \lor q)) \land ((p \leftrightarrow x) \land (q \leftrightarrow y) \land (m \leftrightarrow z)) \Leftrightarrow$

$(m \land (p \lor q)) \land (p \leftrightarrow x) \land (q \leftrightarrow y) \land (m \leftrightarrow z) \Leftrightarrow$ (and now you use it!)

$(z \land (x \lor y)) \land (p \leftrightarrow x) \land (q \leftrightarrow y) \land (m \leftrightarrow z) \Leftrightarrow$

$((x \lor y) \land z) \land ((p \leftrightarrow x) \land (q \leftrightarrow y) \land (m \leftrightarrow z)) =$

$\phi_b \land \phi_c$

So note: it is not the case that$ \phi_a \Leftrightarrow \phi_b$, but you do have that $\phi_a \land \phi_c \Leftrightarrow \phi_b \land \phi_c$

So you can't say that $\phi_a$ and $\phi_b$ are equivalent, but you can say that within the context of $\phi_c$, $\phi_a$ and $\phi_b$ say the same thing.