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…

  • $\begingroup$ What do you mean by the last part about reduction from classical validity? $\endgroup$
    – PW_246
    Feb 27 at 3:42
  • $\begingroup$ 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. $\endgroup$ Feb 27 at 6:39


You must log in to answer this question.

Browse other questions tagged .