# Complexity of entailment between equivalences of dual formulas

Consider a propositional language over the set of propositional variables $$\{p^+,p^-,q^+,q^-,\ldots\}$$ and connectives $$\{\wedge,\vee,\rightarrow,\equiv\}$$ (conjunction, disjunction, implication, equivalence). We call a formula $$\phi$$ monotone if it only contains $$\wedge$$ and $$\vee$$. Additionally, we call $$\phi^\partial$$ the dual of $$\phi$$ if all $$\wedge$$'s are swapped for $$\vee$$'s (and vice versa) and all $$p^+$$'s with $$p^-$$'s (and vice versa).

E.g., $$p^+\wedge(q^-\vee p^-)$$ is dual to $$p^-\vee(q^+\wedge p^+)$$.

Now let $$\phi$$ and $$\chi$$ be two monotone formulas. What is the complexity of determining whether the following formula is valid in classical logic? $$(\phi\equiv\phi^\partial)\rightarrow(\chi\equiv\chi^\partial)$$

It seems that it should be in $$\mathsf{coNP}$$ but showing hardness turned out to be not straightforward — I did not find a reduction from the classical validity…

• What do you mean by the last part about reduction from classical validity? Feb 27 at 3:42
• Given a classically valid formula $\psi$, construct an instance of the problem above that has a positive solution iff $\psi$ is valid. But it does not have to be a reduction from validity specifically. Anything will do: I only care about the complexity evaluation. Feb 27 at 6:39