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(y1,...,yn) 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 finit 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]||-u- T[v1,...,v1] (*)
(Sorry I do not know how to type mathematical formula in Latex).

||-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 values for (*),

    y1=v1,...,yn=vn
Where y1,...,yn are variables and v1,...,vn 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 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.

Notes:- T(y1,...,yn) and B(k) are defined in first-order language of V[X].