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].