§

A constructivist theory of meaning does not include a semantic theory, in the strict sense of a theory of how sentences are determined as true or as false; more cautiously expressed, a constructivist theory of meaning does not need to include such a theory. For constructivism repudiates the conception of the sentences of our language as being determinately true or false, independently of our means of recognising them as such. It may or may not consider that the notions of truth and falsity require an explanation going beyond the ‘disquotational’ account whereby to say that A is true is simply to say that A, and to say that A is false is to say that not A; but, however those notions are explained, the explanation will be consistent with constructivist principles only if they are not taken to be properties possessed by sentences independently of our capacity to recognise that they possess them. In any case, it is not in terms of the notions of truth and falsity that constructivism conceives of the meanings of sentences as being given. The meanings of sentences do not consist, on the constructivist view, in our conception of how they are determined as true or as false independently of our means of judging their truth or falsity, but in what we recognise as constituting a verification or a proof of them. The notions of truth and falsity therefore do not need to enter into any specification of the meanings of sentences or of their component expressions: a theory of (canonical) proof thus replaces a theory of reference in the narrow sense.

The distinction between sense and reference, as Frege drew it, is therefore incapable of figuring in a constructivist theory of meaning. The sense of an expression, on the Fregean account, is the way its reference is given to us in virtue of our knowledge of the language to which it belongs. Since its reference, on this account, is its contribution to the determination of the truth-value of a sentence in which it occurs, and that conception of truth-value has no place in the constructivist theory of meaning, neither does the notion of reference, so understood; and, since sense is explained as the way in which the reference is given, the Fregean notion of sense has no place in that theory, either. Our question must accordingly be, not whether the classical distinction between sense and reference is to be admitted in a constructivist theory, but whether such a theory admits of a distinction in any way analogous.

In the classical theory, we distinguished predicates, relational expressions, and logical constants, on the one hand, from singular terms and functional expressions in the standard sense, on the other. A specification of the references of expressions of the former class required specific mention of truth-values; but the references of expressions of the latter class, though serving to determine the truth-values of sentences containing them, could be specified without any explicit mention of truth-values. A similar distinction holds good within a constructivist theory meaning. In order to state the meanings of predicates, relational expressions, and logical constants, we need to make express mention of proofs of sentences in which they occur. The meaning of a predicate is to be specified as consisting in a means of recognising something as a proof that the predicate applies to an object given in some particular way; likewise, the meaning of a sentential operator is to be specified as consisting in a means of recognising something as a proof of a sentence in which it is the principal operator, given what constitute proofs of the subsentences. By contrast, the meaning of a singular term or of a functional expression (in the standard sense that does not include predicates) can be specified without explicit mention of proofs.

For expressions of the former kind, there is no room for a distinction analogous to that between sense and reference. Where the term “semantic theory” is interpreted in a broad sense, namely as denoting whatever part of a theory of meaning plays the central role played, in a realist theory, by the theory of reference, our grasp of the meaning of such an expression just is our grasp of what is to be assigned to it, in a constructivist semantic theory, as its semantic value: it does not consist in some particular way in which that semantic value is given to us. It might be objected that it is possible to define the extensional equivalence of predicates as a relation weaker than identity of meaning. It will hold if we have a means of transforming any proof that an object satisfies F into a proof that it satisfies G, and conversely; but, even though we possess such a means, F and G need not have the same meaning, since, before we carry out the transformation, a proof that an object is F is not, of itself, a proof that it is G, nor conversely.

Provable extensional equivalence is thus a weaker relation between predicates than intensional coincidence. That is not enough, however, to justify applying to them the sense/reference distinction. We grasp the meaning of a predicate when we know how, for any element of the domain over which it is defined, to classify mathematical constructions into those that do and those that do not prove that it satisfies the predicate; and just that principle of classification is the semantic value of the predicate. In grasping it, we are not conceiving of it as a particular way in which the class of predicates provably equivalent to it is given; on the contrary, we could have no conception of that class of predicates unless we already associated with each predicate a meaning of the kind in question. That meaning is not, therefore, to be regarded as a sense determining the predicate’s semantic value or reference. It is of course true that, by replacing one predicate by another provably equivalent to it in a given sentence, we preserve the status of the sentence as provable or otherwise. This may seem to be the analogue to the classical criterion of co-referentiality, namely that replacement should guarantee preservation of truth-value. But it is not. In the classical case, what is required to be preserved is that which, according to classical semantics, constitutes the semantic value of the sentence, namely its truth-value; so the condition is a reasonable one for ascribing the same reference or semantic value to the constituent replaced and that which replaces it. But, in the constructivist theory, the semantic value of a sentence is not its status as provable or not provable. It is, rather, the specific partition of mathematical constructions into those that constitute proofs of that sentence and those that do not, and this partition is not preserved by the replacement of a predicate by one provably equivalent to it. From a constructivist standpoint we have, rather, to acknowledge that for predicates there is no such distinction as that between sense and reference on the classical theory: the semantic value of the predicate and what we grasp when we understand it are one and the same.

