Mark Van Atten
email: vanattenmark@gmail.com

Martin-Löf Prawitz

Predicativity and parametric polymorphism of Brouwerian implication

A common objection to the definition of intuitionistic implication in the Proof Interpretation is that it is impredicative. I discuss the history of that objection, argue that in Brouwer's writings predicativity of implication is ensured through parametric polymorphism of functions on species, and compare this construal with the alternative approaches to predicative implication of Goodman, Dummett,

Impredicativity and intuitionistic implication

A definition is impredicative if it defines a member of a totality in terms of that totality itself. There is a familiar contrast between two kinds of impredicative definitions, as illustrated by these two examples:

1. k = the largest number in {1, 2, 3}; k is a member of that totality.

2. Let s be an infinite set. According to the power set axiom, there exists a set P(s) = ι x(∀y(y ∈ x ↔ y ⊆ s)). Here ∀y is a quantification over the totality of all sets; P(s) is a member of that totality. 1 In the first, the totality in question is enumerated and this is one way of defining each of its elements prior to defining k; the impredicative definition of k serves to single out a certain element of that totality, but is not essential to the introduction of that element. On the other hand, for an infinite set s, there is no alternative to characterising the set of all its subsets by relating it to the totality of all sets, because there is no way to generate all subsets of a given infinite set from below. 1For constructivists this means that the first definition is acceptable as a definition of a mathematical object, whereas the second is not.2 More generally, if at a given moment, the only definition available of a certain object is an impredicative one that refers to a totality for which we at that moment have no construction, then this definition cannot be used to guide a construction process of that object. To construct the defined object, we would first have to construct the totality that its definition refers to, but as this totality contains the object we are in the process of constructing, we find that we can only complete that process if we already have completed it. In such cases the circularity of the impredicative definition is vicious.

