The aim of this paper is to present a constructive solution to Frege's puzzle (largely limited to the mathematical context) based on type theory. Two ways in which an equality statement may be said to have cognitive significance are distinguished. One concerns the mode of presentation of the equality, the other its mode of proof. Frege's distinction between sense and reference, which emphasizes the former aspect, cannot adequately explain the cognitive significance of equality statements unless a clear identity criterion for (...) senses is provided. It is argued that providing a solution based on proofs is more satisfactory from the standpoint of constructive semantics. (shrink)

A form of Kripke's schema turns out to be equivalent to each of the following two statements from metric topology: every open subspace of a separable metric space is separable; every open subset of a separable metric space is a countable union of open balls. Thus Kripke's schema serves as a point of reference for classifying theorems of classical mathematics within Bishop-style constructive reverse mathematics.

The use of the three labels to denote the three foundational schools of the early twentieth century are now part of literature. Yet, neither their number nor the...

The author proved in his Ph.D. Thesis [W. Veldman, Investigations in intuitionistic hierarchy theory, Ph.D. Thesis, Katholieke Universiteit Nijmegen, 1981] that, in intuitionistic analysis, the positively Borel subsets of Baire space form a genuinely growing hierarchy: every level of the hierarchy contains sets that do not occur at any lower level. It follows from this result that there are natural examples of analytic and also of co-analytic sets that are not positively Borel. It turns out, however, that, in intuitionistic analysis, (...) one may give surprisingly different and, in some sense, much more simple examples of analytic and co-analytic sets that fail to be positively Borel. In the paper, two such examples are given. In proving them correct, one obtains new proofs of the Borel Hierarchy Theorem. Brouwer’s Continuity Principle plays a crucial role in arguments. (shrink)

I survey Brouwer’s weak counterexamples to classical theorems, with a view to discovering what useful mathematical work is done by weak counterexamples; whether they are rigorous mathematical proofs or just plausibility arguments; the role of Brouwer’s notion of the creative subject in them, and whether the creative subject is really necessary for them; what axioms for the creative subject are needed; what relation there is between these arguments and Brouwer’s theory of choice sequences. I refute one of Brouwer’s claims with (...) a weak counterexample of my own. I also examine Brouwer’s 1927 proof of the negative continuity theorem, which appears to be a weak counterexample reliant on both the creative subject and the concept of choice sequence; I argue that it provides a good justification for the weak continuity principle, but it is not a weak counterexample and it does not depend essentially on the creative subject. (shrink)

When Kleene extended his recursive realizability interpretation from intuitionistic arithmetic to analysis, he was forced to use more than recursive functions to interpret sequences and conditional constructions. In fact, he used what classically appears to be the full continuum. We describe here a generalization to higher type of Kleene's realizability, one case of which, -realizability, uses general recursive functions throughout, both to realize theorems and to interpret choice sequences. -realizability validates a version of the bar theorem and the usual continuity (...) principles, while also providing naturally, as Kleene's 1965 realizability does not, for versions of lawless sequence axioms, as well as of Church's Thesis. (shrink)

The main result of this paper is a transfer theorem which describes the relationship between constructive validity and classical validity for a class of first-order sentences over the p-adics. The proof of one direction of the theorem uses a principle of intuitionism; the proof of the other direction is classically valid. Constructive verifications of known properties of the p-adics are indicated. In particular, the existence of cylindric algebraic decompositions for the p-adics is used.

We describe a variety of sets internal to models of intuitionistic set theory that (1) manifest some of the crucial behaviors of potentially infinite sets as described in the foundational literature going back to Aristotle, and (2) provide models for systems of predicative arithmetic. We close with a brief discussion of Church’s Thesis for predicative arithmetic.

According to Brouwer’s ‘theory of the exodus of consciousness’, our experience includes ‘egoicity’, a distinct kind of feeling. In this paper, we describe his phenomenology in order to explore and elaborate on the notion of egoic sensations. In the world of perception formed from sensations, some of them are, Brouwer claims, not completely separated or ‘estranged’ from the subject, which is to say they have a certain degree of egoicity. We claim this phenomenon can be explained in terms of the (...) primordial state of consciousness from where the ‘exodus’ starts. Having undertaken the analysis and interpretation of Brouwer’s descriptions and examples of egoic sensations, we provide a formal account of egoicity based on Brouwer’s definition of its relation to estrangement, desire and fear. We show that the four terms can be modeled by a classical and a graded logical hexagon, giving the corresponding axiomatizations. (shrink)