This result follows precisely because the meaning of a predicate is to be explained in terms of proofs. Classically, the semantic value of a sentence is its truth-value, from which very little is to be inferred concerning the thought it expresses: there is accordingly a very wide gulf between the reference of a sentence, classically understood, and its sense. But, constructivistically, the semantic value of a sentence is a principle for classifying mathematical constructions into those that are and those that are not proofs of it, and when we have grasped this principle, we have thereby grasped the thought expressed by the sentence. Thus, for sentences, constructively understood, there can be no distinction between sense and reference. The impossibility of drawing such a distinction is transmitted from sentences to predicates, of however many places, precisely because the notion of proof enters explicitly into the characterisation of their meanings. The meaning of any expression constitutes its contribution to the meaning of a sentence in which it occurs; but the meaning of a predicate is expressly given as being its contribution, that is to say, in terms of the meaning of a sentence containing it, considered as characterised by what is to count as a proof of such a sentence. For that reason, the lack of a sense/reference distinction for sentences entails the absence of such a distinction for predicates. No such inference can be drawn for singular terms or term-forming functional expressions, because, although they go to determine what constitutes a proof of a sentence in which they occur, their meanings are not directly given in terms of proofs.

At first sight, there is exactly the same reason in constructive mathematics to distinguish the references of terms for natural numbers, or other finitely presented mathematical objects, from their senses as there is in classical mathematics. One and the same natural number may be given in different ways: as 13 in decimal notation, or as 1101 in binary notation, or again as $4 + 3^2$ , etc., etc. If analytic judgements extend our knowledge, then the equation “ $4 + 3^2 = 13$ ” extends our knowledge, even though mere computation is sufficient to establish it; so the senses of the two sides of the equation must differ, as they plainly do, while their references are the same, because the equation is true.

But should a constructivist view the matter in this same simple way as does the classical mathematician? That way of viewing it depends upon taking the equals sign, when standing between terms for natural numbers, as the sign of identity, strictly understood, as Frege insisted that it should be taken; but should a constructivist so construe it? For the classical mathematician, the natural numbers are abstract objects which may be identified or picked out in differing ways just as concrete objects like stars may be. But the constructivist is disposed to say that natural numbers, like all other mathematical entities, are mental constructions. If so, then surely 13 and $4 + 3^2$ are different mental constructions. In this case, numerical equality, albeit decidable, is not identity, properly so called, but merely an equivalence relation, indeed a congruence relation with respect to the ordinary number-theoretic operations, relations, and properties. We should then be in a position similar to that relating to predicates: there would be, for number-theoretic terms, no genuine analogue of the classical distinction between sense and reference.

The argument appears highly dogmatic, indeed metaphysical. It turns on the abstruse question whether natural numbers are to be described as abstract objects or as mental constructions. Different pictures accompany these divergent descriptions: it is nevertheless far from immediately clear what substance is to be given to them and to the choice between them. To characterise mathematical entities as ‘mental constructions’ is at least questionable, because it prompts Frege’s objections concerning the communicability of what is created by the mind, that is to say, by some individual mind. The substantial difference between the classical and the constructivist conception of mathematical entities is that, for the classical mathematician, a mathematical object, like a concrete object, has fully determinate properties independently of whether we recognise it as having them or are capable of doing so, whereas, for the constructivist, it has only those properties we are able to recognise it as having. The only sense the constructivist attaches to the hypothesis that a mathematical object has a given property is as the hypothesis that we could prove it to have that property, whereas the classical mathematician regards such a hypothesis as capable of holding good regardless of what we can or cannot prove.