Of Brouwerian intuitionism it has been argued that various of its definitions are impredicative in the vicious sense, and hence not constructive: the propositional connective of implication, the principle of induction, certain sequences in the so-called Theory of the Creating Subject (Troelstra's Paradox), the theory of ordinals, certain species in Brouwer. I will here focus on the clause for implication in the Proof Interpretation; it will turn out that this requires also a discussion of species, and sheds some light on the theory of ordinals. 3 An often cited formulation of it is that in Constructivism in Mathematics by Troelstra and van Dalen:

A proof of A → B is a construction which permits us to transform any proof of A into a proof of B. [Troelstra and van Dalen 1988, vol.1, p.9] In this formulation, one will want to understand 'construction' as a function f , because then the explanation what a proof of an implication is will have the definiteness, stability, and uniformity characteristic of a function: for each argument there will be a determinate value, to a given argument at any time the same value will be assigned, and to all arguments a value is assigned in the same way.

How is the domain of such a function f to be understood? It cannot be given by an inductive definition of all proofs of A, as there can be no such definition. In particular, proofs of A may themselves contain the implication A → B, for example in this way:

(A → B) → A A → B →-E A
Thus a prior explanation of A → B would be required, rendering the definition circular.

But if the domain is to be all proofs of A in an absolute sense that can not be given by an inductive definition, then, so the claim goes, the definition of such a function f will take a form that renders it impredicative:

f is a function such that, for any x in the totality of all intuitionistic proofs, if x is a proof of A, then f (x) is a proof of B.

Any specific definition of this form will define an individual proof of A → B by referring to a totality to which it belongs, and thus be impredicative.

Intuitionists consider the notion of proof to be open-ended, not only epistemically (at no moment do we know all possible proofs) but ontologically, and hence they deny that there is such a thing as the totality of all intuitionistic proofs (Brouwer, 1907, pp.148-149). There is only a growing universe of mathematical objects and proofs. For those who share the criticism that intuitionistic implication is impredicative, this intuitionistic conception of the universe would of course be part of what makes the whole enterprise incoherent: Intuitionists cannot have both a universe that is growing and a notion of implication that demands that it is a totality. Hence the intuitionistic denial that the universe is a totality only makes the question more urgent whether there are understandings of the notions of proof, function, and domain, such that they allow for an intuitionistically coherent reading of the clause for implication in the Proof Interpretation.

It might seem possible to circumvent the problem by defining A → B to mean 'From the assumption that A is true, a proof of B can be obtained', the idea being that by making a mere assumption, talk of proofs is avoided altogether. 4 But on Brouwer's notion of truth, according to which 'truth is only in reality i.e. in the present and past experiences of consciousness' [START_REF] Brouwer | Consciousness, philosophy and mathematics[END_REF](Brouwer, , p.1243)), the fundamental meaning of 'Proposition A is true' is that a suitable mental construction that is correctly described by A has been carried out. Brouwer allows the idealisation that, whenever the Subject has not actually carried out a given construction method, but could do so in principle, the construction it leads to may be counted among those that have been carried out. But in each case an appeal to this must be made explicitly, for otherwise there is no conceptual reduction to what has been experienced. The latter remains the primary notion. Either way, there is no such thing as a mere assumption. To assume that A is true is to assume that a construction for A has been carried out (perhaps in an idealised sense).

A kind of 'weak impredicativity' may also be associated with the Proof Interpretation. The term is taken from a draft note of 1970 by Gödel, not on the Proof Interpretation, but on his computable functionals of finite type:

In particular, there exist functions of lower type which, within T , can only be defined in terms of functions of higher types. This is a kind of impredicativity. True, it is only one of those weak impredicativities that are admitted even in Princ[ipia] Math[ematica] 2nd ed. p.[XL],5 ff. In our proofs of the axioms of T this impredicativity appears in the fact that the concept of reductive proof may itself occur in reductive proofs (just as in Heyting's logic the general concept of proof may occur in a proof). (van Atten, 2015b, p.218) In the case of intuitionistic implication, this would pertain to the composition of the function f , which may depend on proofs of implications up to a definite, but arbitrarily high, type, as a proof of a statement may refer to proofs of more complex statements (Troelstra, 1990, p.233). To take a simple example, f may be h • g, with g raising the type and h appropriately lowering it again. It may seem then as if the existence of functions of a lower type presupposes the existence of functions of higher types. I will return to this problem after the discussion of strong impredicativity.

History of the objection

It has been claimed [START_REF] Dean | Kreisel's theory of constructions, the Kreisel-Goodman paradox, and the second clause[END_REF], section 2) that the thought that intuitionistic implication is impredicative goes back to Gödel's lecture titled 'The present situation in the foundations of mathematics', presented at a meeting of the Mathematical Association of America in Cambridge, Massachusetts on December 30, 1933 [START_REF] Gödel | The present situation in the foundations of mathematics[END_REF]. Contrary to the organisers' plan, Gödel left the text unpublished, but it was included in the Collected Works in 1995. And the suggestion that the objection of impredicativity is made there seems natural; in that text Gödel questions the constructive character of the intuitionistic explanation what a proof of a negation consists in, which is a particular case of that for implication, and his scepticism turns on the observation that this clause involves quantification over all possible proofs. In this section, I will first argue that, all the same, the objection that Gödel is actually making in 1933 is a different one, and then conjecture that it was shortly after Yale lecture of 1941 that the thought that intuitionistic implication is impredicative must have occurred to him. I will then consider the question who was the first to make that objection in print.

Gödel's 1933 lecture is concerned with the question of a constructive consistency proof for classical arithmetic. In considering what should count as constructive mathematics, Gödel there argues against accepting impredicative definitions, and insists on inductive definitions. Gödel discusses the prospects for a consistency proof for classical arithmetic using intuitionistic logic, then best known from Heyting's formalisation 'Die formalen Regeln der intuitionistischen Logik' (Heyting, 1930a,b,c), as well as Heyting's Königsberg lecture of 1930, 'Die intuitionistische Grundlegung der Mathematik', published as [START_REF] Heyting | Die intuitionistische Grundlegung der Mathematik[END_REF]. When writing the text for his talk, Gödel was able moreover to consult Heyting's manuscript on intuitionism meant for their joint book, eventually published by Heyting alone in Mathematische Grundlagenforschung [START_REF] Heyting | Mathematische Grundlagenforschung, Intuitionismus, Beweistheorie[END_REF]. Heyting had sent the manuscript of his part to Gödel in August 1932 (Gödel, 2003, p.54), more than a year before Gödel's talk.

In 'Die formalen Regeln der intuitionistischen Logik', Heyting says about a ⊃ b that it means 'If a is correct ['richtig'], then so is b' (Heyting, 1930a, p.5). In his Königsberg lecture of 1930, Heyting did not discuss implication in general, but about the special case of negation he said: 'The proposition "C is not rational" means the expectation that from the assumption that C is rational, a contradiction can be derived' (Heyting, 1931, p.113). Gödel knew that lecture well, because he had been in the audience, and in 1932 he reviewed the published version for the Zentralblatt [START_REF] Gödel | Review of 'Die intuitionistische Grundlegung der Mathematik[END_REF]. But it is in Mathematische Grundlagenforschung that one finds the first formulation of the general clause for implication.6 On p.14, Heyting describes the construction required to prove an implication a ⊃ b as one 'which from each proof of a leads to a proof of b'.7 This is a formulation that, unlike the earlier ones, makes it explicit that this is an operation on proofs of a and not a proof from the assumption a. I do not know whether Heyting's book of 1934 contained significant changes compared to the manuscript he had sent Gödel in 1932. But if so, it will not have been on this particular point, as Heyting's correspondence with fellow intuitionist Freudenthal shows that Heyting had obtained the reading of implication as 'I possess a construction that derives from every proof of a a proof of b' shortly after the Königsberg lecture (Troelstra, 1983, pp.206-207). It is this understanding that is assumed in Gödel's criticism in the 1933 lecture.

The principles in Heyting's formalisation that have Gödel's special interest are those for 'absurdity', that is, intuitionistic negation. But Gödel goes on to argue that this notion is not constructive in his sense, and hence of no use for a constructive consistency proof of classical arithmetic. The problem he sees is that their intuitionistic explanation involve a reference to the totality of all constructive proofs. The example he gives is p ⊃ ¬¬p which, he says, means 'If p has been proved, then the assumption ¬p leads to a contradiction'. 8 Gödel says that these axioms are not about constructions on a substrate of numbers but rather on a substrate of proofs, and therefore the example may be explicated as 'Given any proof for a proposition p, you can construct a reductio ad absurdum for the proposition ¬p'. He then comments that Heyting's axioms concerning absurdity and similar notions [. . . ] violate the principle, which I stated before, that the word 'any' can be applied only to those totalities for which we have a finite procedure for generating all their elements [. . . ] The totality of all possible proofs certainly does not possess this character, and nevertheless the word 'any' is applied to this totality in Heyting's axioms [. . . ] Totalities whose elements cannot be generated by a well-defined procedure are in some sense vague and indefinite as to their borders. And this objection applies particularly to the totality of intuitionistic proofs because of the vagueness of the notion of constructivity. Therefore this foundation of classical arithmetic by means of the notion of absurdity is of doubtful value. (Gödel, 1933b, p.53) A draft of this passage in Gödel's archive does not quite end with a rejection of Heyting's logic. Instead, it reflects: Therefore you may be doubtfull [sic] as to the correctness of the notion of absurdity and as to the value of a proof for freedom from contradiction by means of this notion. But nevertheless it may be granted that this foundation is at least more satisfactory than the ordinary platonistic interpretation [. . . ]9

Either way, the doubt about, or objection to, the notion of absurdity immediately generalises to implication as such.

It is remarkable, given the construction of Gödel's talk, in which the discussion of the intuitionistic logical connectives is preceded by an argument against the use impredicative definitions for foundational purposes, that the objection Gödel puts forward is not that Heyting's principles for absurdity are impredicative, but that they are vague. Impredicativity of course entails constructive undefinability and in that sense vagueness, and it is possible that Gödel had seen the problem of impredicativity but thought that, in the context of a consistency proof that is looked for because of its epistemic interest, vagueness is the more important thing to note, even if impredicativity is the cause of it.

But vagueness may arise on other grounds, and indeed to me it seems that the vagueness Gödel finds problematic in 1933 is not that caused by impredicativity, but by open-endedness. After all, when Gödel writes that For the totality of all possible proofs certainly does not possess this character [of being an infinity that is generated by a finite procedure], and nevertheless the word 'any' is applied to this totality in Heyting's axioms the second clause is evidently not presented as an explanation of the first. But if one's objection were that of impredicativity, one would do just that. One would argue that to accept the application of the word 'any' to the totality of all possible proofs, an application that occurs in Heyting's explanation of what a proof of a negation consists in, is to accept the existence of a proof that is impredicatively defined, and therefore of a proof that will never be generated by a finite procedure; and that, by implication, the totality of all possible proofs does not possess the character of being an infinity that is generated by a finite procedure, and hence is not constructive in the sense Gödel requires. But this is not an argument one finds in his lecture. In fact, while Gödel does point out the problem, from a constructive point of view, with impredicatively defined integers, he does not say anything at all about impredicatively defined proofs. The first incompleteness theorem, on the other hand, was brought up earlier in the lecture, and explained as meaning that no single consistent formal system can embrace all formal proofs. There is, then, no finite generating procedure to exhaust all possible proofs. And that the term 'any' as it figures in Heyting's axioms indeed must be taken to apply to the totality of all possible proofs, and cannot be explained via the notion of provability in any single formal system, was a result, based on the second incompleteness theorem, that Gödel had contributed to Menger's seminar in 1931/1932, 10 well before writing his Cambridge lecture. 11 Also in his subsequent discussions in the 'Lecture at Zilsel's' of 1938 and the lecture at Yale 'In what sense is intuitionistic logic constructive?' of 1941, 10 It was published in Gödel 1933a. 11 When Gödel in the lecture goes on to say that 'this objection applies particularly to the totality of intuitionistic proofs because of the vagueness of the notion of constructivity' (Gödel, 1933b, p.53), he is pointing to a reinforcement of the problem, not the problem as he sees it come about.

Gödel emphasises that intuitionistic provability cannot mean provability in a particular formal system, and is therefore not constructive in what he there takes to be the strictest sense, but he does not thematise impredicativity of any logical operation (Gödel 1938, pp.100-102;Gödel 1941, p.190).

As long as Gödel held on to the 'concrete' notion of constructivity outlined in each of the lectures of 1933, 1938, and 1941, a notion founded on the idea of finite generating procedures, his argument that intuitionistic logic is vague on account of the incompleteness theorem must have convinced him that it is of no epistemic value in consistency proofs. But it no longer could when, in the year after the Yale lecture, Gödel came to accept, like the intuitionists, abstract notions as part of his concept of constructivity; the suggestion occurs already in his Princeton lectures on intuitionism, which ended on May 1, whereas the Yale lecture had been delivered on April 15 (van Atten, 2015b, section 11.3.5.2). In Gödel's case, the abstract notion accepted as constructive was not the intuitionistic notion of proof, but that of computable functional of finite type, which he showed can replace the former when limited to its application in arithmetic. (Gödel describes the necessity of admitting abstract notion in print only in his Dialectica paper of 1958; in the introduction of that paper Gödel is, in effect, also addressing his former self.) On the other hand, Gödel continued to hold, unlike the intuitionists, that there exists a totality of all proofs. 12 But while the predicativity of his old notion of constructivity was ensured by its definition, this was not so for the widened one. This became (and remained) a matter of great concern to Gödel. If the thought that implication in Heyting's Proof Interpretation might be impredicative had not occurred to him before, it will have then.

Not much time later, between November 1942 and May 1943, Gödel wrote his paper 'Russell's mathematical logic', published in 1944. There, Gödel comes to speak of the 'self-reflexivity' of impredicatively defined properties (Gödel, 1944, p.139) 13 and points out that this self-reflexivity need not be problematic in general, but, when it occurs in definitions that are meant to be constructive, renders them viciously circular. However, he 12 In the 1972 version of the Dialectica paper, Gödel introduced the notion of 'reductive proof', by which he hoped to arrive at an interpretation of intuitionistic logic that 'in no way presupposes Heyting's and that, moreover, it is constructive and evident in a higher degree than Heyting's. For it is exactly the elimination of such vast generalities as "any proof" which makes for greater evidence and constructivity' (Gödel, 1972, p.276n, emphasis mine); see also van Atten 2015b, sections 11.3.5.7 and 11.3.5.9. 13 Russell, in his paper 'On some difficulties in the theory of transfinite numbers and order types' (1906), which Gödel refers to in his own paper, had used the simpler term 'reflexive'.

does not add that, specifically, the property of being an intuitionistic proof of an implication is problematic.

The first manuscript of Gödel's in which it is stated that intuitionistic logic is impredicative is an intermediate version of around 1970 of the revised Dialectica paper, and it is also included in the last, 1972 version, posthumously published in Collected Works.14 By then, it had of course been stated in print elsewhere.

Although Gödel, in print, remained silent on the question, his use of the term 'self-reflexivity' in relation to impredicativity in the Russell paper seems to have struck a chord. When Heyting published his book Intuitionism. An Introduction (1956), probably the most influential publication on intuitionism ever, it was immediately reviewed by Sigekatu Kuroda, in the Journal of Symbolic Logic. That review may well be the first publication of, in effect, the objection that intuitionistic implication is impredicative:

The proof of the fan theorem in this book is strikingly brief, although it is essentially the same as Brouwer's original proof of 1926 (Mathematische Annalen vol.97, p. 66, Th. 2). 15 By means of the dialogue method the author discusses a certain peculiarity of the proof of the fan theorem, namely that it depends on inferences, i.e., constructions, which are assumed to have been executed previously. The comment of the author (or a person in the dialogue) about it is as follows: 'If we are well aware that the hypothesis of a theorem consists always in the assumption of a previous execution of some construction, we can offer no objection against the use of considerations about the way in which such a construction can be performed as a means of proof.' The reviewer fully agrees to this comment. However, the assumed construction may contain a construction by the application of other fan theorems, in which further previous constructions are assumed, and so on. In this way the assumption of a fan theorem may contain, so to speak, in a nested manner many other fan theorems. The same situation arises when we wish to clarify the intuitionistic concept of negation (cf. 7.1.1), and of implication, as well as that of a function. The self-reflexive character of these could never be completely clarified by any formal method. [. . . ] Nevertheless, some clear analysis of the proof of the fan theorem would be necessary, because no proof may be self-reflexive. (Kuroda, 1956, p.369) It is not wholly clear to me to what extent Kuroda takes an intuitionistic implication to be different from a theorem based on a hypothesis; on Brouwer's conception of truth, however, they are the same, as to assume that P is to assume that P has been demonstrated. The identification of assuming the antecedent of an implication and assuming that a prior construction has been effected is also clearly shown by Heyting's clause for implication in the book under review:

The implication p → q can be asserted, if and only if we possess a construction r, which, joined to any construction proving p (supposing that the latter be effected), would automatically effect a construction proving q. (Heyting, 1956, p.98) Perhaps the reason why Heyting in chapter 3 does not present the fan theorem in logical notation was that he was there focused on its mathematical content, whereas logic is discussed only in the penultimate chapter of his book; the same remark can in fact be made about all theorems outside the chapter on logic.

Be that as it may, Kuroda signals the same problem for both. Although he does not invoke impredicativity here, it clearly is the problem he is describing, using instead the same term that Gödel had associated with impredicative definitions and its problem for constructivists in his Russell paper, 'self-reflexivity'.

Kuroda's review came out in 1956, after he had passed the academic year 1955-1956 at the Institute for Advanced Study, where he had had discussions with Gödel and also with Kreisel (Kuroda, 1958, p.248). 16 Kuroda had published four paper intuitionistic logic and its philosophical aspects before (1947; 1948; 1949; 1951). One readily imagines therefore that the question of the meaning of intuitionistic logic was among the topics of his conversations with Gödel and Kreisel; however, that has so far not been documented. Indeed, it is Kreisel who soon after Kuroda's review does use the term 'impredicative' to characterise the intuitionistic notion of proof, in his 1958 review of Wittgenstein's Remarks on the Foundations of Mathematics:

[Intuitionism] goes beyond finitism because it makes statements concerning all possible constructions, which certainly do not constitute a concrete totality. [. . . ] undecided propositions, and even implications between such propositions, may be used as premisses in implications, i.e. one makes assertions which involve an hypothetical proof, namely a proof of the premise, though the totality of all proofs is not concretely specified [. . . ] Finitist mathematics does not use the general notion of a constructive proof at all, in fact it might be said to avoid logical inferences (which involve an impredicative concept of proof ) because it is restricted to purely combinatorial operations. (Kreisel, 1958, pp.147-148; emphasis mine) Later Kreisel added a twist: in 'Mathematical logic' [START_REF] Kreisel | Mathematical logic[END_REF] he accepts a certain theory as constructive, even though on the interpretation he proposes it is not predicative, on the ground that the Proof Interpretation is not predicative either:

We give here a formulation for intuitionistic logic which is proof theoretically equivalent to R [Feferman's 1964 system of predicative analysis]. [. . . ] [N]ote that, for the interpretation of Section 2 [i.e., the Proof Interpretation], this theory does not have predicative character at all, because the intuitionistic logical operators are themselves defined self-reflexively. (Kreisel, 1965, p.176, 3.531) (Note the use of 'self-reflexive'.) Myhill in 'The formalization of intuitionism' of 1968 comments that it is an ingenious ad-hominem argument (p.337), and indeed it is not an argument that settles the matter.

Brouwerian implication is predicative and parametrically polymorphic

Myhill goes on to say that 'Brouwer's own practice leaves the issue [of predicative vs impredicative intuitionism] quite undecided'. That impression is based on cases in which Brouwer seems to countenance certain impredicative definitions, of which we will see examples below. But I will argue that this is only seemingly so, and that Brouwer did not accept impredicative definitions. In particular, he had notions of proof, function, and domain that allow for an understanding of implication that is predicative. Readers familiar with the literature on Martin-Löf's Constructive Type Theory will see a similarity of the account presented in this section with the conception of type theory as a predicative open-ended system with an infinite series of expanding universes; in particular, with Michael Rathjen's point 'that all functions that deserve to be called effective must at least be definable in a way that is persistent with expansions of the universe of types' (Rathjen, 2009, p.427). My aim here is not to analyse such similarities but to present, for its own sake, the older Brouwerian wherewithal that happens to bring this similarity about.

Brouwer held that mathematics consists first of all in mental acts of construction [START_REF] Brouwer | Over de Grondslagen der Wiskunde[END_REF], and Heyting explained the relation between such constructions and proofs as follows:

If mathematics consists of mental constructions, then every mathematical theorem is the expression of a result of a successful construction. The proof of the theorem consists in this construction itself, and the steps of the proof are the same as the steps of the mathematical construction. (Heyting, 1958, p.107) After certain acts of mental construction have been carried out, these may in reflection, be objectified. For Brouwer this is one form (the nonlinguistic one) of 'second-order mathematics': the mathematical viewing of mathematical acts (Brouwer, 1907, pp.98,119n,173). There is, then, a primary sense of proof as process, and a secondary one of proof as objectified process, and the object constructed in the process is the whole of the constructed objects and relations between them that make the proved proposition true; a state of affairs.

In order to keep proofs in Brouwer's sense, that is proofs in the sense of episodes in the mental life of the Creating Subject, terminologically distinct from proofs in the sense of linguistic or abstract objects outside the mind, we may propose to call Brouwer's proofs demonstrations [START_REF] Sundholm | The proper interpretation of intuitionistic logic. On Brouwer's demonstration of the Bar Theorem[END_REF]; the ambiguity between demonstration as act and demonstration as object is accepted and dealt with by adding the appropriate qualification.

The most memorable example of Brouwer's use of demonstration objects is in his paper 'Über Definitionsbereiche von Funktionen' (Brouwer, 1927b), in which he gives a demonstration of the Bar Theorem and in footnote 8 adds this elucidation: Just as, in general, well-ordered species are produced by means of the two generating operations from primitive species (see my paper [Brouwer 1927a, p. 451]), so, in particular, mathematical demonstrations ['Beweisführungen'] are produced by means of the two generating operations from null elements and elementary inferences ['Elementarschlüssen'] that are immediately given in intuition (albeit subject to the restriction that there always occurs a last elementary inference). These mental mathematical proofs ['gedanklichen Beweisführungen'] that in general contain infinitely many parts ['Glieder'] must not be confused with their linguistic accompaniments, which are finite and necessarily inadequate, hence do not belong to mathematics.

The preceding remark contains my main argument against the claims of Hilbert's metamathematics. (Brouwer, 1927b, p.64n8) Brouwer says here that a Beweisführung is a species, one of Brouwer's two constructive analogues to a classical set, 17 and a well-ordered one at that. What will be of particular interest for the present purpose is not that individual demonstrations are species, but that, being mathematical objects, demonstrations may be collected in a second-order species. Brouwer defined species as properties supposable for mathematical entities previously acquired, and satisfying the condition that, if they hold for a certain mathematical entity, they also hold for all mathematical entities which have been defined to be equal to it, relations of 17 The other one is the spread, which in fact is a special case. equality having to be symmetric, reflexive and transitive; mathematical entities previously acquired for which the property holds are called the elements of the species. (Brouwer, 1952, p.142) Here, an object qualifies as 'previously acquired' if either it has actually been constructed, or a method has been indicated for constructing it. 18 Higher-order species were present from the beginning: A species of order n has as elements mathematical entities or species of order n -1 (Brouwer, 1918, p.4).

An example of objects that count as all acquired even though there are infinitely many of them is of course the natural numbers, given that for them we possess a construction method. Under this definition, then, the existence of an object precedes the existence of any species that it may become an element of, and this rules out essentially impredicative definitions of elements of a species. Curiously, given his early interest in Poincaré and Russell, Brouwer never pauses to state this; Heyting later does (Heyting 18 This explicit condition was absent from the first definition of species (1918):

Unter einer Species erster Ordnung verstehen wir eine Eigenschaft, welche nur eine mathematische Entität besitzen kann, in welchem Falle sie ein Element der Species erster Ordnung genannt wird. (Brouwer, 1918, pp.3-4) It does not occur in the similar definition of 1925 either:

Unter einer Spezies erster Ordnung verstehen wir eine (begrifflich fertig definierte) Eigenschaft, welche nur eine mathematische Entität besitzen kann, in welchem Falle sie ein Element der Species erster Ordnung genannt wird. (Brouwer, 1925, p.245) It seems to make its first appearance in handwritten additions to a manuscript related to the Berlin lectures, which where held in 1927: [. . . ] moreover the admission at each stage of this construction of mathematics of properties which can be presupposed for mathematical previously acquired mathematical thought-entities, as new mathematical thought-entities under the name of species (van Stigt, 1990, pp.483-484, trl. modified) ['. . . en daarbij de toelating, in ieder stadium van dezen opbouw der wiskunde, van eigenschappen, die voor reedsch verkregen mathematische denkbaarheden ondersteld kunnen worden, als nieuwe mathematische denkbaarheden onder den naam van soorten.' (van Stigt, 1990, p.482)] At the time, Brouwer had the project of publishing the Berlin lectures as a book (van Dalen, 2005, p.551), but this addition may have been made at any time; it was incorporated almost verbatim in [START_REF] Brouwer | Richtlijnen der intuïtionistische wiskunde[END_REF], p.23. 1931, p.111, Heyting 1934, p.25). 19 As we will see, Brouwer does make the remark that species, thus defined, cannot be elements of themselves.

But the definition of a species is well-motivated independently of its constructively welcome consequence that the definition of an element of a species is always predicative. This independent motivation can be seen by considering that the existence of a species S amounts to the existence of an assignment, to each existing object a, of the hypothesis that it has the property P . As Brouwer says, a species is a 'property supposable for mathematical entities previously acquired' (emphasis mine). To accentuate the role of hypotheses in Brouwer's species is one of the virtues of Van Stigt's discussion of that notion (van Stigt, 1990, section 6.3.6); I should like to add that this assignment is a function. Its domain is every existing object (all objects 'previously acquired') because for each of them the proposition that it has that property is meaningful (whether that proposition turns out to be true, false, or undecided).

What the domain of the function can not include is objects beyond those that have been previously acquired, as otherwise to construct the domain we should be able to effect a construction out of non-acquired objects, which is impossible;20 and the associated hypotheses would not be meaningful. It would seem, then, that while this conception obviously allows for the existence of the species of the natural numbers, there could be no such thing as, for example, the species of real numbers. There are more than finitely many of them, but no construction method for generating all, and hence at no point they will all have been acquired. But Brouwer adds the following comment:

With regard to this definition of species we have to remark firstly that, during the development of intuitionistic mathematics, some species will have to be considered as being re-defined time and again in the same way, secondly that a species can very well be an element of another species, but never an element of itself. (Brouwer, 1952, p.142) With every further acquisition of objects, the function implicit in the definition of a species that generates the hypotheses P (a) should be defined anew, because this acquisition means that we want to extend the domain of that function; and the definition of the domain is a constitutive part of the definition of a function. 21 But the way in which the new objects belong to the species should be the same as that for the objects it already contains. In the case of the species of real numbers, each object that belongs to it does so because it has the property of being a convergent choice sequence of rational intervals. This warrants speaking of the redefined species being the same species as the previous one: it is a growing object.

This redefinition of species along the different stages of the Creating Subject's activity is of course analogous to the situation in the later developed and more familiar Kripke models, where a predicate may be valuated differently along a path through possible worlds ('evidential situations'), with later valuations including the earlier ones. By this I do not mean to make the farther-reaching suggestion that Kripke models explain the intended meaning of intuitionistic logic. 22 It is rather a stepping stone towards the idea that, to make the notion of a species such as Brouwer uses it fully explicit, one may associate to it an infinite sequence that starts with a species in the strict sense (i.e., with a fixed domain), and in which every further species is obtained in a separate defining act of the Creating Subject, as an extension of the previous one.

A special case of growing species are those for which we have a a method to generate denumerably many elements of it, but also a method to extend any species thereby obtained. This is very close to Russell's notion of 'selfreproductive processes and classes'.

[A]ccording to current logical assumptions, there are what we 21 So the need of redefinition in the case of certain species was implicit in the definition of species as soon as it started to include the qualification 'previously acquired entities'; see footnote 18.

22 Indeed it was not designed to meet that desideratum:

I do not think of 'possible worlds' as providing a reductive analysis in any philosophically significant sense, that is, as uncovering the ultimate nature, from either an epistemological or a metaphysical point of view, of modal operators, propositions, etc., or as 'explicating them'. [. . . ] The main and the original motivation for the 'possible worlds analysis' -and the way it clarified modal logic -was that it enabled modal logic to be treated by the same set theoretic techniques of model theory that proved so successful when applied to extensional logic. It is also useful in making certain concepts clear. (Kripke, 1980, p.19n18) may call self-reproductive processes and classes. That is, there are some properties such that, given any class of terms all having such a property, we can always define a new term also having the property in question. Hence we can never collect all the terms having the said property into a whole [. . . ] (Russell, 1906, p.36) This is from Russell's paper 'On some difficulties in the theory of transfinite numbers and order types' of 1906. Brouwer's notebooks towards his dissertation, and that dissertation itself, defended in February 1907, contain no indication that he was aware of Russell's paper. Be that as it may, the 'denumerably unfinished sets' that he introduces in the dissertation are very similar:

[H]ere we call a set denumerably unfinished if it has the following properties: we can never construct in a well-defined way more than a denumerable subset of it, but when we have constructed such a subset, we can immediately deduce from it, following some previously defined mathematical process, new elements which are counted to the original set. But from a strictly mathematical point of view this set does not exist as a whole, nor does its power exist; however we can introduce these words here as an expression for a known intention.23 [START_REF] Brouwer | Over de Grondslagen der Wiskunde[END_REF], p.148, trl. Brouwer 1975, p.82) Brouwer's definition is motivated by a preceding discussion why Cantor's second number class is not, as a whole, a constructible entity; it is a denumerably unfinished set. Following this definition are the examples of the totality of definable points on the continuum and a fortiori the totality of all possible mathematical systems. Brouwer's notebooks towards his dissertation show that he made his first remark on denumerably unfinished sets early on (probably 1905), while reading chapter 55, on projective geometry, in Russell's Principles of Mathematics (1903):

One will never be able to resolve the whole mystery of space and surfaces in such a way, that there is no hocus-pocus to it anymore; for the number of possible buildings [i.e., constructions] is denumerably unfinished, hence not surveyable. (Brouwer, no date, Notebooks 1904-1907, vol.II, p.32)24

Later, Dummett would discuss collections of that type, with reference to Russell but not to Brouwer, as 'indefinitely extensible concepts'. 25 It has been noticed that the concept of a denumerably unfinished set more or less disappears from Brouwer's writings after the introduction of choice sequences (van Dalen, 1999, p.115); with the new concept of redefined species, Brouwer could moreover subsume that of denumerably unfinished set under the latter.

Illustrative in this respect is Brouwer's assertion, in a paper of 1927, of the existence of 'the species O of ordinal numbers' (Brouwer, 1927a, p.487). Firstly, because strictly speaking there is no such thing as the species of ordinal numbers; whenever we have defined an enumeration of ordinals, this can be used to construct a new ordinal. But it is the implicit redefinitions of the species that allow Brouwer to speak this way. 26 Secondly, because he is not calling O a denumerably unfinished set here. Earlier, in a published reply to Mannoury's review of his dissertation, Brouwer had called the set of definable points on the continuum denumerably unfinished; and although that is not the same set, Brouwer here is otherwise repeating his reply to Mannoury. 27 Similarly, in the Cambridge Lectures of 1946-1951 he can accept the species of all species of real numbers (Brouwer, 1981, p.26n),28 and he could, a fortiori, have accepted the species of all species of natural numbers. 29Implicit redefinition of a species is also essential to considerations whether some hypothetical object would belong to a certain species: This is possible because, on Brouwer's conception of existence, to reason about a hypothetical object is to reason under the hypothesis that that object has been acquired, and hence that the species has been redefined accordingly.

And just as in the case of the species, the function that is implicit in its definition may have to be redefined time and again, so will every function defined on such a species. The reason is again that the change in the species which is the domain of the function necessitates a redefinition of the function, even though the way the new function acts on the elements of its domain is the same as for the old function. These redefinitions of a function on a species can be made explicit as an infinite sequence of functions parallel to the infinite sequence of species.

The one thing that needs to be verified is that from the mere schemata of the species and the function defined on it a sufficient justification can be found for the constructibility of such functions on arbitrary elements of the species. In the case of demonstration, the most obvious and most frequently used property is that a demonstration of A has conclusion A. If that is all the information that the function will use, then it will indeed work for arbitrary demonstrations of A. But in the case of the Bar Theorem, Brouwer considered that for A = 'There is a (decidable) bar in the tree' a further structural property is known, namely that every demonstration object of A can be put into a specific canonical form.

In Brouwer's view, as we saw, demonstration objects of propositions are themselves objects of mathematics and hence may become elements of species. The species of demonstration objects of A is not an example Brouwer gives explicitly. But when we understand implication as There exists a function f that transforms any element of the species of demonstration objects of A into an element of the species of demonstration objects of B our understanding should reflect the fact that both this function and the species that is its domain (and, perhaps, the species that is its range) are growing objects. As constructions, these take the form of infinite sequences. Hence, that formulation is to be taken as shorthand for There exists an infinite sequence of species of demonstration objects of A indexed by their stage of definition m, and an infi-nite sequence of functions f m , each extended by the next, such that f m transforms any element of the species of demonstration objects of A at stage m into an element of the species of demonstration objects of B at stage m.

f : A → B = A 1 ⊆ A 2 ⊆ A 3 • • • A m • • •     f 1     f 2     f 3     f m B 1 ⊆ B 2 ⊆ B 3 • • • B m • • •
By thus taking 'the species of all demonstration objects', and hence any subspecies 'demonstration objects of A' to be a façon de parler for an infinite sequence of ever larger species, and a function on such a species to be a façon de parler for an infinite sequence of functions that all have been, or will be, defined according to the same schema, an understanding of implication becomes possible that does not require quantification over the totality of demonstration objects. 30From the perspective of modern type theory, and the theory of programming languages, one would not call it a façon de parler, but rather an implementation, namely, of parametric polymorphism. 31 A function is parametrically polymorphic if its arguments need not each be of one fixed type, but may come from a family of types, on which the function however acts uniformly; 32 the types of the arguments are considered to be parameters, and with different instantiations of these parameters the function takes a different shape. A standard example is a function that takes finite sequences of elements of arbitrary type and returns the length of the sequence. In the case of Brouwerian implication, as reconstructed here, a function f that proves an implication A → B is likewise parametrically polymorphic. The family of argument types it can act on consists of the species of demonstration objects of A at stage m, for all m; the function f has, so to speak, infinitely many types at once. Depending on A, the arguments of the function f may themselves be polymorphic functions (iteration of implication), but all polymorphic functions used here are bounded in that their domains are limited to demonstration objects that have been 'previously acquired'. This induces a stratification. In particular, then, none of these polymorphic functions can be an element of its own domain. The form of parametric polymorphism described here is more expressive than unstratified predicative polymorphism (where polymorphic type variables are always instantiated with non-polymorphic types), and less expressive than impredicative polymorphism (where polymorphic type variables may be instantiated with any type).33 This is known as 'finitely stratified polymorphism' [START_REF] Leivant | Finitely stratified polymorphism[END_REF]; the finiteness comes naturally in Brouwerian intuitionism, where mathematical construction acts are taken to proceed in an ω-order, so that any stage of the Creating Subject's activity has only finitely many predecessors, and hence by stage n there exist only the finitely many species of demonstration objects of A at stage m < n.

From this point of view, the upshot of the present account, then, is that not only is intuitionistic logic an appropriate logic to reason about parametricity,34 but, on a Brouwerian conception of logic at least, it does itself arise from parametricity. There is no circularity because for Brouwer logic depends on mathematics, not the other way around, and parametricity is a mathematical phenomenon. 35Heyting's formalisation of species in 1930, which predates the discussion of impredicativity in the Proof Interpretation, is set up in a way that, in hindsight, has the effect of specifically blocking parametric polymorphism:

With this notation it is not possible to extend the domain of a mapping without changing the name of the mapping. If one has defined e.g. the function sin on the domain of the real numbers, and wishes to extend it to the domain of the complex numbers, one from now on needs to refer to that which so far was called sin by sin (real numbers) (Heyting, 1930b, p.12, trl. mine). 36 And Heyting in 1956 defines species in such a way that the need to redefine them, together with functions defined on them, is lost sight of, or rather, is suggested not to exist: Definition 1. A species is a property which mathematical entities can be supposed to possess (L. E. J. Brouwer 1918, p. 4;1924, p. 245;1952, p. 142).

Definition 2. After a species S has been defined, any mathematical entity which has been or might have been defined before S and which satisfies the condition S, is a member of the species S. (Heyting, 1956, section 3.2.1, emphasis mine) This is of importance for a historical understanding of the discussion of impredicativity in intuitionism, because at least until the publication of Brouwer 1975, Heyting's book was a, if not the, major reference in the discussion.

The present analysis of Brouwer's species and functions on them also allows for the weak impredicativity that Gödel indicated (see above, p. 4). Gödel was referring to the fact that the definition of a computable functional from a low type to another low type may refer to functionals of arbitrarily higher types; for an implication this corresponds to the idea that a proof of it may contain proofs of statements that are arbitrarily more complex than the antecedent or the consequent. In his Russell paper, Gödel had argued that, if one accepts Russell and Whitehead's axiom that functions occur in propositions only extensionally (introduced in the second edition of Principia, pages xl-xli), then definitions of functions exhibiting this kind of impredicativity 'are quite unobjectionable even from the constructive standpoint [. . . ] provided that quantifiers are always restricted to definite orders' (Gödel, 1944, p.134). On the other hand, intuitionistically that axiom would be unnatural. A construction that depends on a function f , such as a construction that is a truth-maker of a proposition referring to f , should be allowed to depend on how f is given to us. It is, however, possible to define a function at a higher type before certain functions at a lower type that are defined so as to depend on the former, as long as the higher-type function is appropriately generic; that is, as long as it is guaranteed that the higher-type function will also work as expected on arguments that are constructed after it.

Comparison with other predicative accounts of implication

Other constructive accounts of implication that, like Brouwer's, employ the strategy of stratification to give an account of implication that does not quantify over a totality of all possible proofs, are the 'theory of constructions' of [START_REF] Kreisel | Foundations of intuitionistic logic[END_REF][START_REF] Kreisel | Mathematical logic[END_REF] and [START_REF] Goodman | A theory of constructions equivalent to arithmetic[END_REF]1973a;[START_REF] Goodman | The faithfulness of the interpretation of arithmetic in the theory of constructions[END_REF] 37 and the meaning-theoretical approaches of [START_REF] Dummett | The philosophical basis of intuitionistic logic[END_REF], [START_REF] Martin-Löf | An intuitionistic theory of types: predicative part[END_REF][START_REF] Prawitz | Meaning and proofs: on the conflict between classical and intuitionistic logic[END_REF]. As these are well known, the question arises to what extent their different ways of implementing that general strategy may suggest alternatives for a Brouwerian intuitionist to adapt and adopt. I will look at the theory of constructions in Goodman's version as it was specifically adapted from Kreisel's to avoid impredicativity. The idea of canonical proofs will be discussed in quite general terms because, for all the differences that exist between the exact ways in which Dummett, Prawitz, and Martin-Löf have developed it, the fundamental differences with a Brouwerian account arise at a common level. Characteristic of all these accounts, including Brouwer's, is that the notion of a totality of all possible proofs is replaced by that of a potentially infinite collection of proofs of different levels, and an operator is introduced that reduces an arbitrary proof to one in that collection. One of the differences between Kreisel's original theory of constructions and Goodman's version is precisely that Kreisel entertained the thought of a reducibility operator but did not use it (Kreisel, 1965, pp.126-127, 2.215). The reduced proofs are such that they can be constructed 'from below', so that the explanation what a reduced proof of A is will not be circular. The explanations of implication then avoid the notion of an arbitrary proof of A, and instead appeal to that of an arbitrary reduced one. What distinguishes these ap-proaches from one another is their underlying notion of proof and the aspect of proofs that is the basis for the reduction procedure.

In the Brouwerian case, the levels are the stages of the Creating Subject's activity and, as on his conception proofs only exist in the sense of demonstrations, the reducibility operator is the trivial one.

In Goodman's modification of Kreisel's theory of constructions, the levels are identified with 'maximal grasped domains' (Goodman, 1970, pp.109-110). Goodman does not elaborate much on what a 'grasped domain' is, but he does say that it is a domain of constructions that 'has been grasped as a totality', that the sense of 'grasp' here is such that 'we cannot grasp the whole of the constructive universe, which is always only a potential totality', and that a 'maximal' grasped domain is one that 'include[s] everything which is immediately understood when their elements are understood'. For example, the natural numbers form, by themselves, a grasped domain, but not a maximal one because implicit in the species of natural numbers is that of constructive numerical functions (Goodman, 1970, p.110). There is a basic domain B, which is level 0 and includes the natural numbers; and there is an operation E to extend a level so as to obtain the next:

Given any level L, we suppose that we can extend L to a new level containing all the objects of L, all proofs about objects of L, and certain additional constructions [. . . ] We emphasize that this is not a stratification by logical type, but rather a stratification according to the subject matter of proofs.

Clearly, what does and does not belong to a maximal grasped domain is, in its dependence on what is 'immediately understood when the elements are understood', vague, and prone to grow over time, as with further experience we may come to find more to be 'immediately understood'.

The extension operation E suffers from similar problems. Goodman is aware of this: In the companion paper Goodman 1973a, 'The arithmetic theory of constructions', he writes that the rule which leads from the nth level to the n+1st is not a rule which we can understand. If it were, then we could understand the notion of proof in an absolute sense and could visualize the entire constructive universe. But that leads at once to selfreflexive paradoxes.

(I will return to the role of visualisation below.)

In spite of this vagueness, an operator F is introduced:

Suppose we have a grasped domain38 a. Then we wish a to be as self-contained as possible. Therefore, if we have any rule z, then we suppose that we can find a rule F az in the domain a with the property that, if x is in a and zx is defined and in a, then

F azx ≡ zx.
It is crucial to the conception of levels as built from below, Goodman points out, that F a applied to z yields a rule already present in a that represents z in a extensionally; z may itself have been defined at a much higher level, but the definition of F az should not depend on that of z (Goodman, 1970, p.110). Now the key claim is this:

The introduction of the reducibility operator F is made necessary by the impredicative character of intuitionistic implication. It seems to us essential to the intuitionistic position that given a fixed assertion A about a well-defined domain, there is always an a priori upper bound to the complexity of possible proofs of A. In case A is an implication, this principle already guarantees the existence of some sort of reducibility operator. (Goodman, 1970, p.111) Specifically, Goodman assumes that if a statement involves quantification over a domain of level at most p, then if there is a proof of that statement at all, there is one of level p + 1. Under that assumption, implication can be defined in a way that is not impredicative. As mentioned, such a reducibility hypothesis had been stated by Kreisel, but not used (his theory of constructions is not stratified). The hypothesis is a very strong one. Being an existence claim, it requires that such a proof at level p + 1 be obtainable from an arbitrary proof of A by a constructive method. However, in 'The arithmetic theory of constructions', Goodman states his conviction that 'All of constructive mathematics is ultimately based on finitary computation and on reasoning about finitary computation' (Goodman, 1973a, p.284). From what he goes on to say, it is clear that for Goodman 'reasoning about finitary computation' proceeds by visualisation:

These insights can always be put into the following form: a particular rule a, applied to any element of this basic universe, always gives the value ∼ T . Such an insight is evidently in ∀∃ form. It asserts that a certain rule is actually a function -specifically, the constant function whose value is always ∼ T . We can think of the insight as the visualization, or grasping, of the totality of the computations of the values of the function. The formal proof, which is a finite object, is not the insight but only a guide to aid us in the visualization of this infinite structure of computations. [. . . ] Thus we can repeat the entire construction above and consider insights which involve visualizing the whole of level one. These insights will be of level two. (Goodman, 1973a, pp.284,286) Given this conviction about what constructive mathematics consists in, the existence of the required reducibility operator may be easier to argue for, and Goodman makes an attempt in that direction:

Let us suppose we have a rule a which is not of level 0. Suppose we apply a to an object b of level 0 and obtain a result, ab, which is again of level 0. Then it might happen that the computation of the value ab involves the visualization of the whole of level zero or of some even more complicated totality. It seems to us, however, that that visualization cannot actually be essential to the computation. For, the visualization of such a totality of computations cannot make it possible for us to make any computation other than the ones being visualized. Moreover, since the result of the computation does not involve any infinite insight, the computation of ab can only be using, so to speak, a bounded part of the infinite visualization. In other words, we are asserting that if an infinite visualization is essential to a computation, then it must occur in the result of the computation. We may imagine, for example, that the computations are given in a normal form in which the act of visualization plays the role of an ω-rule. Then, following Brouwer's proof of the bar theorem, we are saying that any operation which plays the role of a cut-rule can be eliminated, so that only visualizations which occur in the result are necessary for the computation.

It follows from this line of reasoning that if we are given a rule a which is not of level zero, then we can think of it as a rule c of level zero by simply ignoring any request for a visualization which cannot be carried out at level zero. (Goodman, 1973a, pp.285-286) Further clarification would be needed to explain what, if 'the visualization of a totality of computations cannot make it possible for us to make any computation other than the ones being visualized', and if computation is all we are interested in, would motivate introducing such a visualisation into the construction of a rule a in the first place. Be that as it may, I take it that this, or something like it, is what Goodman had in mind in the paper of 1970; it would be hard to see in what other way he could have hoped to justify the claim he makes.

As an understanding of constructive reasoning about proofs, this limitation to finitary reasoning is overly restrictive, as Kreisel justly complained in his review for Zentralblatt [START_REF] Kreisel | Review of Goodman (1973a)[END_REF].39 A more charitable reading of the 1970 paper than Goodman allows himself in his elucidation of 1973, however, is vulnerable to the point made by Weinstein that The fact that various higher order intuitionistic systems are conservative extensions of Heyting arithmetic with respect to universal decidable sentences is rather weak evidence for such a claim [of the existence of the reducibility operator], since it may just indicate our current inability to successfully exploit the intuitionistic notions. (Weinstein, 1983, p.266) 40 In conclusion of this discussion of Goodman's theory, its notion of level (maximal grasped domain) is much less clear than in the Brouwerian ac-count (demonstrations effected up to a given stage of the Creating Subject's activity), and the required reducibility operator is highly problematic.

The other constructive account of implication to consider is based on the notion of 'canonical proof', introduced by Dummett in his talk at the Bristol Logic Colloquium in 1973 and published as 'The philosophical basis of intuitionistic logic' [START_REF] Dummett | The philosophical basis of intuitionistic logic[END_REF]. (Brouwer also had a notion of canonical proof, but that is significantly different, as will be discussed below.) A canonical proof is one in which the last step towards the conclusion is the introduction of the main connective in the conclusion. The key observation is that an inference such as

(A → B) → A A → B →-E A
and indeed modus ponens generally, is not canonical. Impredicativity of the clause of the Proof Interpretation for implication then would be avoided by explaining a proposition A → B not in terms of any proof of the antecedent, but in terms of proofs that are canonical (Dummett, 1977, p.394ff). Sundholm (1994, p.149) has remarked that that requirement would be unnecessarily strong: Implication may be defined for propositions whose proofs can be reduced to canonical form. The function f that proves A → B would then begin by performing that reduction. Of course also this latter way of going about it depends for its success on the existence of a proof that is wholly canonical.

The reduction procedure would fulfill the role of the reduction operator in the general scheme of stratification outlined above; the stratification would have only one level, that of the canonical proofs. The status of the reducibility thesis that every proof is equivalent to one in canonical form depends entirely on one's exact notion of proof. In Martin-Löf's type theory, proofs are reducible to canonical form by definition: in that theory, that an object a is a proof of proposition A means that a is ultimately reducible to a proof in which all steps are canonical. The reduction of the former to the latter is a mechanical procedure based on the syntax of the language. Any object that does not allow for such canonisation is for that reason not a proof. For those not accepting that approach, the reducibility thesis is a very substantive one. Dummett, who never discussed Martin-Löf's work in detail, 41 let alone adopt particular ideas of it, 42 never quite managed to find a justifiable alternative construal. That the attempt, in the first edition of Elements of Intuitionism, to identify canonical proofs with normal derivations in a formal system was problematic was acknowledged there by Dummett himself (1977, pp.400-403), 43 and likewise he considered the reworked conception in The Logical Basis of Metaphysics of 1991 'very shaky ' already then (1991b, p.277). 44 In the second edition of Elements of Intuitionism (2000), Dummett instead chose to argue that impredicativity of implication is harmless. The particular case he discusses is that of (B → C) → D. The ability to understand proofs of the antecedent would seem to require an ability to survey of all possible proofs of it, because there is no a priori limit to the complexity of an operation transforming proofs of B into a proof of C. This would threaten compositionality of meaning, as understanding (B → C) → D then presupposes an understanding of propositions that are of the same or greater complexity than its own. But, Dummett argues, this is not so; all that is really required to understand the antecedent is the ability to recognise of an operation that it is effective and that it will transform any proof of B into a proof of C. 'We need not survey or circumscribe possible such operations in any more particular way than this' (Dummett, 2000, p.274).

Be that as it may, there are very general reasons why to a Brouwerian the meaning-theoretical approach to logic exemplified in the work of Dummett, Prawitz, and Martin-Löf, 45 is not attractive; and the differences are of mathematical significance, as seen in the example of the Bar Theorem, of which there is a demonstration on a Brouwerian construal of that term but 41 Sundholm informed me that part of the motivation behind his 'Vestiges of realism' (1994) was to encourage Dummett to do so; alas, Dummett in his published reply did not seize this opportunity.

42 I will leave it to others to determine how easy or difficult this might be, given Dummett's other theoretical commitments. See, for a start, Sundholm 1994 and Dummett's reply, Dummett 1994. 43 See also Prawitz 1987, section 8, and Weiss 1997. 44 On this point also Prawitz 1994, p.375 and Sundholm 1998, pp.205-209. 45 It should be noted that of these three, it is in various ways Martin-Löf's approach that comes closest to Brouwer's; I have in mind here in particular the role of the difference between proof objects and demonstrations, the importance accorded to acts more generally, and its functional character; see also footnote 50. But I share Veldman's reservations having to do with the homogeneity of the notion of type and with the largely linguistic character of the theory (Veldman, 1984, pp.312-313); I would say these are typical for an ontological descriptivist faced with meaning-theoretical foundations (Sundholm & van Atten, 2008, section 5). not a meaning-theoretical one. 46 These general reasons have been discussed in [START_REF] Sundholm | The proper interpretation of intuitionistic logic. On Brouwer's demonstration of the Bar Theorem[END_REF] We there characterised Brouwer's views as 'ontological descriptivist' as opposed to meaning-theoretical; an ontological descriptivist is someone for whom 'the correctness of a knowledge claim is [. . . ] ultimately reduced to matters of ontology' (Sundholm & van Atten, 2008, p.71), and meaning theory plays no ultimate role. Here I should like to make, in that light, some remarks on Brouwer's notion of canonicity and its differences from the meaning-theoretical notion of canonicity.

Canonicity as appealed to by Brouwer in 'Definitionsbereiche' (1927b, p.64), is not that of a small set of general steps into which any proof can be analysed. His notion is general with respect to structure only in the sense that for him mathematical demonstrations are species that are wellordered; 47 but they are not general with respect to what the canonical steps are. They may vary from case to case, as is clear from the example of the the three canonical steps that figure in Brouwer's analysis of demonstrations that a tree is barred. The only criterion for canonical steps is that they be 'immediately given to intuition' (Brouwer, 1927b, p.64n8) 48 . Such intuitive givenness will depend on the structure of the specific objects involved in the demonstration, 49 and on the specific property to be established. Here lies also the reason why Brouwer's thesis that if there is a demonstration that a tree is barred, then there is one in the canonical form he specifies, does not presuppose a grasp of all possible means to establish the presence of a bar, which is an open-ended collection. The three canonical steps Brouwer specifies are obtained not from such a grasp, but derived directly from properties of the objects involved: Any other way to show that all choice sequences passing through a given node in the tree meet the bar would imply the presence of restrictions on those sequences that are not stated in 46 Constructivists of other stripes often accept the principle of bar induction as primitive, an alternative that Brouwer had indicated in Brouwer 1927b, p.63n7. As a curiosity, I mention that Gödel once suggested that a normal form for all mathematical proofs might be found, and expressed the hope of proving the Bar Theorem from that (van Atten, 2015b, p.223).

47 More precisely, they are 'pseudo-well-ordered': a well-ordered structure of which the elements are subsequently marked 'empty' or 'full', depending on whether they play a role in the demonstration or not (Brouwer 1927b, p.64n8 andBrouwer 1981, pp.46-47).

48 'der Intuition unmittelbar gegeben' 49 One may wish to generalise, with Husserl, the notion of syntax, and distinguish between the syntax of linguistic expressions and the syntax of categorially formed objects: Husserl 1974, section 42b-d and Beilage I; Husserl 1976, section 11;Husserl 985b, p.247n. the hypothesis of the Bar Theorem. (This suggestion will be worked out in a later note.)

Brouwer's notion of canonicity then is in particular not constrained by linguistic forms, of which logical form would be an example. 50 This view is expressed already in Brouwer's dissertation: While thus mathematics is independent of logic, logic does depend upon mathematics; in the first place intuitive logical reasoning is that special kind of mathematical reasoning which remains if, considering mathematical structures, one restricts oneself to relations of whole and part; the mathematical structures themselves are in no respect especially elementary, so they do not justify any priority of logical reasoning over ordinary mathematical reasoning. [START_REF] Brouwer | Over de Grondslagen der Wiskunde[END_REF], p.127, trl. Brouwer 1975, p.73) And even though Brouwer did not at that point have his notion of canonical demonstration yet, he was already at that stage prepared to allow that the structure of a mental demonstration and the structure of a linguistic representation of it do not coincide:

