Конструктивная арифметика. Пожалуйста, помогите решить.

[kochnevd]

Здравствуйте! Помогите, пожалуйста, решить задачу.

Может ли быть невыводимо в конструктивной арифметике утверждение $\forall x(\neg \neg\exists y B(x,y)\Rightarrow\exists y B(x,y))$ где $ B(x, y)$ разрешимое свойство, то есть $ \forall x,y(\neg B(x,y) \vee B(x,y)) $ выводимо?

Заранее спасибо!

PS: можно решить построив миры Крипке.