Now should this difference prompt the constructivist to deny that natural numbers, and similar finitely given mathematical entities, are abstract objects? Whether or not an adherent of constructive mathematics recognises a sufficient analogy between them and concrete objects depends upon what he thinks about the physical world. If he takes a realist view of it, he will think, concerning physical objects like stars, what the classical mathematician thinks concerning mathematical objects: that they have fully determinate properties independently of whether we recognise them as having those properties or are capable of doing so. He may indeed take their possession of such properties, independently of us, as what makes them objects, a distinguishing characteristic of the formal concept ‘object’. Mathematical entities, as he conceives of them, will then not, for him, qualify as objects: it will be, on his view, a misconception to think of them as abstract objects or as objects of any kind at all. Their identity will be wholly determined by the manner in which we conceive of them: 13 and $4 + 3^2$ will accordingly be distinct, even though the relation of numerical equality holds between them.

He may, on the other hand, take the same view of physical objects as he does of mathematical entities: he may think of physical objects, too, as possessing properties only inasmuch as we can recognise them as doing so. He may take physical reality to exist only as having, not merely a form, but matter in the scholastic sense of that of which it is the form, and believe that only experience of it can provide it with matter in this sense. In this case, he will have no objection to agreeing with a platonist that natural numbers and similar mathematical entities are objects: abstract objects, indeed, but objects in the same sense as concrete objects like stars and glaciers. Unlike the platonist, he believes that natural numbers have no properties we cannot recognise them as having; but, then, he believes the same about stars and glaciers. Since natural numbers are objects, we may, he will think, regard “13” and “ $4 + 3^2$ ” as denoting the same object, just as the platonist does, and hence as differing in sense while agreeing in reference.

The conclusion, that constructivist acceptance of the sense/reference distinction is consequent upon his view of the ontological status, not of mathematics, but of physical reality, depends on the error of arguing from metaphysics to the theory of meaning. Even from the standpoint of a constructivist who refuses to regard natural numbers and similar mathematical entities as objects, a numerical term is to be seen as a means of picking out a natural number in a manner in which a predicate is not to be seen as a means of picking out an equivalence class of extensionally equivalent predicates. The notion of a natural number is more basic than that of any particular notational system for referring to natural numbers; the standard operations of addition, multiplication, etc., are presented as effective means of arriving from given natural numbers at other natural numbers. It is thus correct to regard numerical terms as aiming at natural numbers by varying routes, and hence to apply to each of them a distinction between its reference—the natural number aimed at—and its sense—the particular means for specifying that natural number. The fundamental question, for deciding whether or not we can distinguish between the sense and reference of a term for a natural number in a manner analogous to that in which the distinction is made in classical semantics is not whether natural numbers are objects, but over what we conceive of number-theoretic predicates as being defined. A number-theoretic predicate is defined over the natural numbers. We do not need to specify its application to the different mental constructions represented by “13,” “ $\mathrm {SSSSSSSSSSSSS}0,$ ” “ $4 + 3^2,$ ” “1101,” and the like. The standard definitions of basic arithmetical predicates make no mention of any particular notation for the natural numbers, although, given any such notation, it is simple to derive from those definitions a routine for deciding them; likewise, neither the recursion equations for the basic operations, nor their definitions in terms of cardinality (the ‘set-theoretic’ definitions), make any allusion to a system of notation. Because equality is a decidable relation, and there is an effective means of finding the value, expressed in standard notation, of an arithmetical term like “ $4! - 11$ ,” there is no obstacle to considering arithmetical predicates as defined over the natural numbers themselves, rather than over means of representing, constructing or conceiving of them. If arithmetical predicates were defined on mental constructions, we should decide the truth of “ $4^2 - 3$ is prime” by directly considering the application of “ $\_\hspace{-0.6pt}\_\hspace{-0.5pt}\_\hspace{-0.5pt}\_$ is prime” to $4^2 - 3$ . On the contrary, we first evaluate “ $4^2 - 3$ ” and then determine the application of “ $\_\hspace{-0.6pt}\_\hspace{-0.6pt}\_\hspace{-0.5pt}\_$ is prime” to 13; and this is the exact analogue of the way in which, on the classical conception, reality determines its truth in two stages, namely arriving at the reference of “ $4^2 - 3$ ” and determining the application of the predicate to it. Despite our doubts, therefore, first impressions have proved correct: there is exactly the same reason for applying the sense/reference distinction to terms for natural numbers, and hence also expressions, simple or complex, for functions on the natural numbers, as there is in the classical case.

§

