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,\ldots,y_n)$ be an $B(T)$-free algebra as it is defined in [2], where $B(T)$ is the equational class of all finite heyting algebras with unary opertors from the finite partial order set $T$.

Since $B(T)$ is first-order definable then $B(T)$ is in $V^{X}$.

We have a decision problem,

$$"V^{X}\Vdash_{u} T[v_1,\ldots,v_n] "\label{*}\tag{*}$$

Where $\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 $T(y_1,\ldots,y_n)$,$y_1,\ldots, y_n$ are variables and $v_1,\ldots,v_n$ are sets of codified sentences from the $V^{X}$-language .

I think \eqref{*} is a decision problem for two reasons,

1. First, $B(T)$ is equivalent to an algebraic variety generated by the algebra $\{0,1\}(T)$, ([2], Theorem 10, p. 8).

2. Second, any finite free algebra of $B(T)$ is a Boolean product of $\{0,1\}(T)$-subalgebras,([2] Corollary 16, p. 11).

My first question is this: are these hypotheses sufficient to find a function $$ f:\{0,1\}^\ast\to \{\mathrm{yes,no}\} $$ to make \eqref{*} a decision problem?

My second question is this: since the Heyting algebras are models for intuitionistic logic, could we say that \eqref{*} is equivalent to the decision problem of intuitionistic logic, which is pspace-complete?.

References

[1]. Benavides, John, "Sheaf logic, Quantum set theory and the interpretation of Quantum Mechanics", arxiv 1111.2704 (2011).

[2]. Sanjuan, Eric, "Heyting algebras with Boolean operators for rough sets and information retrieval applications", Discrete Applied Mathematics 156, No. 6, 967-983 (2008), MR2395615, ZBL1134.06007.

Note:- $T(y_1,\ldots,y_n)$ and $B(T)$ are defined in the first-order language of $V^{X}$. $T$ in $T(y_1,\ldots,y_n)$ is different from $T$ in $B(T)$. $T(y_1,\ldots,y_n)$ is a first-order set theory sentence about the $B(T)$-free algebra on $T$.