Complexity of Intuitionistic Predicate Logic with One Variable
Maarten Marx

Abstract:
The validity problem for intuitionistic predicate logic with one
variable is complete for the class of co--nexptime problems. This
result holds for both constant and for expanding domains.  The upper
bound follows because every refutable formula can be refuted in a
Kripke model whose size is exponential in the length of the
formula. The lower bound is obtained by an encoding of the square
tiling problem.

Keyword(s): Intuitionistic logic, complexity, nexptime