This extracts a simple case from a cross-post at cs.SE.
Here is a fact about Intuitionistic Propositional Logic:
A formula $p$ is equivalent to a formula of the form $q \lor \neg q$ if and only if $\neg p$ is false.
This can be reformulated in algebraic semantics:
For any Heyting algebra $H$ and any element $p\in H$, there exists a $q\in H$ with $p=q\lor\neg q$ if and only if $\neg p=\bot$ (the bottom element of $H$).
This eliminates an existential quantifier, in the sense of finding an equivalent condition on $p$ which does not involve any "there exists" statement.
This leads to the question that interests me:
Given a pair of elements $p,p'$ in a Heyting algebra $H$, when can they be written as $p=q\lor\neg q$ and $p'=q'\lor\neg q'$ with $q\land q'=\bot$?
Is it possible to eliminate existential quantifiers here too?
Much later -- update: a still simpler similar question which I also do not know anything about.
Can one eliminate the existential quantifier from the following formula (in the language of Heyting algebras): $$ \exists x\ p = (q\land x)\lor\neg(q\land x) $$
