ABSTRACT. Intuitionistic logics are very useful in practise, they are for example valuable for proof assistants. Nevertheless, they have been regarded controversial. David Hilbert wrote that: "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists."[5] Indeed, this property of intuitionistic logic may cause problems when trying to embed them in higher-order logic. The talk will give a short overview about this challenge and discuss possible solutions.