 Kripke models and Beth models are powerful tools for establishing properties of intuitionistic formal systems; cf. Troelstra and van Dalen [1988], Smorynski [1973], de Jongh and Smorynski [1976], Ghilardi [1999] and Iemhoff [2001], [2005]. However, there is no purely intuitionistic proof that every sentence which is valid in all Kripke and Beth models is provable in \(\mathbf{IQC}.\) Following an observation by Gödel, Kreisel [1958] verified that the completeness of intuitionistic predicate logic for Beth semantics is equivalent to Markov’s Principle MP, which Brouwer rejected.