In March 1973, W. Veldman [1] discovered that, by a slight modification of a Kripke-model, it was possible to give an intuitionistic proof of the completeness-theorem for the intuitionistic predicate calculus (IPC) with respect to modified Kripke models. The modification was the following: Let f represent absurdity, then we allow the possibility that and we agree that, for all sentences ϕ, , if . Just one modified Kripke model is constructed such that validity in implies derivability in IPC. While usually one thinks of as some subset of ⋃ n Nat n and of as the discrete natural ordering in ⋃ n Nat n, in Veldman's model , is a spread and , where Γα and Γβ are sets of sentences associated with α, resp. β, is a nondiscrete ordering.

In the completeness-proofs, both for Beth and for Kripke models that we present here, we consider only models over ⋃n Nat n, with the natural discrete ordering and we need validity in all models, not just in one, to get derivability in IPC. Also we have to modify the definition of a model in a somewhat different way than Veldman did. We agree that if ∨s[M⊨s f], then M⊨sϕ for each s ∈ ⋃n Nat n and for each sentence ϕ.

One can view a single model of the type constructed in [1] as the result of throwing together all the models of (the type constructed in) this paper into one big model, which has the somewhat strange properties mentioned above.