Variable elimination for propositional formulas in Heyting algebras

Question

By an (intuitionistic) propositional formula $\varphi(x_1,\ldots,x_n)$ I mean a formula built up from a (finite) number of variables $x_1,\ldots,x_n$ using connectors $\top, \bot, \land, \lor, \Rightarrow$. Given such a formula $\varphi(x_1,\ldots,x_n)$, given a Heyting algebra $H$ and elements $u_1,\ldots,u_n \in H$ we can evaluate $\varphi(u_1,\ldots,u_n)$ in the obvious way (resulting in an element of $H$).

Given a propositional formula $\varphi(t,x_1,\ldots,x_n)$, I would like to know if $\bigwedge_t \varphi(t,x_1,\ldots,x_n)$ and $\bigvee_t \varphi(t,x_1,\ldots,x_n)$, which are evaluated in a complete Heyting algebra $H$ as the inf, resp. sup, of all values of $\varphi(t,x_1,\ldots,x_n)$ where $t$ ranges over $H$, i.e., by quantifying over truth values, can be rewritten (by eliminating the $\bigwedge$ or $\bigvee$ quantified variable $t$) as a propositional formula in $x_1,\ldots,x_n$ and possibly other variables $p_1,\ldots,p_m$ depending on $H$ (but on nothing else). More precisely:

Question: is it true that for any propositional formula $\varphi(t,x_1,\ldots,x_n)$ there exist propositional formulae $\varphi^\wedge(x_1,\ldots,x_n,p_1,\ldots,p_m)$ and $\varphi^\vee(x_1,\ldots,x_n,p_1,\ldots,p_m)$ (for some $m$) such that, for any complete Heyting algebra $H$ there exist $p_1^H,\ldots,p_m^H \in H$ such that, for all $u_1,\ldots,u_n \in H$, the following hold?

• $\bigwedge_{v\in H} \varphi(v,u_1,\ldots,u_n) = \varphi^\wedge(u_1,\ldots,u_n,p_1^H,\ldots,p_m^H)$

• $\bigvee_{v\in H} \varphi(v,u_1,\ldots,u_n) = \varphi^\vee(u_1,\ldots,u_n,p_1^H,\ldots,p_m^H)$

Comments:

• Unless I am mistaken, the analogous question for Boolean algebras is easily seen to have a positive answer (rewrite $\varphi(t,\underline{x})$ as $(a(\underline{x})\land t) \oplus b(\underline{x})$ for propositional formulas $a(\underline{x}), b(\underline{x})$, and then $\bigwedge_t\varphi(t,\underline{x})$ is $b(\underline{x}) \land \neg a(\underline{x})$ while $\bigvee_t\varphi(t,\underline{x})$ is $a(\underline{x}) \lor b(\underline{x})$).

• As an example, if $\varphi(t,x) := (t\Rightarrow x)$, then $\varphi^\wedge(x) = x$ and $\varphi^\vee(x) = \top$. On the other hand, if $\varphi(t,x) := (x\Rightarrow t)$, then $\varphi^\wedge(x) = \neg x$ and $\varphi^\vee(x) = \top$. (More generally, for any $\varphi$ that is order-preserving in $t$, we get $\varphi^\wedge$ and $\varphi^\vee$ by substituting $\bot$ and $\top$ respectively for $t$, and for any $\varphi$ that is order-reversing, $\top$ and $\bot$.)

