Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:
(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:
(2) If A is intuitively true, then ⊨ A.
Then one might hope to be able to prove
(3) If ⊨ A, then ⊦IPCA.
If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.
![](//static.cambridge.org/content/id/urn%3Acambridge.org%3Aid%3Aarticle%3AS0022481200050180/resource/name/S0022481200050180_eqnU1.gif?pub-status=live)
Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.