When we turn to mathematical entities like real numbers that are not finitely presented, the question bears a radically different face. One of the two fundamental differences between classical and constructive mathematics lies in the opposition, not between conceiving of mathematical entities as independently existing abstract objects and as mental constructions, but between divergent conceptions of meaning, as related to what makes a statement true and as related to what constitutes a proof of it. A real number, such as $\pi $ , can be given in different, even though provably equivalent, ways. For classical mathematicians and constructivists alike, the specific way in which the number $\pi $ is given affects what is required for a proof of a statement about it, at least until the different possible definitions have been proved equivalent; that is why the sense of an expression, and not just its reference, must be something common to all. In classical semantics, however, the semantic value of a term denoting $\pi $ will be its contribution to what determines, not what is required to prove a statement in which it occurs, but its truth-value, and that is just the denotation of the term, the number $\pi $ itself; that is why its sense is not part of its semantic value. In a constructivist meaning-theory, by contrast, the semantic value of the term is, precisely, its contribution to determining what is to count as a proof of any statement in which it occurs; and therefore the way in which the denotation is given to us is an integral ingredient of its semantic value.

This makes clear that the classical Fregean way of drawing the distinction between sense and reference cannot be generally sustained within constructive mathematics, even for terms. Nevertheless, the way in which the matter has been put, speaking about “the way in which the denotation is given to us,” concedes that a distinction is to be admitted between the denotation of a term and the way in which the object it denotes is given; and this is plainly akin to the classical distinction between its reference and its sense. It is not the same distinction, since the way in which the denotation is given is an ingredient of the semantic value of the term; but it is sufficiently akin to it to constitute a constructivist analogue of that distinction.

By no means all constructive mathematicians will agree that such a distinction ought to be allowed. Adhering to the conception of mental constructions, they hold that we must treat the denotation of a term as an intensional object: that intensional object will then embody the manner in which it is apprehended, which will not, however, be a way in which something else is given to us. Let us call this the ‘intensionalist’ conception, and that which allows an analogue of the sense/reference distinction the ‘objectual’ one. Which of the two should we adopt?

The second of the two fundamental divergences between classical and constructive mathematics lies in their differing attitudes to infinity. A process is a sequence of operations, and the everyday conception of an infinite sequence is that of one that does not terminate. The constructivist takes this seriously: since an infinite process does not terminate, we cannot regard it as having a final product. The classical mathematician thinks that this is to introduce time into mathematics, where it has no place. He agrees that an infinite process, taking place in time, can have no final product. But he holds that, although the sequences we first encounter, such as the strokes of a clock, are temporal, in mathematics the notion of a process can be stripped of its temporal character, just as Frege insisted that the general notion of sequence can. A sequence in the logical sense employed in mathematics has indeed a generating relation in which each term of the sequence stands to the next one; but this need not be temporal succession, but may be a relation of any kind. A non-temporal sequence, including a process, even though infinite, can exist all at once. We are therefore entitled to think of infinite processes as yielding determinate products; for example, a Cauchy sequence of rationals as yielding a real number. We may, when convenient, specify the product by reference to the process that yields it; but, when it is the product that we are interested in, we may thereupon disregard the process and speak only of the properties of the product, however arrived at.

The constructive mathematician is not, of course, as naïve as this rebuttal takes him to be. He realises perfectly well that a mathematical sequence can be defined in terms of a purely mathematical relation between its successive terms. But he does not wish, as the classical mathematician does, to cut the link between our mathematical concepts and what we (that is to say, what human mathematicians) actually do. He will therefore admit an operation on a mathematical object as well defined only if it is one that we can actually carry out. An infinitary operation cannot be carried out, and therefore it is not admissible. It is in this sense that an infinite process cannot be completed. We can, indeed, talk about the product of such a process; but we cannot think of the product apart from the process that produces it, and we cannot ascribe to it properties other than those determined by what we know of the generating process.

This attitude is, of course, closely connected with treating the meaning of a mathematical statement as given by what is required of a proof of it: our question is whether it obliges us to take an intensionalist view of infinitary mathematical entities. We gain little help from the terminology of constructive mathematicians. They sometimes say that we should conceive of an object together with the way in which it is given, thus adopting an objectualist mode of expression distinguishing between what is given and how it is given; but they also say that an object a should be said to be identical to an object b, rather than merely extensionally equal to it, only if they are given in exactly the same way; and this is to say, in effect, that all the objects of constructive mathematics are intensional ones.

