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 witnesses u for (*),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 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(y1,...,yn) and B(k) are defined in first-order language of V[X].