Even in domains of mathematics where no relations of whole and part enter, the relations which were in the mind are often transformed into relations of whole and part, when they must be communicated verbally to other people; hereby the usual language of mathematics is imbued with that of logical reasoning. However, this fact is due only to the centuries-old tradition of logical terms in language, in connection with its limited vocabulary. [START_REF] Brouwer | Over de Grondslagen der Wiskunde[END_REF], p.128n, emphasis Brouwer's, trl. Brouwer 1975, p.73) 50 As Kreisel pointed out, for Brouwer the (introduction and elimination) rules for the logical connectives would not define them, but describe (languageless) mathematical operations for which they have been recognised to be valid (Kreisel, 1965, p.122, 2.121). In this particular respect, functional interpretations of intuitionistic logic come closer to what intuitionists mean than meaning-theoretical accounts depending on cut elimination (such as Dummett's and Prawitz', but not Martin-Löf's): From the intuitionistic point of view, the former track the original languageless process of construction, whereas the latter yield a linguistic object that is no longer a direct representation of that process. (This footnote was inspired by Kreisel & MacIntyre 1982, p.231. I thank Göran Sundholm for his emphasis, in discussion of this footnote, that Martin-Löf's Constructive Type Theory is a functional interpretation.)

By the time of the Bar Theorem, Brouwer exploits another structural difference: demonstrations, conceived of as mental objects, are in general potentially infinite, whereas expressions in the languages we actually use are finite. This contrast is brought up by Brouwer as his main argument, in 1927, against Hilbert's formalism (quoted on p. 14 above); it likewise serves to draw a contrast to the meaning-theoretical tradition.

That is, inductively. It is possible to define the species of subsets of a given infinite set, but not to generate its extension; see p. 19 below on Brouwer's acceptance of the species of all species of real numbers. In his criticisms of Cantorian set theory in his dissertation, Brouwer rejects arbitrary exponentiation, but does not go into the notion of power set. See on this point van Dalen 1999, p.113. See also Poincaré 1909 (thanks to Thierry Coquand for the suggestion).

The Brouwer-Kripke Schema can be used to construct an intuitionistic analogue of sorts to P(N )[START_REF] Van Dalen | The use of Kripke's schema as a reduction principle[END_REF]. For an analysis of that schema, see van Atten 2018.

For a discussion of the principle of induction, see van Atten 2015a; for Troelstra's Paradox, van Atten 2017.

This is done in 'Basic Logic', e.g.,[START_REF] Ruitenburg | Basic logic and Fregean set theory[END_REF]

[The typescript erroneously has 'XI', as had the original publication of Gödel's Russell paper(Gödel, 1944, p.134).]

In Brouwer's work one finds various applications of it avant la lettre; see van Atten 2009, section 3.1.

'die aus jedem Beweis für a zu einem Beweis für b führt'.

Gödel says this example shows 'the character of the axioms assumed by Heyting', but in Heyting's paper this one is not an axiom but a theorem(Heyting, 1930a, p.49, 4.3). In a footnote, Heyting says that he had considered it an axiom, until Glivenko pointed out to him that it was derivable.

Gödel no date, Series IV, box 7b, folder 26, document #040113, page 22. Work of Kurt Gödel used with permission. Unpublished Copyright (1934-1978) Institute for Advanced Study. All rights reserved by Institute for Advanced Study.

Gödel Papers, 9b/144, item 040454, pages 13, end of note (j), 9b/144, item 040456, pages 6, end of note (j), and item 040459, pages 6, end of note (j); and Gödel 1990, p.274 note f.

[Brouwer 1927b]

'The author has begun this work while at the Institute for Advanced Study in Princeton, to which the author would like to express his gratitude for its giving him an opportunity to ponder on the foundations of mathematics, specifically to Professors Kurt Gödel and Georg Kreisel for many strict criticisms and valuable discussions on this work at that time.'(Leopoldt, 1975, p.2)

These passages confirm Beeson's supposition(Beeson, 1985, p.52) that Heyting's intention was to insist that species be defined predicatively.

This means also that the function cannot be a member of its own domain; see the postscript to van Atten 2017.

['Intention' translates the Dutch 'bedoeling'.]

'Men zou het heele mysterie van ruimte en vlakken nooit kunnen ophelderen zóó, dat er geen hokuspokus meer aan is; immers het aantal mogelijke gebouwen is aftelbaar onaf, dus niet te overzien.'

First in 'The philosophical significance of Gödel's Theorem'[START_REF] Dummett | The philosophical significance of Gödel's theorem[END_REF], without reference to Russell. For a more elaborate discussion, with the reference, see Dummett 1991a, pp.316-319. Various connections can be made also to the discussion of such concepts by[START_REF] Shapiro | All things indefinitely extensible[END_REF] in their 'All things indefinitely extensible

'. 26 Thus, I do not share the view expressed inGielen et al. 1981, p.127 that Brouwer's accepting this species O is an indication that over the years he had become 'more

liberal'.27 See[START_REF] Mannoury | Over de grondslagen der wiskunde[END_REF] Brouwer 1908 (pp.162 and 170 of the reprints in van Dalen 2001), and, for further discussion of 'denumerably unfinished sets',[START_REF] Kuiper | Ideas and Explorations. Brouwer's Road to Intuitionism[END_REF]

section 7.6.2.28 In contrast, its editor, Dirk van Dalen, in a footnote(Brouwer, 1981, p.26n18) comments that 'Brouwer literally quotes the power set of the reals'. (He continues by pointing out that Brouwer does not actually need the power set for the example he

gives on that page.)29 Heyting (1962, p.195) considered it 'doubtful' that these formed a species, and preferred not to use the notion.

Independently, a formal semantics showing a structurally similar approach to intuitionistic implication has simultaneously been developed in Tabatabai 2017.

 31 The notion was introduced in a lecture course by ChristopherStrachey in 1967, published as Strachey 2000. See also[START_REF] Cardelli | On understanding types, data abstraction, and polymorphism[END_REF]. Simultaneously with the first preprint of the present paper, the preprint Pistone 2017 appeared, which draws attention to the epistemological significance of parametricity for the study of impredicativity, there in the context of consistency arguments for impredicative

systems.32 In intuitionistic mathematics, that should not mean that the function cannot inspect its arguments at all; in the Bar Theorem, where non-canonical proofs of the antecedent are to be transformed into canonical form, on which then a proof of the consequent is based, it is even essential that one can. What cannot be done is to treat, upon inspection, different arguments instantiating the same polymorphic type differently.

It would be interesting to know more, historically, about Brouwer's knowledge of Russell's ramified theory of types.

For an overview, see Meseguer 1989. Of particular interest is also McCarty 1991, which relates polymorphism to Brouwer's notion of apartness.

Conversely, the notion of parametricity is broadly applicable in mathematics. See[START_REF] Hermida | Logical relations and parametricity -A Reynolds programme for category theory and programming languages[END_REF]

'Bei dieser Schreibweise ist es nicht möglich, das Gebiet einer Abbildung zu erweitern, ohne die Benennung der Abbildung zu ändern. Wenn man z.B. die Funktion sin für das Gebiet der reellen Zahlen definiert hat, und man will sie auf das Gebiet der komplexen Zahlen erweitern, so ist man genötigt, dasjenige, das bisher sin hieß, weiterhin durch sin (reellen Zahlen) anzudeuten.'

For a recent discussion of this theory (these theories), and further references, see[START_REF] Dean | Kreisel's theory of constructions, the Kreisel-Goodman paradox, and the second clause[END_REF]

[By this point, Goodman has adopted the convention that the grasped domains will always be understood to be maximal(Goodman, 1970, p.110).]

Kreisel will have thought of the introduction to Gödel 1958.

Since these conservativity results had not been invoked by Goodman, it seems that they were the most plausible consideration that Weinstein could think of in favour of Goodman's claim (his list of references includes neither Goodman 1973a nor[START_REF] Kreisel | Review of Goodman (1973a)[END_REF]

Acknowledgement. I am grateful to Walter Dean, Hidenori Kurokawa, Per Martin-Löf, Joan Moschovakis, Uday S. Reddy, Adrian Rezuş, Göran Sundholm, and Anne Troelstra for comments and discussion. Earlier versions (without section 4) were presented at the ASL meeting in Seattle in April 2017, at the workshop 'Critical Views of Logic' in Oslo in August 2017, at the 'Journées SND' in Paris in September 2017 and at the meeting 'Axiomatic Thinking' in Lisbon in October 2017. I thank the organisers for the invitations, and the audiences for their questions and comments. Finally, I thank the Institute for Advanced Study, Princeton, for permission to quote from unpublished material in the Gödel Papers.


F Chinesta
email: chinesta@ec-nantes.fr

A Leygue

A Poitou

S Chatel

J A Garcia

L L Gascon

Proper Generalized Decomposition of LCM models

Keywords: RTM, Permeability, Separated representations, Model reduction

Simulation of RTM processes is usually performed in 2D. Thus, only a mesh of the middle plane is needed with the associated degrees of freedom savings with respect to fully 3D modeling. However such modeling needs the definition of an equivalent in-plane permeability representing the ignored dimension (the thickness). The definition of such permeability is not a trivial task because each ply in the thickness direction can be anisotropic, being the principal anisotropy direction different from one ply to the neighbor plies. In this work we propose a novel fully 3D modeling whose computational cost is equivalent to a 2D solution. It allows addressing properly the equivalent in-plane permeability issue.

INTRODUCTION

In general the simulation of RTM processes assumes a 2D flow model. The most usual model results of combining the Darcy's law and the flow incompressibility: that results in the second order BVP:

The main issue in defining this model concerns the definition of the permeability tensor . Different techniques exist, but in that follows we are assuming that an averaged permeability has been determined for each type of reinforcement architecture.

PGD IN PLATE DOMAINS

In what follows we are illustrating the construction of the Proper Generalized Decomposition of a model defined in a plate domain with and :

(1)

We consider that the laminate is composed of P different anisotropic plies each one characterized by a well defined permeability tensor -it is assumed constant in the ply thickness-. Moreover, without a loss of generality, we assume the same thickness for the different layers of the laminate, that we denotes by h. Thus, we can define a characteristic function representing the position of each layer: ,

where . Now, the laminated permeability can be given in the following separated form:

(3)

where .

The weak form of Eq. (1) writes:

(4)

with the test function in an appropriate functional space. The solution is searched under the separated form:

(

In what follows we are illustrating the construction of one such decomposition. For this purpose we assume that at iteration the solution is already known:

(6) and that at the present iteration we look for the solution enrichment:

(7)

The test function involved in the weak form is searched under the form: that defines an elliptic 2D problem defined in the middle plane of the plate.

Computing from :

When is known the test function writes:

(17) and the weak form (9) reduces to:

Now, as all the functions involving the in-plane coordinates are known, they could be integrated in . Thus, using the previous notation, we can define:

CONCLUSIONS

This paper comes back to a recurrent issue in the numerical modelling of RTM flows, the one related to the pertinence of using 2D flow models making use of an averaged permeability of the different layers involved in the laminate. In complex situations significant deviations could be found, these deviations are being studied at present, and could justify the use of a fully 3D modelling. However, 3D simulations are reputed expensive from the point of view of the computational resources required for addressing complex scenarios. The use of separated representations as the ones involved in the proper generalized decompositions -PGD-could be an appealing alternative for addressing 3D models with a cost characteristic of 2D simulations. The application of the PGD on the fully 3D simulation of flows encountered in RTM processes constitutes a work in progress.

  the enrichment process is non-linear we propose to search the couple of functions and by applying an alternating direction fixed point algorithm. Thus, assuming known, we compute , and then we update . The process continues until reaching convergence. The converged solutions allow defining the next term in the finite sums decomposition: and We are illustrating each one of the just referred steps: all the functions involving the coordinate z are known, they could be integrated in . that allows writing equation (12) into the form (16)

  that allows writing equation (18) into the form (21) that defines a one-dimensional BVP.