Why should we bother with strict identity, so understood? The reason for doing so arises from considering what it is for a function to be defined on the given entities. Bishop’s remark that the validity of the axiom of choice is “implied in the very meaning of existence,” as constructively understood, has in some sense to be true; but it is true generally only if the identity relation on the domain of the choice function is strict (i.e., intensional). Goodman and Myhill showed by a simple example that the axiom of choice, applied to statements beginning $\forall S \exists n$ , where S ranges over species, implies the law of excluded middle if the choice function is required to have the same value when applied to extensionally equal species. We must therefore either deny that “the very meaning of existence” implies the existence of a choice function, or accept that species are intensional entities, identical only when they are defined in the same way. The former denial seems unfaithful to a constructive interpretation of existence; the latter is, then, our only option. We may distinguish between operations and functions, where functions have the same value for extensionally equal arguments, while the action of an operation may depend on some non-extensional feature of the object to which it is applied, so that “the very meaning of existence” as expressed in a quantifier combination of the form $\forall x \exists y$ guarantees, in general, only the existence of a choice operation, not of a choice function; this will not disguise the need to take the object as an intensional one.

That species should be regarded as intensional entities is not so hard to swallow: we have to conceive of them as extensions of concepts in a sense that Frege did not intend. It is harder to accept that infinite sequences and real numbers should be so regarded. Let us start at the further end, with real numbers. There is a disagreement about what real numbers are. Intuitionists usually characterise them as equivalence classes of Cauchy sequences of rationals; between such equivalence classes there is an obvious relation of extensional equality, that of having the same members. For Bishop and his disciples, followed by Beeson, a set has always to be provided with an equality relation, of which we demand only that it be an equivalence relation. We can therefore dispense with the equivalence classes and take the Cauchy sequences of rationals themselves to be the real numbers; the same equivalence relation between them as before will then serve as the relation of equality between real numbers.

In this regard, intuitionists conform more closely to classical practice. For classical mathematicians, definitions in terms of equivalence classes are needed to secure the identity of the objects defined: there is, for them, no such thing as stipulating what the equality relation on a given set is to be. A constructivist is unlikely to view the matter as being to do with identity, properly so called. But even if equality is not identity, it should arguably be understood as one and the same relation in all cases, namely as extensional equality between sets and functions, rather than as differently defined for different contexts.

Even if real numbers are not Cauchy sequences, but equivalence classes of them, constructivists are accustomed to say that a real number, $\pi $ for example, must always be thought of as given in a particular way, namely by means of a specific Cauchy sequence. For all that, like classical mathematicians, constructivists think primarily in terms of the number $\pi $ , rather than of one or another Cauchy sequence of which it is the limit. In this sense, it is contrary to how anyone actually thinks to say, with Bishop, that real numbers simply are Cauchy sequences of rationals. An equivalence class consists, for a constructivist, of elements of some species that are provably equivalent. There are, moreover, distinct ways of characterising it: either as a maximal subspecies all of whose members are equivalent, or as the species of elements equivalent to some one given element. If real numbers are defined as equivalence classes of the second sort, then a real number will be given as determined by a Cauchy sequence. If it is borne in mind that the sense of a term is part of its semantic value, there will then be no need for any special thesis that a real number must come equipped with such a Cauchy sequence: that will be supplied by its definition, which embodies the sense of the term that denotes it. It need not, therefore, be considered as an intensional entity, for which there is no distinction between what it is and how it is given: it is a mathematical object, a proof of a proposition concerning which will depend, as for any object, on how it is given.

How, then, do matters stand for infinite sequences? Must quantification over or reference to them be understood as relating to intensional objects? Any specific sequence must be picked out in some way; it must be identifiable, so that, for each n it is determinate what its n-th term is. As a real number is given in terms of a Cauchy sequence, so a sequence is given by reference to a process that generates it. A process is not an intensional object, in the sense of one that exists only in thought; but it is not a mathematical object, either, being identified, not by its results, but by how it is carried out. It may be carried out by mathematical means, each term being uniformly determined by some effective operation. There will then be no need to think of it as taking place in time: it is individuated simply by the mathematical rule for determining each term of the sequence. It remains that any operation upon the sequence must be an operation on the generating process: since the operation must be finitary, its base must consist of the finite amount of information which serves to individuate the process, and anything deducible from that, including the values of any finite number of terms.