• The possible need for extra parameters $p_1,\ldots,p_m$ is illustrated by taking $\varphi(t) := t\lor\neg t$, in which case $\bigwedge_t \varphi(t)$ is the truth value of LEM in $H$, which certainly depends on $H$ (so we can't write it as a propositional formula of zero variable).

• If the answer to my question is negative, I would appreciate a pointer to literature, if there is any, on the class of formula obtained by closing the propositional variables by the propositional connectors and the quantifiers $\bigwedge,\bigvee$ ranging over propositional variables.

Answer 1

The answer for $\bigwedge_t$ is no. Perhaps the idea here can be adapted to $\bigvee_t$.

Consider the propositional formula $t \vee (t \to x)$ in the complete Heyting algebra of open subsets of $\mathbb{R}$.

Claim. For any open set $U \subseteq \mathbb{R}$, $\bigwedge_t t \vee (t \to U)$ is the set $U^\bullet := \{r \in \mathbb{R} : r \in U\text{ or }r\text{ is isolated in }\mathbb{R} \setminus U\}$.

Proof of claim. Clearly if $r \in U$, then $r \in (t \vee (t \to U))$ for any open set $t$. If $r$ is isolated in $\mathbb{R}\setminus U$, then for any open set $t$, we either have that $r \in t$ or $(\mathbb{R} \setminus t) \cup U$ contains a neigbhorhood of $r$. Conversely, if $r\notin U$ but $r$ is also not isolated in $\mathbb{R} \setminus U$, then $r \notin ((\mathbb{R} \setminus \{r\}) \vee ((\mathbb{R} \setminus \{r\}) \to U))$.

So now consider some propositional formula $\varphi(x,\bar{p})$. We need to show that this fails to be equal to $\bigwedge_{t} t \vee(t \to x)$ for all open sets $x$. Since there are only finitely many open sets in the tuple $\bar{p}$, we can find a non-empty open set $U \subseteq \mathbb{R}$ such that for each $i < |\bar{p}|$, either $U\wedge p_i = U$ or $U \wedge p_i = \bot$. For each $i < |\bar{p}|$, let $q_i = \top$ if $U \wedge p_i = U$ and let $q_i = \bot$ if $U \wedge p_i = \bot$. We now have that for any open $V$, $U \wedge \varphi(V,\bar{p}) = U \wedge \varphi(V,\bar{q})$.

Let $F$ be a closed subset of $U$ that is homeomorphic to Cantor space plus a single isolated point. Let $r$ be the single isolated point of $F$. Let $V = \mathbb{R} \setminus F$. Clearly we have that $V^\bullet = V \cup \{r\}$.

Claim. $U\wedge \varphi(V,\bar{q})$ is either $U$, $U \wedge V$, or $\bot$.

Proof of claim. We prove this by induction on propositional formulas in the single variable $x$ (i.e., we prove that for any propositional formula $\psi(x)$, $U \wedge \psi(V) \in \{U,U \wedge V,\bot\}$). Clearly we have that the statement is true for $U \wedge \bot = \bot$, $U \wedge \top = U$, and $U \wedge x$ (which is $U \wedge V$ when $x=V$).

If the statement is true for two propositional formulas $\psi(x)$ and $\chi(x)$, then it's easy to check that the statement is true for $\psi(x) \wedge \chi(x)$ and $\psi(x) \vee \chi(x)$. This just leaves $\psi(x) \to \chi(x)$. If $U \wedge \psi(V) = \bot$ or $U \wedge \chi(V) = U$, then $U \wedge (\psi(V) \to \chi(V)) = U \in \{U,U \wedge V,\bot\}$. If $U \wedge \psi(V) = U$, then $U \wedge (\psi(V) \to \chi(V)) = \chi(V) \in \{U,U \wedge V,\bot\}$. Finally, if $U \wedge \psi(V) = U \wedge V$ and $U \wedge \chi(V) $ is $U$ or $U \wedge V$, then $U \wedge ( \psi(V) \to \chi(V)) = U \wedge V \in \{U,U \wedge V,\bot\}$. So in every case, we have that $U \wedge (\psi(V) \to \chi(V)) \in \{U,U \wedge V, \bot\}$. Therefore, by induction, the same is true for $U \wedge \varphi(V,\bar{q})$.

Finally, note that $U \wedge V^\bullet \notin \{U,U\wedge V, \bot\}$, whence $\varphi(V,\bar{p}) \neq V^\bullet = \bigwedge_t t \vee (t \to V)$.

Since we can do this for any formula $\varphi(x,\bar{p})$, we have that $\bigwedge_t t \vee (t \to V)$ is not equal to any propositional formula with parameters.