Provability of existential quantification in intuitionistic logics

The type inhabitation problem, in other terminology formula provability problem, in the second-order lambda calculus with existential quantifier and arrow will be proved during the talk to be undecidable, which contrasts with the result that the second-order lambda calculus with existential quantifier, conjunction and negation is decidable. The proof of the undecidability will be done with help of the tiling puzzle technique. In addition the picture of the complexity of provability for constructive logics will be shown.