 Moreover, Dyson and Kreisel [1961] showed that if \(\mathbf{IQC}\) is weakly complete for Beth semantics (that is, if no unprovable sentence holds in every Beth model) then the following consequence of MP holds :  \[ \tag{GDK} \forall \alpha_{B(\alpha)} \neg \neg \exists x R(\alpha, x) \rightarrow \neg \neg \forall \alpha_{B(\alpha)} \exists x R(\alpha, x),\]  where \(x\) ranges over all natural numbers, \(\alpha\) ranges over all infinite sequences of natural numbers, \(B(\alpha)\) abbreviates \(\forall x (\alpha(x) \leq 1),\) and \(R\) expresses a primitive recursive relation of \(\alpha\) and \(x.\) Conversely, GDK entails the weak completeness of \(\mathbf{IQC}.\) This interesting principle, considered as a schema with \(R\) required to be quantifier-free, would justify the negative interpretation of a form of Brouwer’s Fan Theorem. It is weaker than MP but unprovable in current systems of intuitionistic analysis. Kreisel [1962] suggested that GDK may eventually be provable on the basis of as yet undiscovered properties of intuitionistic mathematics.