For some constructivists, a sequence can be generated only by applying an effective mathematical operation to determine its terms. Some leave the notion of an effective operation without further delineation; others are willing to accept Church’s thesis and to identify an effective operation with a recursive function. For intuitionists, on the other hand, although what the process yields must be of a mathematical nature, the process need not be individuated by mathematical means; and, if it is not, it must be conceived as a process in time. The same will apply as before: an operation upon a sequence generated by such a process must take the form of an operation on the process itself; and, as before, the base of the operation must consist of the finite amount of information serving to individuate the process, and of the values of any finite number of its terms. The difference, of course, is that we can deduce much less concerning the terms generated from the way the process is to be individuated; and within the mathematical theory, the means by which it is individuated remains in the background, notice being taken only of whatever restriction on the terms of the sequence is imposed by the character of the particular process.

A sequence is given in terms of the process that generates it. Whether it should itself be considered an intensional object depends on how universal quantification over sequences is to be interpreted, and whether we need a distinction between operations on and functions of sequences. For those constructivists who identify sequences of natural numbers with constructive functions on the natural numbers, and constructive functions on the natural numbers with general recursive functions, an extensional interpretation of the universal quantifier is possible: for them, although quantification over sequences of natural numbers is indeed quantification over effective rules, such rules can be coded as natural numbers, and we have a means of expressing extensionally that the rule coded as the number e yields the number m as the n-th term of the sequence: intensionality is swallowed up in the theory of recursive functions.

Constructivists, like those of the Bishop school, who identify sequences of natural numbers with constructive functions on the natural numbers without accepting Church’s thesis, do not have recourse to this device: they maintain bland agnosticism. They are therefore forced to maintain the distinction between operations and functions, and thereby in effect to regard infinitary mathematical entities like infinite sequences as intensional objects. While mathematicians want to get on with the mathematics without bothering much about its foundations, philosophers want to be clear just what constructive mathematics is about: Brouwer himself repudiated logical foundations for mathematics, but was rightly concerned with its conceptual foundations.

Cannot the intuitionist’s understanding of infinite sequences be formulated as fundamental principles of his mathematical theory, so avoiding the need to treat them as intensional entities? Beeson regards continuity principles as serving precisely this purpose. He says:

Continuity principles, however, do not encapsulate the whole content of the intuitionistic conception of how infinite sequences are given to us. They embody only one consequence of that conception, and they relate only to propositions beginning with a particular type of quantifier combination. The general case is a proposition about some one given choice sequence. A principle laying down on what basis such a proposition can be asserted is one of those known as data principles; it will take the form of saying that, if a proposition $A(\alpha )$ holds, then for some species S of a particular type to which $\alpha $ belongs, $A(\beta )$ will hold for every other choice sequence $\beta $ in S.

The formulation of a correct such principle serves to make precise the notion of a choice sequence, by an exact analysis of how a sequence can be given. The search for such precision was pursued by Myhill and, above all, by Troelstra, whose most important contribution was to focus attention on the need for the class of choice sequences to be closed under continuous operations. If, for example, we were to take the species S to consist of the elements of a spread, then, given a choice sequence $\beta $ , we can suppose $\alpha $ to be obtainable from $\beta $ by some continuous operation: but then our data principle would tell us that any other sequence $\gamma $ in that spread, and agreeing with $\alpha $ on some initial segment, would be similarly related to $\beta $ , which is absurd. Our data principle went astray because it ignored the possibility that one choice sequence may be given in terms of another: the sequence $\alpha $ was given as the result of applying a certain continuous operation to $\beta $ .

The point vividly illustrates the importance of taking adequate account of how a choice sequence is given to us; but, if we replace the continuity principle by a sound data principle from which it can be derived, Beeson is right that the formulation of a principle laying down how, in general, a sequence may be given liberates us from having to consider sequences as intensional entities. For constructivists of a different school, Church’s thesis performs the same service. Only the agnosticism of the Bishop school compels its members to maintain a distinction between operations and functions, and hence an intensionalist stance. To despair of formulating foundational principles for constructive mathematics is to withdraw its claim to provide a clear alternative to the classical variety, let alone to be the only way in which mathematics ought to be done. The objectual view is thus vindicated: we should distinguish what is given from how it is given, while acknowledging that how it is given affects what we take to be central to its meaning, namely what is required to prove something about it.