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(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 this first-order set theory sentence 

$$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 choice of the truth witnesses u for (*),Where $y_1,\cdots,y_n$ are variables and $v_1,\cdots,v_n$ are elements of $V[X]$.

I think (*)is a decision problem for two reasons,

First,$B(T)$is equivalent to algebraic variety generated by the algebra {0,1}(T),(Theorem10,page8,[2]).

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

My first question,is this enough to fined a function f:{0.1}* -->{yes,no} to make (*) decision problem?.


My second 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]$.$T$in $T(y_1,\cdots,y_n)$ is deferent from $T$ in $B(T)$.$T(y_1,\cdots,y_n)$ is a first-order set theory sentence about $B(T)$-free algebra on $T$.