×

zbMATH — the first resource for mathematics

Extending the topological interpretation to intuitionistic analysis. (English) Zbl 0197.00201
In this paper the author begins the investigation of a (classical) model for intuitionistic analysis, essentially different from Kleene’s realizability interpretations and from the various models of Kreisel and Troelstra, which arises from a clever extension of the topological interpretation of Heyting’s predicate calculus. Here only the elementary theory of order in the continuum is considered, and various partial independence results are obtained; in Part II these results are considerably strengthened and an interpretation of real-valued function of a real variable (satisfying the uniform continuity principle of Brouwer) is introduced.
The model is obtained from a topological space \(T\) (e.g. Baire space \(N^N)\) as follows. To each formula \(A\) an open subset \([A]\) of \(T\) is assigned, such that
\[ [A\wedge B] = [A]\cap [B],\;[A\vee B] = [A] \cup [B],\;[\neg A]=\text{In}(T \sim [A]),\;[A \to B] = \text{In}((T\sim [A]) \cup [B]), \]
\[ [\exists xA(x)] = \bigcup_{\xi\in\mathcal R} [A(\xi)],\quad\text{and}\quad [\forall xA(x)] = \text{In} \bigcap_{\xi\in\mathcal R} [A(\xi)], \]
where \(\mathcal R\) is the class of all continuous functions \(\xi: T\to\mathbb R\), \(\mathbb R\) is the set of classical reals, and \([A(\xi)]\) denotes the value assigned to \(A(x)\) when \(x\) is given the value \(\xi\). The atomic formula \(x<y\) is assigned the value
\[ [\xi<\eta] = \{t\in T: \xi(t) < \eta(t)\} \]
when \(x,y\) are interpreted by \(\xi, \eta\), respectively. The formula \(A\) is valid if \([A] =T\). This assignment satisfies the usual intuitionistic axioms for the measurable natural ordering of the continuum. (The treatment can be extended to the theory obtained by adding terminology and axioms for the rationals; indeed, it is this extension which apparently suggested the interpretation of the reals as continuous functions.)
The author shows that for an open formula \(B(x,y)\) in two variables, which is equivalent to \(A(x<y,y<x)\) for some formula \(A(P,Q)\) of propositional calculus, the statement \(\forall x\forall y B(x,y)\) is provable from the intuitionistic order axioms for the reals if and only if \(\vdash \neg (P\vee Q) \to A(P,Q)\) in intuitionistic propositional calculus; he obtains a similar condition for formulas in three variables.
Further independence results follow from the observation that if \(\forall x \neg \forall y B(x,y)\) is invalid in the model, then \(\forall x \neg \forall y B(x,y)\) is valid; similarly for three variables. (In Part II these results are generalized to arbitrary open formulas.)
The style of the paper is graceful, and its content augmented by that of Part II) represents a substantial contribution to the modern study of intuitionistic analysis.
(This volume is dedicated to Prof. Heyting on his 70th birthday)

MSC:
03B20 Subsystems of classical logic (including intuitionistic logic)
03F55 Intuitionistic mathematics
Keywords:
general logic
PDF BibTeX XML Cite
Full Text: Numdam EuDML
References:
[1] E. Bishop [1] Foundations of Constructive Analysis , New York, 1967. · Zbl 0183.01503
[2] A. Heyting [2] Intuitionism. An Introduction , Amsterdam, 1956. · Zbl 0125.00510
[3] S.C. Kleene and R.E. Vesley [3] Foundations of Intuitionistic Mathematics , Amsterdam, 1965. · Zbl 0133.24601
[4] G. Kreisel [4] Mathematical Logic , in Lectures on Mathematics, vol. III, (ed. T. L. Saaty), New York, 1965, pp. 95-195. · Zbl 0147.24703
[5] H. Rasiowa and R. Sikorski [5] The Mathematics of Metamathematics , Warsaw, 1963. · Zbl 0122.24311
[6] A.S. Troelstra [6] The Theory of Choice Sequences , to appear. · Zbl 0263.02017
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.