Let $V[X]$ be a sheaf model of ZF set theory, where $X$ is a topological space as it is defined in [1].

Let $T(y_1,\cdots,y_n)$ be an $B(k)$-free algebra as it is defined in [2], where $B(k)$ is the equational class of all finite heyting algebras with unary opertors from the finite partial order set $k$.

Since $B(k)$ is first-order definable then $B(k)$ is in $V[X]$.

We could define this decision problem as the following:

$$V[X]\Vdash_{u} T[v_1,\cdots,v_1] \qquad(*)$$

$\Vdash_{u}$ is the satisfaction relation of the sheaf model $V[X]$ and $u$ is an open subset of $X$, which is a truth witness of (*).

The decision problem here is the search for the truth witnesses u for (*),Where $y_1,\cdots,y_n$ are variables and $v_1,\cdots,v_n$ are elements of $V[X]$.

My question is this, Since the Heyting algebras are models for intuitionistic logic, could we say that, (*) is equivalent to the decision problem of intuitionistic logic, which is pspace-complete?.

[1]. Sheaf logic,Quantum set theory and the interpretation of Quantum Mechanics, J.benavides arxive 1111.2704.

[2]. Heyting algebras with Boolean operators for rough sets and information retrieval application, EricSanjuan.

Note:- $T(y_1,\cdots,y_n)$ and $B(k)$ are defined in first-order language of $V[X]$.