Article contents
An intuitionistically plausible interpretation of intuitionistic logic
Published online by Cambridge University Press: 12 March 2014
Extract
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.
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.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1977
References
REFERENCES
- 10
- Cited by