Méven Cadet

Marco Panza

Francesca Boccuni

Abele Lassale Casanave

Annalisa Coliva

Pieranna Garavaso

Gerhard Heinzmann

Gregory Landini

Paolo Mancosu

Dag Prawitz

Philippe De Rouilhan

Julien Ross

Marco Ruffino

Matthias Schirn

François Schmitz

Andrea Sereni

Göran Sundholm

Jamie Tappenden

The Logical System of Frege's Grundgesetze: A Rational Reconstruction

This paper aims at clarifying the nature of Frege's system of logic, as presented in the first volume of the Grundgesetze. We undertake a rational reconstruction of this system, by distinguishing its propositional and predicate fragments. This allows us to emphasise the differences and similarities between this system and a modern system of classical second-order logic.

Preliminaries and proposals

The primary aim of Frege's Grundgesetze der Arithmetik ([18]) was to set up a formal system, that he called 'Begriffsschrift' (FGGBS, from now on) 1 , within which it should have been possible to get both a formal theory of natural numbers, and a formal theory of real numbers. Frege's purpose was to obtain these theories by adding the appropriate explicit definitions to such a system 2 . To make this possible, he included in FGGBS two axioms dealing with value-ranges of functions-the infamous Basic Law V and the Basic Law VI, involving, together with extensions, Frege's operator of definite description-and based on them to explicitly define a two-argument first-level function-the function ξ ζ, in Frege's notation-, conceived in order to dispense with higher-level functions 3 . Frege considered these ingredients of his system to be perfectly logical in nature. Hence, he did not present his whole system as resulting from the addition of non-logical axioms and definitions to an underlying system of logic, independent both of value-ranges and of definite descriptions, provided by the remaining axioms-the Basic Laws I, IIa, IIb, III, and IV-together * We thank, for valuable remarks, suggestions,

with a number of deductive rules. Even though this underlying system can be easily identified and is close to the one that Frege had offered some years earlier in his booklet Begriffsschrift4 -which involves, indeed, no analogue of Basic Laws V and VI and makes, then, no mention of value-ranges and of definite descriptions-, in the Grundgesetze, he made no effort to separate, within his theories of natural and real numbers, what depends on laws V and VI from what is, instead independent of them, and, thus, of value-ranges and definite descriptions. On the contrary, he pervasively used the function ξ ζ to avoid the appeal to higherlevel functions, even when this use would have dispensed him from appealing to value-ranges and definite descriptions. These play, then, a pervasive role in Frege's deductions, often without intrinsic necessity [START_REF] Burgess | Fixing Frege[END_REF] .

Despite this, we know, that, whereas the whole FGGBS is provably inconsistent, the subsystem provided by Basic Laws I, IIa, IIb, III and IV, together with the corresponding deductive rules is not, and it is in many respects analogous to a modern system of full second-order predicate logic. This analogy goes with a number of important differences, however. The purpose of our paper is to emphasise some of these differences, by suggesting a reconstruction of such a subsystem, which is intended to both follow the modern usual standards of exposition, and to be faithful to Frege's conceptions, especially in what makes them contrast with other conceptions, nowadays quite standard and on which modern systems of predicate logic are based. This double intent makes our purpose distinct from that of a number of other presentations and critical discussions of Frege's conceptions and systems of logic (which the reader can find, for example, in [42], [12], [5], [35], [1], [25], [31]).

The adoption of modern standards of exposition apart, there are, however, some important differences between our reconstruction and Frege's original presentation.

One of them pertains to our focusing on a fragment of Frege's whole system, to which he does not seem to have been willing to assign a distinct role [START_REF] Cauchy | Cours d'analyse de l' École royale polytechnique[END_REF] . This goes together with our distinction between a propositional and a second-order system. Moreover this distinction does not correspond to any distinction that Frege would have emphasised in the Grundgesetze. Though many of the arguments and considerations included in the first part of this treatise ( [18], § § I.1-I.52) [START_REF] Demopoulos | Frege and the rigorization of analysis[END_REF] are inescapably propositional in nature, he was, in fact, unconcerned, both in this part, and in the successive ones, with a clear identification of a propositional fragment of his whole system. Comparing the Grundgesetze with the Begriffsschrift could certainly offer another picture, since the system offered in the latter does not only involve, as we have said above, neither value-ranges nor definite descriptions, but also includes a propositional fragment which is much more easily separable from the whole system. Still, it seems important to us to notice that in the Grundgesetze, to which we shall here limit our attention, things go otherwise.

Another often mentioned radical difference between Frege's conception of logic and our own depends on his not making a clear separation between the syntax of his system and the meaning to be attributed to the symbols involved in it. As it has been often remarked, this results in his interweaving syntactical and semantic aspects (at least with respect to the usual modern conception of the distinction between syntax and semantics). Though our reconstruction will largely reflect this attitude, we shall not insist on this wellknown feature of Frege's exposition. This is only an aspect of a more general attitude with regard to the nature and role both of logic and of formal languages, which we shall not focus on, though we hope that the discussion on this matter, quite intense at present, could benefit from the reconstruction we offer. In fact, our reconstruction is so conceived as to make its syntactical ingredients easily identifiable, so as to allow to separate them from the semantic ones. Doing this would result in a rendering of the purely syntactical features of Frege's system. It is noteworthy that this rendering would stand on its own. This shows that Frege's interweaving syntactical and semantic aspects does not result in making the former intrinsically dependent on the latter. Their actual dependence only pertains to Frege's own way of looking at them, which our reconstruction is intended to reflect.

For this purpose, it seems to us indispensable to begin with a discussion of Frege's notion of a function, aiming both at setting some relevant features of this notion and at emphasising the basic role it is intended to play in FGGBS [START_REF] Demopoulos | Frege's Philosophy of Mathematics[END_REF] . This will also be the occasion to emphasise some relevant aspects of this system. This is the purpose of § 2. The next two § § are instead devoted to our reconstruction: § 3 focuses on the propositional fragment of FGGBS, § 4 focuses on its second-order one. 2 Frege's Notion of a Function and Other Related Aspects of FGGBS

The Historical Background

Frege presented FGGBS as a general theory of objects and functions. He did not only suggest to replace, as he had already done in the Begriffsschrift ( [14], p. VII), the subject/predicate duality, on which logic had been classically based before him, with the argument/function duality, but he also claimed that "objects stand opposed to functions", declared to "count as objects everything that is not a function" ( [18], § I.2, p. 7; [22], p. 7 1 ), and identified logical constants themselves with appropriate functions. In short, he grounded not only the presentation of his system, but also his very conception of it, on the notion of a function in its opposition to that of an object. This depends on his adopting a peculiar view of the nature of functions. Many aspects of this view are left implicit in the Grundgesetze. Others are set fourth, instead, in the same time as FGGBS is expounded. An example is the remark with which Frege opened his treatise (Foreword and Introduction apart: [18], § I.1, p. 5; [22], p. 5 1 ):

If the task is to give the original reference [Bedeutung] of the word 'function' as used in mathematics, then it is easy to slip into calling a function of x any expression [Ausdruck ] that is formed from 'x' and certain determinate numbers by means of the notations [Bezeichnungen] for sum, product, power, difference, etc. This is inappropriate [unzutreffend ], since it presents [hingestellt] the function as an expression, since in this way a function is depicted [hingestellt] as an expression, as a combination of signs [Verbindung von Zeichen], and not as what is designated [Bezeichnete] thereby [START_REF] Demopoulos | On logicist conceptions of functions and classes[END_REF] . One will therefore be tempted to say 'reference of an expression' instead of 'expression'.

It is not clear who or what Frege had precisely in mind in advancing this warning. But it is a matter of (historical) fact that this warning can be read as a reproach to many 18th-century mathematicians, which had, instead, openly defined functions as expressions. A relevant example is Lagrange, whose Théorie des fonctions analytiques includes the following definition ( [30], § 1; [28], Introduction, p. 1):

One calls 'function' of one or several quantities any expression of calculation [expression de calcul ] into which these quantities enter in any way whatsoever combined or not with other quantities which are regarded as having same given and invariable values, whereas the quantities of the function may receive any possible value. This definition is quite surprising for us, since it seems not only to interweave, but rather to mix-up the syntactic level of expressions with the semantic level of quantities: how can, indeed, a quantity properly enter an expression? Accounting for the rationale of Lagrange's definition is outside the scope of the present paper (for this matter, we refer the reader to [13]). It would be enough to say that this definition was intended to be shaped so as to assign to functions a basic role in mathematics. The relevant expressions were conceived as manifestations of the operational relations induced by the arithmetical formalism appropriately extended and generalised-this same formalism that Frege was referring to when speaking of "notations for sum, product, power, difference, and so on". The quantities entering these expressions were conceived, in turn, as "algebraic quantities" ( [30], § 5; [28], Introduction, p. 3), that is, quantities fully determined by their being relata of certain particular relations of this sort ( [13], pp. 99-100 and § 2). Hence, taking functions to be expressions into which quantities enter was a way to present functions as the object matter of a theory studying the operational relations induced by such a formalism. Lagrange's main foundational idea was to consider such a theory as the base on which the whole mathematics should have been erected.

Rejecting the identification of functions with expressions was then, for Frege, a way for rejecting the idea that mathematics should have been reduced to a mere combinatorial game within a given formalism. For him, providing formal theories of natural and real numbers was a legitimate purpose-better an indispensable task to be achieved in order to get an appropriate foundation for mathematics-just insofar as the formalism involved in these theories was intended to have a content, though a logical content. A formal expression was then, for him, nothing but a way to appropriately express this content, and Lagrange's mistake, he would have argued, consisted in taking the form in which the content is expressed as the subject matter of mathematics, whereas mathematics (and logic) cannot but be concerned with the content itself.

By making this criticism, Frege was perfectly in line with the reaction of many 19th-century mathematicians against Lagrange's foundational program, a reaction emblematically represented by Cauchy's opposition to "arguments drawn from the generality of algebra" ( [6], p. ii; [2], p. 1). Still, this reaction also brought mathematicians to abstain from taking the notion of a function as the deepest conceptual ground on which mathematics should have been raised. The so-called program of arithmetization of analysis, mainly promoted by Cauchy, was, indeed, based on the idea that functions were to be defined on numbers, that is, conceived as laws connecting numbers to numbers. So conceived, the notion of a function became conceptually dependent on that of appropriate domains of numbers, namely real and complex numbers; it did not only lose its foundational centrality, but it also became unsuitable to enter a non circular definition of numbers. Hence, Frege could have certainly not conceived the notion of a function in this way and still grounded his whole foundational program on it.

In the very same years during which he was elaborating and partially realising this program, a new perspective was appearing, thanks to the work of Cantor and Dedekind. The first tentative steps in the elaboration of a theory of sets was suggesting, indeed, the possibility of explaining the notion of a function within a more general context than that provided by a theory of real and/or complex numbers, namely by conceiving a function as a law connecting a set to a set. But Frege could not have followed this path, since, for him, the notion of a set required a clarification based on that of a function [START_REF] Demopoulos | Frege's theory of concepts and objects and the interpretation of secondorder logic[END_REF] , and, indeed, his own quite wispy sketch of a theory of sets is actually based on the identification of sets with value-ranges of appropriate functions, namely concepts and relations.

The Paradox of Functions

So, what could have been a function for Frege? Despite his distinction between an expression and what is (purportedly) designated by it, Frege does not say explicitly (either in § I.1 or in other places of the Grundgesetze) that a function is that which an appropriate expression (purportedly) designates. In "Function und Begriff", he even explicitly denies that a function is the reference of a "mathematical expression", since, he argues, if it were so, "it would just be a number" ([16], p. 5; [21], p. 23). Thus, even if there is no doubt that, for Frege, functions were designated by appropriate expressions and that these expressions work as function-names-and are explicitly referred to as such ('Functionsname', in German) [START_REF] Dummett | Frege: Philosophy of Language[END_REF] -and also that, for him, recognising such different expressions went together with recognising different functions (at least for expressions differing from each other under appropriate respect), it does not seem that he would have been inclined to consider the problem solved by merely saying that functions are that which appropriate expressions designate.

In Über Begriff und Gegenstand, while dealing with the paradox of the concept horse ( [17], pp. 195-199), Frege evoked what he ha written, some years earlier, in a footnote of the Grundlagen, namely that "a concept [. . . ] is a possible predicate of a singular judgement-content, an object a possible subject of the same" ( [15], § 66, footnote (**), p. 77; [20], p. 77), then he claimed that, despite having become aware, in the meantime, of the sense/reference distinction, his view had remained "essentially the same", namely that "taking 'subject' and 'predicate' in the linguistic sense: a concept is the reference of a predicate; an object something that can never be the whole reference of a predicate, but can be the reference of a subject" ( [17], pp. 198; [21], pp. 47-48). This claim cannot be taken, however, as a positive definition of concepts, and this because of what it asserts: the sentence 'a concept is the reference of a predicate' has the form of a sentence expressing a subject-predicate judgement, namely 's is P ', and, in agreement with this very claim, 's' can only designate an object, not a concept. This is a version of the paradox, indeed.

To clarify his notion of a function, Frege considered, in § I.1 of the Grundgesetze the example of a particular numerical function, namely 2 + 3x 2 x, and argued that its "essence [Wesen]" depends on the "connection" that it establishes between the numbers put in place of 'x' and the numbers which result when this is done [START_REF] Dummett | Frege. Philosophy of Mathematics[END_REF] . Then, he claimed that for an expression to be appropriate to designate a function, it has to be "in need of completion, unsaturated", that is, it has to involve some signs used to "hold places open" for other signs, and added that the essence of a function designated by a certain expression lies in the "particular type of need of completion" manifested by this expression. Finally, he concluded that a function is in itself unsaturated.

This makes the paradox even sharper, since, if in a phrase like 'the concept Φ (ξ)', one replaces 'ξ' with an object-name, let us say '∆', one gets the phrase 'the concept Φ(∆)', which is openly awkward, since, if 'Φ (ξ)' is a function-name, 'Φ(∆)' is the name of a value of a function, which is an object, according to Frege. It would thus be odd to admit that this phrase includes an empty space, and is then unsaturated [START_REF] Ferraro | Lagrange's theory of analytical functions and his ideal of purity of method[END_REF] . Hence, speaking of need of completion and unsaturation does not solve the problem: despite the several occurrences of the term 'essence', there is nothing in the considerations offered in § I.1 of the Grundgesetze which is appropriate to provide an explicit and clear response to the frank question: what is a function? And, as a matter of fact, in the Grundgesetze such an explicit response is not offered at all. And, it cannot be offered, in fact, since any sentence like 'a function is a . . . ' is a sentence of the form 's is P ', where 's' cannot but designate an object, as said above.

No doubt, according to Frege, the crucial feature of a function lies in its power to associate arguments and values in a certain way. But what are arguments, what are values, and how can this way be identified? If an expression, belonging to an already established language-that of the theory of real numbers, for example-is given, the answers are easy. There is, thus, no difficulty in reasoning on examples, like that of the numerical function 2 + 3x 2 x14 . But how to answer these questions in general, without relying on a previous language and on the ontology associated with it? In the face of this difficulty, Frege seems to have no other resource than appealing to some metaphors, like those of holding places open, of need completion, or of being unsaturated. But, these are just metaphors. Grasping what Frege was willing to communicate through them requires, as Frege himself said, "a grain of salt" ( [17], p. 204; [21], p. 54). The next § expounds what our grain of salt suggests as an interpretation of Frege's ideas (for a better articulation and justification of what follows, we refer the reader to [33]).

Frege's Expository Language and the Role of Function-Names in FGGBS

Claiming truth or falsehood is, for Frege, the same as claiming something about objects, since truth pertains to how objects are. Hence, insofar as logic "deals [...] with being true"( [18], Vorwort, p. XV; [22], p. XV 1 ), in logic one cannot but speak of objects, or, better, logic cannot but be concerned with the ways of claiming something about objects. It follows that the only names to be included as such in the language of logic, namely in the language to be used in FGGBS, are object-names. Function-names occur within it only through the names of their values (which are object-names, as we have said above), that is, as matrices whose completion has resulted in (non-atomic) object-names, and can, then, be recognised in such names as an incomplete part of them. This is an implicit presence, then, so to say. But it is both pervasive and essential, since logic has to do with something's being true, not insofar as it deals with this or that particular object about which truth or falsehood are claimed, but rather insofar as it deals with the mere form of our claiming truth or falsehood, which, for Frege, is the same as saying that it is the general study of the different ways of naming "the True [das Wahre]" and "the False [das Falsche]" ( [18], Vorwort, p. X; [22], p. X 1 ). The True and the False are objects, indeed, for Frege, namely logical objects. Better, they are the two only elementary logical objects, epistemically speaking: any other logical object is designated in terms of its relations with them. And the different ways of naming the True and the False manifest different functions at work, since the different names of the True and the False are obtained by completion from the names of these functions.

Both for forming the (non-atomic) names of the True and the False to be used in FGGBS, and for defining other logical objects-which reduces, in fact, to get appropriate non-atomic names of them-, as well as for

p. 81):

There is a difficulty [. . . ] which can easily obscure the true state of affairs and thereby arouse suspicion concerning the correctness of my conception. If we compare the expression 'the truth-value of ∆'s falling under the concept Φ (ξ)' with 'Φ (∆)', then we see that the 'Φ()' really corresponds to 'the truth-value of ()'s falling under the concept Φ (ξ)', and not to 'the concept Φ (ξ)'. So the latter words do not really designate a concept (in our sense), even though the linguistic form makes it look as if they do.

forming statements in this system, Frege appeals to a number of basic functions working as logical constants. Both the relevant (non-atomic) names of the True and the False, and those of these other logical objects are, indeed, either names of values of these elementary functions, or names obtained from the names of these functions and of their values, according to a complex procedure, which we shall try to explain as clearly as possible in our reconstruction (namely in § § 3.2 and 4.3, above). Statements are formed, instead, as we shall see later, by appropriately transforming the names of the True and the False, according to another procedure, which we shall also try to explain (namely in § § 3.3 and 4.5, above).

These basic functions, as well as any other obtained from them, enter FGGBS just insofar as this system-or better, its language-involves names of their values, or statements obtained from these names.

In agreement with what we have said above, this language does not involve, indeed, expressions designating functions as such. In other words, no well-formed string of symbols in FGGBS designates a particular function, while, as we shall see later, some appropriate (atomic) symbols are used in it to "indicate [andeuten]" (which, for Frege, is quite different from designating: cf. [18], § § I.1, I.8, I.17; [22], pp. 5 1 , 11 1 , 31 1 -32 1 ) functions in general.

But then, where do function-names occur? The answer is that they occur within another language. By insisting on one or another of the roles that Frege assigns to it, this other language could be assimilated either to a preliminary language with respect to the language of FGGBS, or to a metalanguage whose object-language is, again, the language of FGGBS [START_REF] Frege | Die Grundlagen der Arithmetik[END_REF] . For short, we call this language, 'Frege's expository language' [START_REF] Frege | Function und Begriff. Vortrag[END_REF] . This language is used, indeed, to expound FGGBS, namely to introduce the language of this last system, defining its basic functions, and justifying its axioms and deductive rules. In this language, functions are named through unsaturated expressions, involving the appropriate lower-case Greek letters, like 'ξ', 'ζ', or 'ϕ', which are not used to designate something, but merely to hold places open for the names of the arguments of these functions, that is, either for object-names, if these functions are first-level, or for other function-names, if these functions are higher-level. Among these unsaturated expressions, some atomic ones are used to name the basic functions. This is for example the case of 'ξ = ζ', the name of the identity function, where 'ξ' and 'ζ', hold places open for object-names (since, this is a first level-function). Whatever such an unsaturated expression might be, filling all of its open places (that is, replacing the lower-case Greek letters used to hold these places open with names of appropriate arguments) results in transforming it into an object-name, the name of a value of the relevant function.

It is to understand some statements of Frege's expository language, namely those involving functionnames, or better to grasp the content that these statements are intended to communicate, that one has to have recourse to a grain of salt. This means that Frege's expository language is not purely declarative, being rather evocative, so to say, at least partially: it is used to transmit a content that a purely declarative language can hardly transmit, because of the paradox mentioned above. The grain of salt is required to disregard the paradox, and to understand the content that is to be transmitted by speaking of functions as such, either in general, or with respect to particular ones. Let us better explain ourselves. We label 'declarative' a language whose purpose is claiming truth or falsehood. This is the case of the language of any science, and, in particular, of the very language of FGGBS. We label, instead, 'evocative' a language whose purpose is to transmit ineffable content, for example communicating emotions or transferring some sorts of know-how. Our point is that Frege's expository language is evocative insofar as it is used to teach how the declarative language of FGGBS is to be used, since teaching this know-how requires speaking of functions as such, and, according to Frege's view on them, functions are just things of which one cannot speak of as such, without being victim of a paradox, if what is said about them is to be understood as a claim of a [START_REF] Frege | Die Grundlagen der Arithmetik[END_REF] Note, however, that the frank distinction between language and metalanguage, and, then, the very notion of a metalanguage, are far from having been grasped by Frege, and are in many respects at odd with his universalist conception of logic (cf. p. 11, below), with the result that merely taking this other language to be a metalanguage is not faithful to his conceptions. [START_REF] Frege | Function und Begriff. Vortrag[END_REF] Cf. footnote (17), below.

declarative language. Hence, admitting that understanding Frege's expository language requires a grain of salt, is just the same, in our parlance, as meaning that this language is evocative. Moreover, arguing that teaching how the declarative language of FGGBS is to be used requires speaking of functions is the same as meaning that using an evocative language is indispensable to prepare oneself to understand the declarative language of FGGBS17 . It is only in such an evocative language that, in agreement with Frege's conceptions of them, functions can be named as such. This is done by using unsaturated names-that is expressions involving symbols used for holding places open for other appropriate names-in a context in which these places are just not to be filled up, since filling them would transform these expressions in object-names and would bring, then, to awkwardnesses (like it happens when the phrase 'the concept Φ (ξ)', is transformed in 'the concept Φ(∆)'). In the declarative language of FGGBS, functions are, instead, pervasively shown at work, under the cloths of names of their values, but they are never named as such, that is, never shown, in their own cloths. Among the statements of Frege's expository language that have to be understood to prepare oneself to understand the formulas of FGGBS, there are those providing the definition of the basic functions of this last system. Providing such a definition consists in fixing the values that these functions take for any argument. In order to do this, Frege uses two atomic names for the True and the False-namely the name 'True [Wahre]' and 'False [Falsche]'-, and feels free both to carelessly appeal to the totality of objects, and to use appropriate letters, namely some upper-case Greek letters, as indeterminate object-names, i.e. names of unspecified objects. As a matter of fact, Frege seems to also implicitly appeal-just as carelessly, or even more so-to totalities of functions, like the totality of one-argument first-level functions, that of two-arguments first-level function, that of one-argument second-level functions whose argument is a oneargument first-level function, and so on, and uses other appropriate letters, namely other upper-case Greek letters, to form indeterminate function-names, i.e. names of unspecified functions. However, a totality of functions does not seem to be, for him, a domain of entities given as such, as it is the case for the totality of objects, but rather a space of possible functions obtained from the basic ones by appropriate means, or possibly introduced by appropriately extending the language of FGGBS [START_REF] Frege | Grundgesetze der Arithmetik[END_REF] .

This short account of the purpose and features of Frege's expository language should be enough to clarify This justifies our calling 'expository' the language Frege used for this purpose. [START_REF] Frege | Grundgesetze der Arithmetik[END_REF] The question whether Frege admitted, or even grasped a notion assimilable to the modern notion of an arbitrary function, extensionally understood-i.e. the notion of an arbitrary appropriate subset of a set of appropriate ordered pairs (for example, an arbitrary subset of the set of ordered pairs of elements of the relevant domain D of individuals, including one and only one such pair x, y for any element x of D, in the case of one-argument first-level functions)-has been the object of the discussion mentioned in footnote (8). The claim that a totality of functions is, for Frege, a space of possible functions obtained by an appropriate procedure takes side in this discussion, according to the views defended in [33]. We refer the reader to this paper for a justification of this claim. In the present paper, we confine ourselves to account for the procedures admitted within the propositional and the second-order fragments of FGGBS for generating terms conceived as names of values of functions. Though crucial for an assessment both of Frege's conception of logic and of the meaning he assigned to the statements of FGGBS, the question of how he conceived his totalities of functions is, indeed, scarcely relevant to understand the way this system and, in particular, these fragments of it, work, which is the only question we want to focus on, in the present paper.

the fact that, though rooted in a natural one, this language crucially appeals to special symbols, used for a specified purpose, and introduced for this, according to appropriate stipulations. This is, then, a partially artificial language. This is why we have decided to include an account of this language, better of its artificial features, within our reconstructions of the propositional and second-order fragments of FGGBS. We shall use a trick for this purpose: instead of fixing the language of our renderings of these fragments at once, we shall proceed by steps, beginning with the construction of some preliminary formal languages, some elements of which will be discarded in the end, and will not be included, then, in the final formal languages of these renderings, namely the languages used to form their well-formed formulas (as it will be clear above, the way we shall proceed, and the relation connecting these preliminary languages with the final ones will be crucially different in the cases of our rendering of the propositional and of the second-order fragments of FGGBS). Still, this will not dispense us from passing through an even more preliminary stage, in our reconstructions, where natural language, enriched with appropriate symbols informally introduced so as to form names both for the basic functions and for their values (and, then, open to paradox, in agreement with Frege's conceptions), will be used to define these same functions. The symbols obtained from their names, by omitting the lower-case Greek letters occurring within them to hold places open for their arguments, will then be included alone, under the form of functional constants, both in our preliminary formal languages and in the final ones. This allows us to avoid oddity with respect to the usual modern standards, but it is, strictly speaking, unfaithful to Frege's conceptions (since nothing assimilable to such constants has any place in his presentation, where these symbols only occur endowed with appropriate letters, unless when they merely refer to themselves as pure signs, as it happens in § I.6, for the symbol of negation).

Terms, Statements, and Truth

Another thing that should be clear from what has been said up to now is that Frege admitted no principled distinction between truth-values (namely the True and the False) and the objects about which one can claim truth or falsehood. The former are nothing but two particular objects, living in the same realm as any other object, without any distinction of status or type. This goes together with not considering terms as categorically distinct from statements in FGGBS: a statement is obtained by letting a special symbol precede either a name of a truth-value, or an expression obtained by appropriately transforming such a name (cf. p. 7, above). This special symbol is ' ' ( [18], § I.5): letting it precede the name of a truth-value results in the statement that the truth-value named by this name is the True; letting it precede an expression obtained by appropriately transforming such a name results in the statement that the truth-value named by whatever name resulting from this expression by coming back to a name of a truth-value (in an appropriate way, again) is the True. This means that the act of asserting something, or claiming truth or falsehood is rendered, within FGGBS, as the act of holding that a certain appropriate term, or all the terms of a class of appropriate terms refer to the True [START_REF] Frege | Was ist eine funktion[END_REF] . This makes two things clear.

The first is that the True and the False are not merely conceived by Frege as two distinct designated objects whatsoever, but as two peculiar objects having a precise intrinsic nature.

The second is that a statement of FGGBS could be properly said to be true or false only if it were admitted that this means that it embodies a reference to the True or to the False, so to say, which is not what is usually understood when it is said of a statement of a natural language that is true or false. Nothing would prevent one from adopting this parlance as a convenient convention, but it is a fact that, after having used the adjectives 'true [wahr ]' and 'false [falsch]' freely enough in the Foreword of the Grundgesetze, Frege was quite cautious in using them in the following parts of his treatise, where they appear very seldom and only three times in such a way as to openly designate a property of a statement of FGGBS [START_REF] Frege | The Foundations of Arithmetic[END_REF] . In few other cases-like in § § I.12 and I.17-he openly claimed that a statement of FGGBS holds (gilt), while in most cases he merely stated it by implying the same. In § § 3 and 4 we shall adhere to this policy.

This way of forming statements within FGGBS has deep consequences on the internal structure of the system, which we shall try to clarify in our reconstruction. One of them is that the identity sign '=' is allowed to occur both between two object-names other than truth-values (working as the terms of a modern formal language) and between two names of a truth-value. In the former case, it plays the role of our identitypredicate, in the latter, that of our connector of double implication '⇔'. This makes the isolation of the propositional fragment of FGGBS non-trivial. In particular, the problem concerns the role of Basic Law IV, which involves the sign '=' between two names of a truth-value. In order to decide whether this law is part of the propositional fragment of the FGGBS, it is not enough to look at it, as such; it is rather necessary to consider whether such a propositional fragment does require this law in order to result in a complete system of propositional logic. As a matter of fact, section § I. 51 of the Grundgesetze presents the derivation of several propositional theorems from Basic Law IV. Among them are the principles of introduction and cancellation of the double negation (that is, 'p ⇒ ¬¬p' and '¬¬p ⇒ p', in modern notation), whose derivation also has recourse, however, to Basic Laws IIb and III, which are openly second-order in nature. Insofar as these principles were admitted as axioms in the system of the Begriffsschrift (where they are numbered as statements 31 and 41, respectively), this could suggest, at first glance, not only that Basic Law I, (the only one of Frege's Basic Laws that is openly propositional in nature) is not enough, together with the deductive rules that apply to it, in order to provide a complete propositional system, but also that this is no more the case for Basic Laws I and IV taken together. This conclusion would be mistaken, however, since, as we shall prove in § 3.5, Basic Law I is perfectly sufficient alone for this purpose. Frege's appeal to other Basic Laws of FGGBS in order to prove several propositional theorems is rather a symptom of his being unconcerned with isolating a propositional fragment of FGGBS, as we have already observed in § 1 [START_REF] Frege | Translations from the Philosophical Writings of Gottlob Frege[END_REF] . [START_REF] Frege | The Foundations of Arithmetic[END_REF] The first occurrence appears within the footnote appended to § I.114, where one finds this passage: "This statement [it is not relevant here to say which it is, what is important is that it is a statement of FGGBS] is, it seems, unprovable, but it is not asserted as true [als wahr behauptet] here either, since it stands in quotation marks"( [18], I.115, footnote (1); [22], p. 1141). The second and third occurrences occurs within the Nachwort to volume II, where Frege presented his (unsuccessful) way-out to Russell's objection. There, he wrote that "the error [responsible for the paradox] can be only in [. . . ] Law (Vb) [the left-to-right implication included in Basic Law V] which must therefore be false", then, adds, some lines later, that "at least one of the two statements (77) and (82) [two theorems proved in § I.91] is false, and hence also [statement] (1) [another consequence of Basic Law V] from which they follow" ( [18], Nachwort, p. 257; [22], p. 2572). While introducing the symbol ' ', Frege said, instead, that this symbol is needed "in order to be able to assert something as true [um etwas als wahr behaupten zu können]" ( [18], § I.5; [22], p. 91). [START_REF] Frege | Translations from the Philosophical Writings of Gottlob Frege[END_REF] In the Foreword of the Grundgesetze ( [18], Vorwort, pp. VI-VII; [22], pp. VI1-VII1) one finds this disclaimer:

One must strive to reduce the number of [. . . ] fundamental laws as far as possible by proving everything that is provable. Furthermore, [. . . ] I demand that all modes of inference and consequence which are used be listed in advance [. . . ]. This ideal I believe I have now essentially achieved. Only in a few points could one impose even more rigorous demands. In order to attain more flexibility and to avoid excessive length, I have [. . . ] not reduced the modes of inference and consequence to a minimum. Anyone acquainted with my little book Begriffsschrift will gather from it how here too one could satisfy the strictest demands, but also that this would result in a considerable increase in extent. Furthermore, I believe that the criticisms that can justifiably be made of this book will pertain not to rigour but rather only to the choice of the course of proof and of the intermediate steps. Often several ways of conducting a proof are available; I have not tried to pursue them all and it is possible, indeed likely, that I have not always chosen the shortest. Let whoever has complaints on this score try to do better.

If this makes clear, on the one hand, that Frege was aware that his departure from the clear separation realised in the Begriffsschrift, between a propositional and a second-order system, was required by no intrinsic necessity, it also shows, on the other hand, that he was not considering this separation as an important benefit to be conserved for reasons of conceptual clarity. Moreover, nothing, either in this quotation or elsewhere in the Grundgesetze, shows that he was also aware that his Basic Law I is enough, together with the deductive rules that apply to it, to provide a complete propositional system.

Another thing that the previous account should make clear is that Frege's conception of logic is universalist. There was room, for him, neither for a plurality of logical systems, concerning different domains of enquiry, nor for different or restricted domains of objects. As a consequence, the very idea that his system of logic could have had different models, or even a particular model, was outside of his conceptions. He attributed to the logical constants of FGGBS, as well as to any other component of it, a fixed meaning, so conceived as to obtain appropriate definitions and prove theorems in their intended meaning. He was, then, pursuing, so to say, an ideal of absolute completeness. Any requirement of relative completeness were nonsensical for him.

This should not hide, however, that FGGBS was, for Frege, a formal proof system. Its language having been fixed and a meaning having been attributed to all the components of this language, the Basic Laws of FGGBS (i.e. its axioms) were certainly chosen-with the only notable exception of Basic Law V-among the statements of this language that manifestly hold according to this meaning [START_REF] Frege | Basic Laws of Arithmetic[END_REF] , and its deductive rules were certainly designed so as to preserve this property. Moreover, Frege justified both the latter and the former by showing that they meet these conditions. Still, a proof within FGGBS is nothing but a chain of statements following from the Basic Laws according to the deductive rules, which involves, as such, no appeal to the meaning of the relevant symbols or formulas.

In this respect, the differences between FGGBS and a modern formal system are much more subtle than those noted above. The main one depends on Frege's endorsing the so-called context principle: "not to ask for the meaning [Bedeutung] of a word in isolation, but only in the context of a statement" ([15], p. X; [20], p. XXII). Much has been written on this principle (cf. among others, [12], chapter 16-17; [34], § 4.2), and there is certainly no room here for discussing it. It is only relevant to emphasise a particular consequence of it (already mentioned above, en passant), namely the fact that, within FGGBS, non atomic object-names are generated through function-names. As a consequence, within FGGBS, getting non-atomic object-names requires passing through function-names, which, as we have said above, do not belong, as such, to the language of FGGBS. Hence, this language has to import some incomplete symbols from another, previous language, namely from Frege's expository language, and complete them appropriately. Our proceeding by steps in constructing the languages of our renderings of the propositional and second-order fragments of FGGBS is also intended to account for this fact.

Roman, Greek, and Gothic Letters

The situation is even more complex because of another feature of FGGBS, which is independent, as such, of the context principle. We have said above that Frege used upper-case Greek letters as indeterminate objectnames and others to form indeterminate function-names. This only happens in his expository language. In the language of FGGBS, the place of these letters is taken by other letters, namely Roman ones (which, according to Frege, indicate, but do not designate objects or functions: cf. p. 7, above). Above (at pp. 7 and 9) we have also said that in FGGBS statements are obtained by letting the symbol ' ' precede either a name of a truth-value, or an expression obtained by transforming such a name. Roman letters enter such an expression, and are supposed to appear only within statements (since this expression is not allowed to occur outside statements). They indicate that a statement in which they occur is universal, that is, it asserts something that holds for all objects and/or all functions. For a simple example, consider the function ξ = ζ, again. By replacing in its name 'ξ' with 'Γ' and 'ζ' with '∆', one gets a term, namely 'Γ = ∆', which is a name of the True if 'Γ' and '∆' refer to the same object and a name of the False if 'Γ' and '∆' refer to two distinct objects. From this term, one can then get the statement ' Γ = ∆', which asserts that the truth-value named by 'Γ = ∆' is the True, that is, that Γ is the same object as ∆ (note that, by definition, the function ξ = ζ is a dyadic relation, i.e. a two-arguments function whose values are truth-values; a name of whatsoever value of this function is, then, a name of a truth-value). Again, by replacing in this statement both 'Γ' and '∆' with 'a', one gets the other statement ' a = a', which asserts that the truth-value named by any term obtained from 'a = a', by replacing 'a' with the name of any object is the True, that is, that any object is identical with itself. By replacing, instead, 'Γ' with 'a' and '∆' with 'b', one gets the statement ' a = b', which asserts that the truth-value named by any term obtained from 'a = b' by respectively replacing 'a' and 'b' with the names of any objects is the True, that is, that any object is identical both with itself and with any other object. Whereas ' Γ = ∆' is not a statement of FGGBS, the statements ' a = a' and ' a = b' are. Still, neither 'a = a' nor 'a = b' are FGGBS terms. The reason is that they are not well-formed strings of symbols of its language, since, in FGGBS, Roman letters are only licensed to enter statements. It is then possible that a component of a statement of FGGBS, though complete according to the arity of the symbols that enter it, is not well-formed, which contrasts with what happens in a modern formal system. But there is more. The fact that explaining the meaning to be assigned to Roman letters in FGGBS requires appealing to statements and terms which do not involve such letters forces some deductive rules of FGGBS (namely the propositional one) to be firstly stated for statements that do not involve these letters (and, because of that, are not statements of FGGBS), and then extended to these last statements. This is another contrast with what happens in a modern formal system.

A last point to be made, before coming to our reconstruction, concerns the absence of variables in FGGBS, at least if these are conceived as is usual nowadays, that is, as components of a formal language that can enter both bounded and open formulas with respect to them (in such a way that a bounded formula with respect to a certain variable results from bounding this variable in an open one).

One might consider that the role that variables play in a modern formal language is played in FGGBS by two sorts of letters, namely Roman letters for free variables, and Gothic letters for bound ones (we shall come back to Frege's use of Gothic letters in § 4). For Roman letters, this is, for example, Goldfarb's view ( [23], p. 67). But, if this were so, it would also be clear that no single sort of letters (or symbols, in general) play in this system the same role as that which variables play in a modern formal system. Since Roman letters are neither FGGBS terms, nor are licensed to enter these terms [START_REF] Goldfarb | Frege's conception of logic[END_REF] , though the language of FGGBS includes functors, and, in FGGBS, the universal quantifier-the only one that occurs within its language-does not act on these letters, but rather binds Gothic ones. This is more than a mere syntactical difference. As we saw above, Roman letters express generality, for Frege. If they were taken to work as free variables, this would mean that, for him, generality can be expressed through indeterminacy, which is certainly not the idea of generality which is transmitted by a modern predicate language. The idea of generality transmitted by such a language, namely by the way the universal quantifier works in it, is rather that of a specification of indeterminacy by universalisation. This idea could also be detected at work in FGGBS, namely in the way the universal quantifier works there. But this is not so insofar as this quantifier operates, there, on Roman letters (which would allegedly play in this system the role of free variables) and binds them, but, rather, insofar as it operates on Greek letters (either lower-or upper-case), and transform them into Gothic ones. Once discarded the idea that Roman letters work in FGGBS as open variables work in a modern predicate language, this could suggest that what works this way are rather Greek letters. But this would also be wrong, in fact, both for lower-case Greek letters and for upper-case ones. A first reason for this, is that the former do not designate objects or functions, but merely hold places open for names of them, whereas the latter behave as indeterminate names designating objects or functions, rather than as names of indeterminate objects or functions (that is, as indeterminate individual or functional constants, rather than as individual or functional variables, properly). Another reason, which is unquestionable, is that Greek letters do not enter, as such, the language of FGGBS.

It then seems to us that all one can say on the matter of variables, concerning FGGBS, is that different sorts of symbols entering its language, or connected with it (namely Roman, Gothic and Greek letters), play, respectively, in this system, different roles that are somehow similar to the different roles that variables play in a modern predicate system, though none of these symbols works in FGGBS as variables work in a modern predicate system. This is perfectly compatible with Dummett's claim that "nothing exactly corresponding to a free variable appears in Frege's symbolism" ( [11], p. 16).

But there is more than this, in fact. Since it seems that Frege rejected the very notion of a variable as a rightful notion, both in mathematics and in logic. This is suggested by what he wrote in a short paper ( [19]) which appeared in 1904. He dealt there with analysis and arithmetic, but, clearly, the points he made also apply to FGGBS, within which both analysis and arithmetic would have to be re-cast, according to him. In short, these points are the following: "variation occurs within time" ( [19], p. 656; [21], p. 107), and neither analysis nor arithmetic have anything to do with time; though one can conceive something like a particular (physical) magnitude, which is varying (in time), "a number does not vary", since, for a variation to be conceived, something that remains the same during the time of this variation is also to be conceived, and nothing could remain the same if a number were to vary ( [19], p. 658; [21], p. 109).

These are just the ideas which are reflected by Frege's using lower-case Greek letters in function-names as mere marks of unsaturation, rather than as names of variable objects or functions, as it usually happens, and happened in Frege's times, with 'x', 'y', or 'z'. An immediate consequence of this is the impossibility for Frege to account, and then admit, anything like a direct composition of functions. Consider the simplest case of first-level functions. Let Φ (ξ) be such a function. By replacing 'ξ' in it with a function-name, say 'Ψ (ξ)', so as to get 'Φ (Ψ (ξ))', one would commit a syntactical mistake, since 'ξ' is there to hold a place open for object-names, not for function-names. Moreover, by doing that, one would not transform 'Φ (ξ)' into an object-name, as it is required, instead to any licensed replacement of 'ξ', since the function-name replacing 'ξ' cannot but be unsaturated, and this replacement would, then, transform an unsaturated expression into another unsaturated expression. According to Frege's conventions (which strictly reflected his views), there is, thus, no way to pass from Φ (ξ) to Φ (Ψ (ξ)), by directly composing the function Φ (ξ) with the other function Ψ (ξ). Something similar also holds for higher-level functions: by replacing a lower-case Greek letter, occurring within a name of such a function to hold places open for function-names, with such an appropriate name, one is intended to get, indeed, an object-name, namely a name of a value of this function, not a name of another, composed function.

This does not prevent Frege from composing functions indirectly, by passing through their values and then coming back to functions. In the case of our first-level functions Φ (ξ) and Ψ (ξ), one can, for example, operate as follows. One first replaces 'ξ' in the name of the latter with an object-name, for example 'Γ', so as to get another object-name, namely 'Ψ (Γ)'. Then, one replaces 'ξ' in the name of the former function with this last name, so as to get a new object-name, namely 'Φ (Ψ (Γ))'. Finally, one replaces in this last name 'Γ' with 'ξ', again [START_REF] Heck | The development of arithmetic in Frege's Grundgesetze der Arithmetic[END_REF] , so as to get the name of a new function, namely 'Φ (Ψ (ξ))'. With the only exception of the basic functions, all other functions occurring within FGGBS, under the cloths of (the names of) their values, are generated this way. We noted above that, within FGGBS, names of objects are generated from names of functions. This should be enough to convince the reader that the reciprocal is also true: names of functions are, in turn, generated from names of objects. The interweave between these two sorts of names-the latter of which, are not part, as such, of the language of FGGBS, as we have said-is pervasive in such a system.

All of this having been said, it is time to come to our reconstruction. In § 3, we present a formal system, which is intended to render the propositional fragment of FGGBS. Later, in § 4, we extend this system so as to render the predicate fragment of FGGBS. We call the former system 'FGGPL R ', for 'Frege Grundgesetze Propositional Logic Reconstructed', and the latter 'FGGL2 R ' for 'Frege Grundgesetze Second-Order Logic Reconstructed'. 3 Frege's Propositional System Reconstructed

Basic Functions

Let the lower-case Greek letters 'ξ' and 'ζ' be used to hold a place open for whatsoever object-name in any expression within which they occur, such an expression being intended as a function-name. This means that such an expression is allowed to be transformed in a name of a value of the relevant function-which is an object-name, in turn-by replacing each occurrence of each of these letters by the same object-name. Let also 'T' and 'F' respectively refer to the True and the False, and the upper-case Greek letters 'Γ', '∆', and 'Θ' be indeterminate object-names. This being supposed, let us admit that the truth conditions are known of any statement of the natural language having one of the following two forms:

-'Γ is T/F if ∆ is (not) T/F, and it is F/T if ∆ is (not) F/T', -'Γ is T/F if ∆ is (not) T/F and Θ is (not) T/F,
and it is F/T if it is not the case that ∆ is (not) T/F and Θ is (not) T/F', where 'is (not)' stands either for 'is' or for 'is not', and 'T/F' and 'F/T' stand either for 'T' or for 'F', alternatively. Finally, let us take

'Γ is T/F if . . . F/T if . . . ' to stand for 'Γ is T/F if . . . , and it is F/T if . . . ' .
By also supposing that 'O' denotes the totality of objects, including T and F, we can then define three first-level functions as follows:

-Let ξ : O → {T, F} be such that Γ is T if Γ is T F if Γ is not T ; -Let ¬ξ : O → {T, F} be such that ¬Γ is F if Γ is T T if Γ is not T ; -Let ζ ⇒ ξ : O 2 → {T, F} be such that ∆ ⇒ Γ is    F if ∆ is T and Γ is not T T if it is not the case that ∆ is T and Γ is not T . context principle).
Here ': O → {T, F}' is used to mean that the relevant functions take an object and give either T or F, while ': O 2 → {T, F}' is used to mean that the relevant function takes two objects (an object as ζ-argument, and another as ξ-argument) and gives either T or F, again [START_REF] Heck | Reading Frege's Grundgesetze[END_REF] .

The function ξ renders the first of Frege's basic functions, namelyξ, introduced in § I.5. It is easy to see that the value Γ of the function ξ, for Γ as an argument is the same object as Γ, whatever object Γ might be. Hence the (indirect) composition of this function with itself results in itself. This justifies the rule that Frege called 'fusion of horizontals [Verschmelzung der Wagerechten]' ( [18], § § 6, 12; [22], pp. 10 1 , 20 1 ), according to which any number of horizontal strokes like ' -', or horizontals tout-court, in Frege's parlance ( [18], § 5; [22], p. 9 1 ), fuse to each other, that is, count as only one horizontal. This allowed Frege to take the signs ' '

-¬ξ : {T, F} → {T, F} to be such that ¬Γ is F if Γ is T T if Γ is F ; -ζ ⇒ ξ : {T, F} 2 → {T, F} to be such that ∆ ⇒ Γ is    F if ∆ is T and Γ is F T if it is not the case that ∆ is T and Γ is F .
It is still a fact that neither in the Grundgesetze, nor in any other of Frege's works, there is any trace of functions that one could render this way, as well as of any other first-level function not defined on the totality of objects. Hence, to stay close to Frege's own exposition, one cannot but consider the functions ¬ξ and ζ ⇒ ξ as genuine basic (and, then, elementary, i.e. non-composed) functions of FGGPL R , and take fusion of horizontals as a consequence of the definition of the function ξ, which merely allows using the sign ' --' within the names of functions ¬ξ and ζ ⇒ ξ, without any inconvenience. It remains, however, that the mere use of this symbol within these names is enough to suggest that each of the functions ¬ξ and ζ ⇒ ξ admits two characterisations: a direct one, depending on their definition, in terms of their own arguments; and a truth-functional one, depending on the occurrence of the sign ' --' within their names, in terms of the values of the function ξ. According to the latter,

-¬ξ : O → {T, F} is such that ¬Γ is F if Γ is T T if Γ is F ; -ζ ⇒ ξ : O 2 → {T, F} is such that ∆ ⇒ Γ is    F if ∆ is T and Γ is F T if it is not the case that ∆ is T and Γ is F .
This is what allows the functions ¬ξ and ζ ⇒ ξ to play, within FGGPL R , the same role as that which the connectives of negation and implication play in a modern propositional system, though they are not, properly, connectives, that is, operators acting on sentences, but functions defined on the totality of objects [START_REF] Hintikka | The skeleton in Frege's cupboard: The standard versus nonstandard distinction[END_REF] . As a matter of fact, operatively speaking, Frege could have avoided introducing the functionξ by directly defining his two functions ξ and ξ ζ just as he did (i.e. in the way we have rendered by our definition of functions ¬ξ and ζ ⇒ ξ), but mentioning neither the former function, nor the horizontal and the negation-and conditional-strokes, that is, by taking the signs ' ' and ' ' as un-composed 28 .

Operatively speaking, the role of the functionξ in FGGBS is, indeed, only that of transforming any object in a truth-value, and this same role could, in fact, also be played by the functions ξ, ξ ζ , as well as by the first-and second-order-quantifier functions (cf. footnote 28, above), also if no appeal to the horizontal stroke (and then, implicitly, to the functionξ) were done in their explanation. Still, apart from resulting in a loss of perspicuity, this would have prevented Frege from using the identity function, both as a propositional connective (which occurs when this functions applies to two values of the functionsξ) and as a relation between two objects whatsoever (cf. p. cf. footnote 27, above). But it is a fact that Frege did not follow this road, which would have, by the way, seriously complicated his formalism and strongly modified the nature of his system. This is why we follow Frege in giving a place to the function ξ within FGGPL R . This allows us to give a precise characterisation of the atomic terms of this system.

Terms and Particular Statements

Defining the functions ξ, ¬ξ and ζ ⇒ ξ has required to appeal to the natural language endowed with some appropriate symbols used for brevity. This having been done, we are now ready to fix the language of FGGPL R . We shall do it by steps.

To begin, let L AT [FGGPL R ] be the language {Γ, ∆, Θ, Λ, Ξ, Π, Σ, . . . , --}, in which 'Γ', '∆', 'Θ', 'Λ', 'Ξ', 'Π', 'Σ', . . . have arity 0 and are called 'FGGPL R object-letters', while ' --' has arity 1, and behaves in agreement with the definitions of the function ξ. Here the ellipses are intended to remain for the same letters 'Γ', '∆', 'Θ', 'Λ', 'Ξ', 'Π', 'Σ' endowed with appropriate indexes, so as to form a potentially infinite collection of symbols, all having arity 0. This simple language is used to form FGGPL R atomic terms, according to the following stipulations: [START_REF] Hintikka | The skeleton in Frege's cupboard: The standard versus nonstandard distinction[END_REF] On the base of these two functions, one could, of course, explicitly define, by indirect composition, two other functions, working as the connectives of conjunction and disjunction. As a matter of fact, Frege observed that the functions ξ ζ and BGconditional ζξ respectively render the 'and' and the 'or' of the natural language ([18], § I.12; [22], p. 211), but introduced no special symbol to shorten the names of these functions. We follow his policy and introduce no special sign for the conjunction and the disjunction, which are rather rendered in FGGPLR by the functions ¬ζ ⇒ ¬ξ and ¬ζ ⇒ ξ. 28 If he had followed this route, he should, of course, have done the same, mutatis mutandis, also for ' ' (cf. footnote 26, above) and for the first-and second-order-quantifier functions.

St AT [FGGPL R ] .i If θ is a FGGPL R object-letter, then θ 29 is a FGGPL R atomic term. St AT [FGGPL R ]
.ii If θ is a FGGPL R atomic term, then also θ is a FGGPL R atomic term.

St AT [FGGPL R ] .iii Nothing else is a FGGPL R atomic term. Now let L T [FGGPL R ] be the language L AT [FGGPL R ] ∪{¬ --, --⇒ --}, resulting from the addition, to L AT [FGGPL R ]
, of the two new symbols '¬ --', with arity 1, and ' --⇒ --', with 2, which behave in agreement with the definitions of the function ¬ξ and ζ ⇒ ξ. This language is used to form FGGPL R terms, according to the following stipulations:

St T [FGGPL R ]
.i If θ and τ are FGGPL R object-letters, atomic terms, or terms, then θ, ¬θ and θ ⇒ τ are FGGPL R terms;

St T [FGGPL R ]
.ii Nothing else is a FGGPL R term.

It follows, of course, that FGGPL R atomic term are FGGPL R terms. FGGPL R object-letters are intended to refer to unspecified objects of any sort, which means that we suppose that there are objects, even if unspecified ones, which these letters name ( [18], § I.5, footnote 3). In agreement with the definition of the functions ξ, ¬ξ and ζ ⇒ ξ, FGGPL R terms are rather intended to refer either to T or to F, which are the only objects that FGGPL R is intended to deal with, specifically. This explains why the previous stipulations are so shaped that replacing FGGPL R terms with FGGPL R object-letters, within a FGGPL R term, might result in getting something that is no longer a FGGPL R term. To take a simple example, start with the FGGPL R term 'Γ ⇒ ∆', and replace in it 'Γ' with 'Γ'. This results in 'Γ ⇒ ∆', which is not a FGGPL R term. Replacing FGGPL R object-letters with FGGPL R terms within a FGGPL R term, always results, instead, in another FGGPL R term. This agrees with the rule of fusion of horizontals, intended as a rule for formation of terms (cf. footnote 36, below), or better as the reciprocal of such a rule. This rule is, thus, implicit in the previous stipulations, and this allows the symbol ' --' to play the role of parentheses in FGGPL R . This use of this symbol parallels Frege's use of his horizontal stroke, but is a little bit larger, since, as it will become clear in § 3.6, it also allows avoiding using parentheses to delimit the scope of the identity sign when it applies to values of the function ξ -like in the statement of Basic Law IV, for example-, whereas Frege is forced to use them for this purpose. Finally, replacing FGGPL R terms with other FGGPL R terms within a FGGPL R term always results, again, in another FGGPL R term.

If within a FGGPL R term, a FGGPL R object-letter is replaced with another such letter or with a FGGPL R term, the new term which is obtained this way remains with the initial one in a special relation, which is fixed by the following stipulation: 29 For the sake of simplicity, in the present § 3, we take the liberty of using some meta-variables intended to range over FGGPLR object-letters, terms, or object-markers, in order to form expressions involving, together with these meta-variables, some symbols of the languages

St Is.T [FGGPL R ] If θ is a FGGPL R object-letter, ϑ a FGGPL R object
L AT [FGGPL R ] , L T [FGGPL R ] and L GS [FGGPL R ]
used to form these same object-letters, terms or objectmarkers (cf. below for the definition of the languages L T [FGGPL R ] and L GS [FGGPL R ] and of FGGPLR object-markers). In this case, we assume that these last symbols refer to themselves as symbols of the object-language, and avoid any use of quotation marks. [START_REF] Lagrange | Théorie des fonctions analytiques[END_REF] Insofar as nothing forbids in this stipulation that ϑ be the same object-letter as θ, it follows that, according to it, any FGGPLR particular statement is an instance of itself.

This stipulation relies on the notion of occurrence of a FGGPL R object-letter within a FGGPL R term. The general notion of occurrence of a string of symbols within another string of symbols will play a crucial role in all what follows, with respect both to FGGPL R and to FGGL2 R . As this notion is common in modern logic, one might believe that it requires no explanation. However, among the differences between FGGPL R and FGGL2 R , on the one side, and a modern system of logic, on the other, there is one that makes the understanding of this notion in the former systems slightly different than in the latter. Though this does not happen for the simple case of the occurrence of a FGGPL R object-letter within a FGGPL R term, it is worth giving as of now a short explanation of the way it has to be understood in FGGPL R and FGGL2 R .

The problem depends on the role plaid in these systems by the function ξ. As we have said above (cf. p. 15), this function is intended to render Frege's functionξ. There is, however, among others, a crucial difference between these two functions, or better between the way the horizontal stroke ' -' works in FGGBS and the way the upper bar ' --' works both in FGGPL R and in FGGL2 R . Whereas any occurrence on the upper bar ' --' is perfectly distinguishable as such, so as to allow one to precisely count these occurrences in any relevant expression (so to say, for example, that 'Γ' differs from 'Γ' and 'Γ' from 'Γ', since the first involves one occurrence of ' --', the second two such occurrences, and the third three), Frege's rule of "fusion of horizontals", makes a single occurrence of the stroke ' -' indistinguishable from as many such occurrences as one wants. For example, in the single expression ' ∆ Γ ', one can find arbitrarily many occurrences of this stroke both before the vertical stoke and after it, both above and below. It follows that this expression can be rendered, in our notation, in an infinity of different ways, for example, by ' [START_REF] Landini | Frege's Notations: What They Are and How They Mean[END_REF] . Hence, whereas both in FGGPL R and to FGGL2 R , the passage from θ to θ (where θ is any term or object-letter) depends on the application of an appropriate rule, in FGGBS no such rule is needed, since no passage analogous to this is detectable. This difference is a price we have to pay, in order to transform Frege's multi-level notation in a mono-level notation.

Γ ⇒ ∆', 'Γ ⇒ ∆', 'Γ ⇒ ∆' Γ ⇒ ∆, 'Γ ⇒ ∆', 'Γ ⇒ ∆', 'Γ ⇒ ∆' 'Γ ⇒ ∆', etc.
When this is coupled with our making, in accordance with Frege's habit, the symbol ' --' play the role of parentheses, then the notion of occurrence of a string of symbols within another string of symbols becomes, with respect to our notation, much less immediately and simply understandable than it is with respect both to Frege's notation and to that currently used in modern systems of logic.

Precisely fixing the notion of occurrence of a string of symbols within another string of symbols with respect to our notation would require a tiresome development. Instead we give an informal explanation limited to the problematic cases we shall run into. Concerning FGGPL R , these cases only pertain to the (values of the) functions ¬ξ and ζ ⇒ ζ (we shall come back in § 4.3 to other problematical cases concerning FGGL2 R ): if θ and τ are two FGGPL R terms32 , then, whereas θ and τ occur within θ ⇒ τ , and θ occurs within ¬θ, neither θ nor τ occur within θ ⇒ τ , and θ does not occur within ¬θ.

This being said, let us return to our formal presentation, and further extend our formal language, by adding the symbol ' ' to L T [FGGPL R ] , so as to get the language

L PS [FGGPL R ] = L T [FGGPL R ] ∪
. This language is used to form FGGPL R particular statements. This hinges on the following stipulations:

St PS [FGGPL R ] .i If θ is a FGGPL R term, then θ is a FGGPL R particular statement. St PS [FGGPL R ]
.ii Nothing else is a FGGPL R particular statement.

If θ is a FGGPL R particular statement, let us say that θ is its FGGPL R term. Let us then say that:

St As.PS [FGGPL R ]
A FGGPL R particular statement asserts that the truth-value named by its FGGPL R term is T;

St Hld.PS [FGGPL R ]
A FGGPL R particular statement holds if its FGGPL R term is a name of T; and it does not hold if its FGGPL R term is a name of F.

Stipulation St Is.T [FGGPL R ]
naturally suggests the following one for FGGPL R particular statements:

St Is.PS [FGGPL R ]
A FGGPL R particular statement is an instance of a FGGPL R particular statement if and only if the FGGPL R term of the former is an instance of the FGGPL R term of the latter [START_REF] Panza | From Lagrange to Frege: Functions and expressions[END_REF] .

FGGPL R particular statements can, moreover, follow from each other. This depends on an inductive stipulation, whose base is given by the next eight rules, where, supposing that θ, ϑ, τ are FGGPL R particular statements, we write ' θ -τ ' and '

θ ; ϑ ----τ ' as graphical shorthand for ' τ immediately follows from θ' and ' τ immediately follows from θ and ϑ', respectively:

Rl PS [FGGPL R ]
.i If θ and τ are two FGGPL R particular statements and the latter is an instance of the former, then: θ -τ This is a substitution rule within FGGPL R particular statements, and renders Frege's tacit replacement rules for upper-case Greek letters [START_REF] Potter | Reason's Nearest Kin. Philosophies of Arithmetic from Kant to Carnap[END_REF] .

Rl PS [FGGPL R ] .ii If θ, [θ],
i = 0, for 'κ i,1 ⇒ ' if n i = 1, for 'κ i,1 ⇒ κ i,2 ⇒ ' if n i = 2, &c.
, where the symbol ' ' is intended to mean that the upper strokes over it extend to the right over the following ones, up to the end of the statement), and '⇒ -→ κ 3 ' stands for '⇒ κ 3,1 ⇒ κ 3,2 ⇒ ...

. . . ⇒ κ 3,n 3 ', then:

-→ κ 1 ⇒ θ 1 ⇒ -→ κ 2 ⇒ θ 2 ⇒ -→ κ 3 ⇒ τ --------------- -→ κ 1 ⇒ θ 2 ⇒ -→ κ 2 ⇒ θ 1 ⇒ -→ κ 3 ⇒ τ .
This is a rule of transformation of FGGPL R particular statements, and renders Frege's rule of "permutation of subcomponents" ( [18], § § I.12 and I.48.

-→ κ 1 ⇒ θ £ 1 ⇒ -→ κ 2 ⇒ θ £ 2 -------------→ κ 1 ⇒ θ ¡ 2 ⇒ -→ κ 2 ⇒ θ ¡ 1 .
This is another rule of transformation of FGGPL R particular statements, and renders Frege's rule of "contraposition" ( [18], § § I. 15 ] .iii, while ' -→ κ 3 ⇒' behaves like ' -→ κ 1 ⇒' in this same rule, then: ---------------

-→ κ 1 ⇒ θ ⇒ -→ κ 2 ⇒ θ ⇒ -→ κ 3 ⇒ τ -
→ κ 1 ⇒ θ ⇒ -→ κ 2 ⇒ -→ κ 3 ⇒ τ .
This is a new rule of transformation of FGGPL R particular statements, and renders Frege's rule of "fusion of equal subcomponents" ( [18], § § I.15 and I.48.4; [22], pp. 29 1 and 61 1 ). [START_REF] Sandu | Ramsey and the notion of arbitrary function[END_REF] The rule of fusion of horizontals is embodied in Frege's notation, with the result of blurring the twofold role it plays in FGGBS, as a rule for the formation of terms and as a deductive rule. This rule is however both appealed to during the explanation of the function-names ' -ξ', ' ξ' and ' ξ ζ ' ( [18], § § 6, 12), and listed among the deductive rules ( [18], § I.48.1).

Rl ] . iii, while ' -→ κ 2 ⇒' behaves like ' -→ κ 1 ⇒' in this same rule, then:

θ ; -→ κ 1 ⇒ θ ⇒ -→ κ 2 ⇒ τ --------------→ κ 1 ⇒ -→ κ 2 ⇒ τ .
This is a generalisation of modus ponens, and renders Frege's "first mode of inference" ( [18], Inhaltsverzeichniss of vol. I, p. XXVII, and § § I. 14 --------------------

-→ κ 1 ⇒ θ ⇒ -→ κ 2 ⇒ τ ; -→ κ 3 ⇒ τ ⇒ -→ κ 4 ⇒ ϑ -
→ κ 1 ⇒ θ ⇒ -→ κ 2 ⇒ -→ κ 3 ⇒ -→ κ 4 ⇒ ϑ .
This is another generalisation of modus ponens, and renders Frege's "second mode of inference" ( [18], Inhaltsverzeichniss of vol. I, p. XXVII, and § § I.15 and I.48.7; [22], pp. XXVII 1 , 26-27 1 and 62 1 ). ---------------------

Rl PS [FGGPL R ] . viii If κ i,1 , κ i,2 , . . . , κ i,n i (where i = 1, 2, 3, 4 and n i is an arbitrary natural number), θ, τ are FGGPL R terms, ' -→ κ 1 ⇒', ' -→ κ 3 ⇒', ' -→ κ 2 ⇒', and ' -→ κ 4 ⇒' behave like ' -→ κ 1 ⇒' in rule Rl PS [FGGPL R ] .iii, while '⇒ -→ κ 2 ' and '⇒ -→ κ 4 ' behave like '⇒ -→ κ 3 ' in this same rule, then: -→ κ 1 ⇒ ¬θ ⇒ -→ κ 2 ⇒ τ ; -→ κ 3 ⇒ θ ⇒ -→ κ 4 ⇒ τ -
→ κ 1 ⇒ -→ κ 2 ⇒ -→ κ 3 ⇒ -→ κ 4 ⇒ τ .
This renders Frege's "third mode of inference" ( [18], Inhaltsverzeichniss of vol. I, p. XXVII, and § § I.16 and I.48.8; [22], pp. XXVII 1 , 30-31 1 and 62 1 ). In fact, it is a consequence of rules Rl PS [FGGPL R ] .ii-v, vii, as showed by Frege himself [START_REF] Simons | Frege's theory of real numbers[END_REF] . For the sake of the simplicity of his further deductions, he nevertheless considered appropriate to state it as an independent rule.

It is easy to see that all these rules are sound: they are such that their outputs hold if their inputs do. This is what justifies these rules [START_REF] Snyder | Frege on the real numbers[END_REF] , and makes them a suitable basis for the inductive stipulation fixing the relation of following from, as defined on FGGPL R particular statements: ] . ii is embodied in his notation: cf. footnote 36. [START_REF] Snyder | Frege on the real numbers[END_REF] As it is made clear by the passage quoted in footnote 21, Frege was perfectly aware that he could have reduced the number of his deductive rules. It seems that he felt licensed to multiply them, in the interest of the simplicity of his deductions (without running any risk of error), just insofar as their soundness is manifest.

St Flw.PS [FGGPL R ] .i

General Statements or Well-Formed Formulas

Preliminary Explanations

We can now move on to FGGPL R general statements. These are just the same as FGGPL R particular statements, except for the fact that they include lower-case Roman letters instead of Greek upper-case ones. According to our foregoing stipulation, the latter letters, namely FGGPL R object-letters, are object-names referring to unspecified objects. The former letters are intended to merely indicate objects (cf. p. 7 and § 2.5, above). Their use is submitted to the stipulation that a FGGPL R general statement asserts that the truth-value named by the FGGPL R term of a FGGPL R particular statement obtained from such a FGGPL R general statement, by replacing any occurrence of each such letter with an occurrence of the same FGGPL R object-letter whatsoever, is T, irrespectively of the objects that the relevant object-letters refer to (which entails that the truth-value named by any instance of such a term is also T). This is the same as stipulating that a FGGPL R general statement asserts that a FGGPL R particular statement obtained from it in this way holds irrespectively of the objects that the object-letters occurring within it refer to (which entails that this is also the case for any instance of this particular statement). If this happens, it is, then, natural to say that such a FGGPL R general statement holds, in turn, and that it does not hold, if this is not what happens, which renders bivalence with respect to FGGPL R general statements. Take two simple examples: the FGGPL R general statements ' a ⇒ b' and ' a ⇒ b ⇒ a' respectively assert that the FGGPL R particular statements ' ∆ ⇒ Γ' and ' ∆ ⇒ Γ ⇒ ∆' hold irrespectively of the objects that '∆' and 'Γ' refer to; hence, the latter of these FGGPL R general statements holds, whereas the former does not.

The crucial difference between FGGPL R particular and general statements that results from these stipulations becomes clear by observing that what a FGGPL R object-letter is intended to name is a particular object, though an unspecified one. Hence a FGGPL R particular statement is intended to assert something about a finite number of particular, though unspecified, objects, not about an arbitrary system of arbitrarily many objects. A FGGPL R general statement is, instead, just intended to assert that any system of an appropriate number of objects satisfies a certain condition. For example, whereas the FGGPL R particular statement ' ∆ ⇒ Γ' asserts of the unspecified objects ∆ and Γ that it is not the case that the former is T and the latter is not T-which might certainly happen, if these objects are suitably specified-, the FGGPL R general statement ' a ⇒ b' asserts that the FGGPL R particular statement ' ∆ ⇒ Γ' holds irrespectively of the objects that '∆' and 'Γ' refer to, i.e. that, whatever these objects might be, it is not the case that the former is T and the latter is not T-which certainly does not happen.

Insofar as this stipulation is the only one we make about the meaning to be ascribed to lower-case Roman letters within FGGPL R , it follows that these letters are only licensed to enter FGGPL R statements, namely general such statements, but not FGGPL R terms, or any other sort of well-formed strings of symbols that one might form within FGGPL R . This makes any FGGPL R term a particular term: a term referring to a particular object, though unspecified, which agrees with Frege's views expounded in § 2.5 while speaking of free variables (cf., in particular, the passage quoted in footnote 23).

These views are in line with Frege's admission of no propositional particular statement within FGGBS, that is, with the idea that propositional particular statements have their place only within the expository language of this system, whereas the system itself only includes general such statements. Hence, properly speaking, FGGPL R particular statements render no well-formed formula of FGGBS, and it is, then, natural to take FGGPL R general statements to be the only well-formed formulas of FGGPL R , while considering FGGPL R particular statements as auxiliary statements, and L PS [FGGPL R ] , as well as L T [FGGPL R ] and L AT [FGGPL R ] , as auxiliary preliminary languages.

Formal Treatment

All this being said in the guise of preliminary explanations, let us consider the matter formally.

Let L GS [FGGPL R ] be the language a, b, c, d, . . . , --, ¬ --, --⇒ --, obtained from L PS [FGGPL R ] by replacing its object-letters with the Roman letters 'a', 'b', 'c', 'd', . . . , called 'FGGPL R general letters for objects', also with arity 0. Here the ellipses are intended to stay for the same letters 'a', 'b', 'c ', 'd' endowed with appropriate indexes, so as to form a potentially infinite collection of symbols, all having arity 0. This language is used to form FGGPL R general statements (which explains our using the acronym 'GS' in 'L GS [FGGPL R ] '), according to the following stipulations: .i -so that the latter results from the former according to the inverse replacements-, then the former is said to correspond to the latter and vice versa. For example, ' a ⇒ b' is said to correspond to ' Γ ⇒ ∆', and vice versa. If each of several FGGPL R general statements corresponds to one of as many FGGPL R particular statements, according to the same replacements of FGGPL R object-letters with FGGPL R general letters for objects, the former statements are said to uniformly correspond to the latter ones, and vice versa. For example, ' a ⇒ b' and ' a ⇒ b ⇒ a' are said to uniformly correspond to ' Γ ⇒ ∆' and ' Γ ⇒ ∆ ⇒ Γ', and vice versa.

St GS [FGGPL R ] .i
Let us also stipulate that 40 :

St As.GS [FGGPL R ]
A FGGPL R general statement asserts that a FGGPL R particular statement which corresponds to it holds whatsoever objects might be named by the FGGPL R object-letters occurring within it;

St Hld.GS [FGGPL R ]
A FGGPL R general statement holds if and only if a FGGPL R particular statement which corresponds to it holds irrespectively of the objects that the object-letters occurring within it refer to.

Axiom and Theorems

According to the meaning assigned to the functions ξ and ζ ⇒ ξ, from stipulation St Hld.GS

[FGGPL R ] it follows that the FGGPL R general statement Ax [FGGPL R ] .I ' a ⇒ b ⇒ a'
40 Insofar as FGGPLR object-letters refer to unspecified objects, a FGGPLR particular statement θ which correspond to a certain FGGPLR general statement |θ| holds whatsoever objects might be named by the FGGPLR object-letters occurring within it if and only if this is also the case of any other FGGPLR particular statement θ which correspond to |θ|, since the conditions under which the statement ' Γ ⇒ ¬∆ ⇒ Γ' holds are, for example, just the same at those under which the statements ' Γ ⇒ ¬Θ ⇒ Γ' or ' Λ ⇒ ¬Ξ ⇒ Λ' hold. Hence, the indefinite article 'a' in the following stipulations could be replaced by the adjective 'every' without any alteration of the content of these stipulations.

holds. Let us take it to be the only axiom of FGGPL R . This renders Frege's Basic Law I ( [18], § § I.18, 47). Let also stipulate that: This last stipulation can be equivalently restated in a more direct way. To this purpose, call 'FGGPL R Roman object-marker', or, merely 'FGGPL R object-marker', for short, that which results from a FGGPL R term by replacing each distinct FGGPL R object-letter in it with a distinct FGGPL R general letter for objects ( [18], § § I.17 and I.26; [22], pp. 33 1 and 44 1 ). This is equivalent to calling in this same way that which results from R general statements by omitting the symbol ' ' in front of them. This suggests restating rules Rl PS [FGGPL R ] . i -viii with reference to FGGPL R general statements rather than to FGGPL R particular statements: it is enough, for this, to rewrite these rules by taking the variables involved in them to range over FGGPL R object-markers rather than over FGGPL R terms. Let Rl

St Flw.GS [FGGPL R ] If |τ |, |θ i | (i =
[FGGPL R ] . i -viii ). St Flw.GS * [FGGPL R ] . ii If τ , θ i (i = 1, 2, . . . , n), ϑ i (i =

Completeness

Insofar as Ax [FGGPL R ] .I holds, and the deductive rulesRl GS [FGGPL R ] . i-viii are all sound, then any theorem of FGGPL R holds, and FGGPL R is, itself, sound, and, then, consistent. One can also prove that FGGPLR is deductively equivalent to a complete modern system of classical propositional logic, and is, then, complete, in turn.

Consider, for example, the system M, which has been proved to be sound and complete ([32], § I.4), whose axioms are the following (in modern notation)

Ax [M] .i A ⇒ (B ⇒ A) Ax [M] .ii A ⇒ (B ⇒ C) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)) Ax [M] .iii (¬B ⇒ ¬A) ⇒ ((¬B ⇒ A) ⇒ B)
, where 'A', 'B', 'C' are meta-variables ranging on the well-formed formulas of M, and whose single deductive rule is modus ponens.

To render these axioms within FGGPL R , it is enough to replace in them the meta-variables 'A', 'B', 'C' with 'a', 'b', 'c', and the parentheses with ' --', while adding the symbol ' ' in front of each of them. This results in the three following FGGPL R general statements:

GS [Ax [M] ] [FGGPL R ] .i a ⇒ b ⇒ a GS [Ax [M] ] [FGGPL R ] .ii a ⇒ b ⇒ c ⇒ a ⇒ b ⇒ a ⇒ c GS [Ax [M] ] [FGGPL R ] .iii ¬b ⇒ ¬a ⇒ ¬b ⇒ a ⇒ b .
The replacement of meta-variables 'A', 'B', 'C' with 'a', 'b', 'c' is to go together with the adoption of an appropriate deductive rule allowing replacements within FGGPL R general statements. Rule Rl GS [FGGPL R ] .i is perfectly appropriate for this purpose. Once this rule is admitted, the rule of modus ponens for M can be replaced with a particular case of rule Rl GS [FGGPL R ] . vi (where ' -→ κ 1 ⇒', '⇒ -→ κ 2 ', and ' -→ κ 2 ⇒' stand for nothing, that is, n 1 = n 2 = 0, and θ and τ are respectively taken to be a and b). Insofar as GS ] .iii within this system, that is, to show that these statements follow from Ax

[Ax [M] ] [FGGPL R ] .i coincides with Ax [FGGPL R ] .I, to prove that M is interpretable in FGGPL R , it is, then, enough to prove GS [Ax [M] ] [FGGPL R ] .ii and GS [Ax [M] ] [FGGPL R
[FGGPL R ] .I (according to St Flw.GS * [FGGPL R ] .i-iii
). This is enough to prove that FGGPL R is complete. Insofar as both M and FGGPL R are sound, this is also enough for proving that these systems are deductively equivalent, as said above.

Here is how this can be done:

1. a ⇒ b ⇒ c ⇒ a ⇒ b ⇒ c ⇒ a ⇒ b ⇒ c Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 2. a ⇒ b ⇒ c ⇒ a ⇒ b ⇒ c Rl GS [FGGPL R ] . v, ii on 1 3. a ⇒ b ⇒ a ⇒ b ⇒ a ⇒ b Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 4. a ⇒ b ⇒ a ⇒ b Rl GS [FGGPL R ] . v, ii on 3 5. a ⇒ b ⇒ a ⇒ a ⇒ b ⇒ c ⇒ a ⇒ c Rl GS [FGGPL R ] . vii, ii on 2,4 6. a ⇒ b ⇒ a ⇒ a ⇒ b ⇒ c ⇒ c Rl GS [FGGPL R ] . v, ii on 5 GS [Ax [M] ] [FGGPL R ] .ii a ⇒ b ⇒ c ⇒ a ⇒ b ⇒ a ⇒ c Rl GS [FGGPL R ] . iii, iii on 6 1. ¬b ⇒ a ⇒ ¬b ⇒ a ⇒ ¬b ⇒ a Rl GS [FGGPL R ] .i on Ax [FGGPL R ] .I 2. ¬b ⇒ a ⇒ ¬b ⇒ a Rl GS [FGGPL R ] .v, ii on 1 3. ¬b ⇒ a ⇒ ¬a ⇒ b Rl GS [FGGPL R ] . iv on 2 4. ¬b ⇒ ¬a ⇒ ¬b ⇒ a ⇒ ¬b ⇒ ¬a Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 5. ¬b ⇒ ¬a ⇒ ¬b ⇒ a ⇒ a ⇒ b Rl GS [FGGPL R ] . iv on 4 6. a ⇒ ¬b ⇒ a Rl GS [FGGPL R ] .i on Ax [FGGPL R ] .I 7. a ⇒ ¬b ⇒ ¬a ⇒ a ⇒ b Rl GS [FGGPL R ] . vii,ii on 5,6 8. ¬b ⇒ ¬a ⇒ a ⇒ b Rl GS [FGGPL R ] .v, ii, iii on 7 9. ¬b ⇒ a ⇒ ¬b ⇒ ¬a ⇒ b Rl GS [FGGPL R ] .viii on 3,8 GS [Ax [M] ] [FGGPL R ] .iii ¬b ⇒ ¬a ⇒ ¬b ⇒ a ⇒ b Rl GS [FGGPL R .
ii, iii on 9

Identity

It is not clear whether Frege was aware that, together with the deductive rules we have rendered with Rl GS [FGGPL R ] . i-viii, his Basic Law I is enough to deduce all the statements of the language of FGGBS only involving the functionsξ, ξ and ξ ζ , which holds according to the definitions of these functions (which is what we have rendered by saying that FGGPL R is complete). What is certain is that, after having proved, in § I.49, a few very simple propositional theorems from Basic Law I alone, he turned to his other Basic Laws, and appealed to some of them, namely Basic Laws IIb, III and IV, to prove, in § I.51, other propositional theorems, whose proof can, in fact, dispense from these laws. This is the case, for example, of theorems IIIg and IVb, which could be respectively rendered in our notation thus: ¬a = ¬a and a = ¬¬a.

Taken as such, these are not theorems of FGGPL R , since they are not well-formed formulas of this system, insofar as they involve the identity function that is not part of it. Still, Frege's definition of this function ( [18], § I.7) immediately suggests different ways of transcribing these theorems within L GS [FGGPL R ] . Using our notation, this definition can be rendered as follows:

-ξ = ζ : O 2 → {T, F} be such that ∆ = Γ is T if ∆ is Γ F if ∆ is not Γ .
By (indirectly) composing this function with ξ (and appropriately extending our suppositions about our knowing the truth conditions of the statements of the natural language to be used for this purpose), we get the new function

-ξ = ζ : O 2 → {T, F} such that Γ = ∆ is T if Γ is T and ∆ is T or Γ is not T and ∆ is not T F if Γ is T and ∆ is not T or Γ is not T and ∆ is T , which is clearly such that -ξ = ζ : O 2 → {T, F} is such that Γ = ∆ is T if Γ is T and ∆ is T or Γ is F and ∆ is F F if Γ is T and ∆ is F or Γ is F and ∆ is T .
It is manifest that the function ξ = ζ, easily obtained from ξ = ζ, is perfectly suitable to play, within FGGPL R , the same role as that which the connective of double implication plays in modern propositional systems. This, together with the remark that Frege himself got his functionξ = -ζ by indirectly composing ξ = ζ withξ ( [18], § I.18), suggest innocently adding to L GS [FGGPL R ] the symbol ' --⇔ --', with arity 2, by explicitly defining it through the following stipulation:

St GS⇔ [FGGPL R ]
If θ and τ are FGGPL R terms, then 'θ ⇔ τ ' stands for '¬θ ⇒ τ ⇒ ¬τ ⇒ θ'.

Frege's theorems IIIg and IVb can, then, be rendered within FGGPL R as follows:

¬a ⇔ ¬a and a ⇔ ¬¬a.

If one would prefer avoiding adding the symbol '

--⇔ --' to L GS [FGGPL R ]
, these same theorems could, on the other hand, more prolixly be rendered thus: ¬¬a ⇒ ¬a ⇒ ¬¬a ⇒ a and ¬a ⇒ ¬¬a ⇒ ¬¬¬a ⇒ a.

The completeness of FGGPL R ensures that all these are theorems of this system, and it is, indeed, quite easy to prove them. This is, for example, a simple proof of ' ¬¬a ⇒ a' ( [32], lemma 1.11(a); cf. ibid., lemma 1.11(b), for a proof of ' a ⇒ ¬¬a' 43 ):

1. ¬a ⇒ ¬¬a ⇒ ¬a ⇒ ¬a ⇒ a Rl GS [FGGPL R ] .i on GS [Ax [M] ] [FGGPL R ] .iii 2. ¬a ⇒ ¬a ⇒ ¬a Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 3. ¬a ⇒ ¬a Rl GS [FGGPL R ] .v,ii on 2 4. ¬a ⇒ ¬¬a ⇒ a Rl GS [FGGPL R ] . vi on 1, 3 5. ¬a ⇒ ¬¬a ⇒ a Rl GS [FGGPL R ] . ii on 4 6. ¬¬a ⇒ ¬a ⇒ ¬¬a Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 7. ¬¬a ⇒ a Rl GS [FGGPL R ]
. vii, ii on 5, 6

One could, then, wonder why Frege used Basic Laws III and IV to prove his theorems IIIg and IVb and some other propositional theorems (for which the same argument can be repeated, mutatis mutandis). It is quite implausible that he did not see the possibility of deducing appropriate versions of them from Basic Law 43 Once ' ¬¬a ⇒ a' and ' a ⇒ ¬¬a' have been proved, in order to prove ' ¬a ⇒ ¬¬a ⇒ ¬¬¬a ⇒ a', it is enough to apply to them the following derivation-schema, where θ and τ are FGGPLR terms:

1. θ 2. τ 3. θ Rl GS [FGGPL R ] . ii on 1 4. τ Rl GS [FGGPL R ] . ii on 2 5. θ ⇒ ¬τ ⇒ θ ⇒ ¬τ ⇒ θ ⇒ ¬τ Rl GS [FGGPL R ] . i on Ax [FGGPL R ] .I 6. θ ⇒ ¬τ ⇒ θ ⇒ ¬τ Rl GS [FGGPL R ] . v, ii on 5 7. τ ⇒ θ ⇒ ¬θ ⇒ ¬τ Rl GS [FGGPL R ] . iv on 6 8. θ ⇒ ¬θ ⇒ ¬τ Rl GS [FGGPL R ] . vi, ii on 4,7 9. ¬θ ⇒ ¬τ Rl GS [FGGPL R ]
. vi, ii on 3,8

I alone.

A more convincing answer is that he was unconcerned with separating the propositional fragment of his system from the rest of it, as we have argued for in § § 1 and 2.4. This lack of concern is perfectly evident from his simple deduction of theorems IVc and IV d ( [18], § I.51), which could be rendered in our notation as follows:

f ¬¬a ⇒ f (a) and f (a) ⇒ f ¬¬a ,
where 'f ' is used to indicate first-level functions just as FGGPL R general letters for objects indicate objects.

To this purpose, Frege did not only appeal to theorem IVb, but also to a consequence of Basic Law III (namely theorem IIIa: ibid., § I.50), drawn from it through an appeal to Basic Law IIb. A simple particularisation of these theorems, immediately provides the two propositional principles of elimination and introduction of double negation, mentioned just above. But Frege did not state any new theorem expressing these principles, namely, neither ' a a ', nor ' a a ', which merely involve, nonetheless, the three functionsξ, ξ and ξ ζ . Clearly, he was not only unconcerned with deducing these theorems from Basic Law I alone; he was also unconcerned with stating these theorems as such, after having stated the more general theorems IVc and IVd.

It seems to us that this is strong evidence supporting our claim that Frege was unconcerned with separating the propositional fragment of his system from the rest of it. Still, the way he proved his theorems IIIg and IVb, as well as the other propositional theorems involving the functionξ = -ζ, is also evidence for another, related claim, namely that Frege considered essential to have a unique identity function, both applying to objects in general, as it is the case for our identity function, and to truth-values, in particular, so as to make it able to play the role that we assign to the double implication connector. In other terms, for him, there was no room for something assimilable to this connector as such: identity, as a total fist-level function, was rather the crucial tool to be used, and possibly applied to truth-values. This is perfectly in line both with his universalist conception of logic, and with his conception of its propositional fragment as a theory of terms referring to truth-values (that is, in the very end, with his conception of truth, and his view on ontology, i.e. with the idea that the world is made up of objects, without any distinction of status or type). But it is also a deep reason that plausibly pushed him to consider that a separation of propositional logic from other departments of logic would have been inappropriate. His being unconcerned with separating the propositional fragment of his system from the rest of it was then deeply rooted in his way on conceiving logic, in general, and was not merely a consequence of carelessness.

Still, if, despite all of that, we would like to integrate, the identity function within FGGPL R , we could certainly do it, by adding to the languages L T

[FGGPL] , L PS [FGGPL R ]
, and L GS [FGGPL R ] the symbol ' --= --', with arity 2, agreeing with the previous definition of the functions ξ = ζ and ξ = ζ, so as to get, respectively, the new languages L T=

[FGGPL R ] , L PS= [FGGPL R ]
, and

L GS= [FGGPL R ] .
To this purpose, we should also amend stipulation St T

[FGGPL R ] as follows:

St T= [FGGPL R ]
. i If θ and τ are FGGPL R object-letters, atomic terms, or terms, then θ, ¬θ, θ ⇒ τ , and θ = τ are FGGPL R terms;

St T= [FGGPL R ] . ii Nothing else is a FGGPL R term.
This would allow to render Basic Law IV with a FGGPL R general statement, to be added to Ax [FGGPL R ] .I as a new axiom of FGGPL R :

Ax [FGGPL R ] .IV ¬a = ¬b ⇒ a = b .
It is clear both that this statement holds, and that it cannot be deduced in FGGPL R from Ax [FGGPL R ] .I, since none of the rules Rl GS [FGGPL R ] . i-viii allow one to introduce the symbol '='. It is also clear that, once this axiom is admitted, these last rules allow to deduce other statements from it, either alone or together with Ax [FGGPL R ] .I, all including this symbol, and, then, all non-deductible from this last axiom alone. In a sense, adding Ax .IV-would, then, result in properly extending this system, without going beyond the limit of a propositional system. Still, this is not in contradiction with the previous result to the effect of which FGGPL R is complete. Since for each new theorem that would be obtained this way, there would be another theorem of FGGPL R , deducible from Ax [FGGPL R ] .I alone and not involving the function ξ = ζ, which would correspond to it under the replacement of any FGGPL R object-marker of the form 'θ = τ ' with a corresponding FGGPL R object-marker of the form '¬θ ⇒ τ ⇒ ¬τ ⇒ θ'. One could then say that none of the former theorems would be genuinely new44 . 4 Frege's Second-Order System Reconstructed 4.1 From FGGPL R to FGGL2 R Though our presentation of FGGPL R as an autonomous system collides with Frege's avoiding a clear separation of the propositional fragment of FGGBS from the other parts of this system, we partially reflect Frege's attitude on this matter by rooting FGGL2 R in FGGPL R . This is made particularly clear by our incorporating FGGPL R basic functions into FGGL2 R , by also considering the function ξ = ζ with its two facets, respectively appearing when its arguments are truth-values or objects in general. This is not the same, however, as merely coming to FGGL2 R by extending FGGPL R . The reason is that the generation of terms in the former system proceeds in a quite different way than in the latter.

As a matter of fact, Frege did not rigourously expose the way in which terms are generated in FGGBS, but rather used natural language to suggest the way in which they can be obtained from each other.

If we limit ourselves to the propositional fragment of this system, things are clear enough to suggest the simple clauses we have adopted in FGGPL R . Still, stating these clauses essentially depends on appealing to FGGPL R object-letters, which, as we have seen above, do not occur within the language L GS [FGGPL R ] , which is used to state FGGPL R well-formed formulas. Though the use of these letters is confined neither to the informal presentation of the basic ideas the system is based on, nor to the definition of its basic functions (which, from a modern stand-point, could be considered as a purely semantic matter), but is also indispensable for fixing its syntax, they are, then, so to say, only provisionally called into play. The reason for this is that FGGPL R is intended to reflect (among other things) Frege's conception of well-formed formulas of FGGBS as universal in nature (which is, by the way, a natural outcome of his universalist conception of logic), and to adhere, then, to his requirement that no atomic object-name be allowed to occur within these formulas. This requirement entails that the only symbols with arity 0 included in the propositional fragment of FGGBS that are allowed to occur within these formulas are Roman letters for objects (which correspond to FGGPL R general letters for objects). When this is coupled with the fact that no term can be formed by using only these letters together with the other propositional ingredients of FGGBS, this results in the consequence that the propositional well-formed formulas of FGGBS include no terms (which fits, indeed, with the way these formulas are conceived, namely as statements that are general insofar as they assert that other statements, namely appropriate classes of particular ones, hold). This is why the language L GS [FGGPL R ] is shaped so as to not only include no terms among its atomic symbols, but also to render impossible the generation of terms within it. Both provisional atomic terms, and rules to generate other terms from them are, then, needed, and this is what FGGPL R object-letters are required for.

When one proceeds beyond the restricted limits of the propositional fragment of FGGBS and passes to its second-order fragment, things change quite crucially, since it is no more true that no term can be formed by using only the ingredients of this last fragment of FGGBS that are allowed to enter its well-formed formulas. To anticipate, let us consider two simple examples: ' a a' ' f a f (a)' are term of FGGBS and are perfectly allowed to enter well-formed formulas of this system. In the second-order fragment of FGGBS, there are, then, the resources to generate terms by involving neither atomic object-names nor analogous syntactical resources to be used to designate unspecified functions. It is then natural to shape FGGL2 R so as to avoid having recourse both to FGGPL R object-letters and to analogous function-letters-that is, letters to be used to form indeterminate function-names-, in order to generate terms 45 , and, then, using the upper-case Greek letters 'Γ', '∆', 'Θ', 'Λ', 'Ξ', 'Π', 'Σ', together with other such letters, like 'Φ', 'Ψ', 'Ω' and 'Υ'-used, indeed, to form indeterminate function-names-only informally, and in the definition of the basic functions to be added to those involved in FGGPL R . This requires, however, to emphasize a feature of Frege's formal language that is somehow kept out of sight in the way terms are generated in FGGPL R . We refer to the impossibility, in this language, of getting a term by direct composition of two other terms: to get a term by composing two other terms, one is to pass through a desaturation of one of the latter, and, then, through a function-name. For example, the two terms 'Γ ⇒ ∆' and '¬∆' being given to get the composed term 'Γ ⇒ ¬∆', one has to desaturate the former, so as to get the function-name 'Γ ⇒ ξ', then to saturate 46 this function-name with the latter term 47 .

It follows that the process of generation of terms requires a continuous coming and going from object-to function-names and vice versa. The propositional fragment of FGGBS can be rendered so as to leave this coming and going somehow implicit, as it happens in FGGPL R . But, when one passes to the second-order fragment, and one wants to render it by avoiding to assign any formal role to FGGPL R object-letters and to analogous function-letters, this coming and going has to be made explicit, and this requires assigning a 45 Note that if FGGPLR had been not presented as a separate system, but rather intended as a (non-autonomous) fragment of FGGL2R, we could have avoided the recourse to FGGPLR object-letters also for generating FGGPLR terms. It would have been enough, for this, to admit appropriate rules of substitution allowing replacing FGGL2R terms with the Roman letters entering

L GS [FGGPL R ]
. This would not have been unfaithful to Frege's original system, since the only objects other than the truth-values that play an effective role in it are value-ranges (at least in the case where these do not reduce, in turn, to truth-values). Moreover, § § I.26-28 of the Grundgesetze, taken together with Frege's conception of functions, seem to suggest that his dealing with the propositional functionsξ, ξ, ξ ζ and with the corresponding deductive rules alone-that is, his operating without any (apparent) consideration of non-propositional ingredients of FGGBS-was only intended for clarity's sake. This is another hint to understand the reasons underlying Frege's avoiding a clear separation of the propositional fragment of FGGBS from his whole system. 46 Here and below we feel free to use the verb 'to saturate' and its cognates in order to speak about the formation of terms or object-markers, which is something Frege did not do with the corresponding German verb 'sättigen' and its cognates, and we associate this use with that of the verb 'to desaturate', which has no German correspondent in the language Frege used in the Grundgesetze. In similar circumstances, for example in § I.26, Frege respectively used, instead, the verbs 'to fill [ausfüllen]' and 'to remove [ausschliessen]', or rather the verb 'to replace [ersetzen]'. Still the literal meaning of the first two of these verbs could be misleading here, since the procedures they are intended to designate are, in fact, much more complex and subtle than this meaning might suggest (as we hope to make clear by the definition of the procedures for forming terms, and object-and function-markers we shall offer in § § 4.3 and 4.4.2, below), and we reserve the third for using it in a more precise way. 47 This makes quite clear what Frege was meaning by claiming that "functions with two arguments are just as fundamentally distinct from functions with one argument as the latter are from objects[. . . ][, f]or, while the latter are fully saturated, functions with two arguments are less saturated than those with one argument, which are already unsaturated "( [18], § I.21; [22], p. 371).

formal role to other symbols that will not eventually appear in the well-formed formulas of the resulting system. These symbols include those that are used within function-names to hold places open, namely the lower-case Greek letters 'ξ', 'ζ', 'ϕ', and other symbols also used in some function-names for another purpose that will be made clear below, namely the letters 'β' and 'γ' 48 . It follows that the language of FGGL2 R has to have recourse to provisional symbols that are not eventually allowed to enter its well-formed formulas, though these are neither FGGPL R object-letters nor analogous function-letters.

This apart, controlling the coming and going from object-to function-names and vice versa is a delicate task, since this process is manifestly open to a risk of circularity. Without the appropriate provisions, it could, indeed, require fixing the way function-names are generated in order to fix the way that terms are, and vice versa. And the task becomes even more delicate if the relevant function-names also include names of higher-level functions, as it is necessarily the case for the second-order fragment of FGGBS, and for any rendering of it. Frege didn't properly show the road toward the solution of the problem, by rather leaving to a skilful use of natural language, making recourse to the non-better defined notions of a name (either an object-or a function-name) "forming a part" of another name (either an object or a function-one, too), and of "removing" the former name from the latter ( [18], § I.26; [22], pp. 43 1 -44 1 ), the task of informally describing it, or better of giving a sufficient insight of it. Still, this provides hints for rendering his ideas through appropriate formal clauses 49 .

To this purpose, and, in particular, to make these clauses as clear as possible, we list here the different sort of functions 50 entering the process: [START_REF] Blanchette | Frege's Conception of Logic[END_REF] First-level functions with one argument, which are saturated by a single object; an indeterminate name for such a function is 'Φ (ξ)', whereas 'Φ (Γ)' is a corresponding name of an unspecified value of it; for short, we denote the totality of these functions 51 with 'F [START_REF] Blanchette | Frege's Conception of Logic[END_REF][START_REF] Blanchette | Frege's Conception of Logic[END_REF] ';

F [1,
F [2,[START_REF] Blanchette | Frege's Conception of Logic[END_REF] First-level functions with two arguments, which are saturated by two objects; an indeterminate name for such a function is 'Φ (ξ, ζ)', whereas 'Φ (Γ, ∆)' is a corresponding name of an unspecified value of it; for short, we denote the totality of these functions with 'F [2,[START_REF] Blanchette | Frege's Conception of Logic[END_REF] ';

F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] Second-level functions with one argument provided by a first-level function with one argument; an indeterminate name for such a function is 'Ω β (ϕ(β))' 52 , whereas 'Ω β (Φ(β))' is a corresponding name of an unspecified value of it; we denote the totality of these functions with 'F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] ';

F [2,2] Second-level functions with one argument provided by a first-level function with two arguments; an indeterminate name for such a function is 'Ω β,γ (ϕ(β, γ))', whereas 'Ω β,γ (Φ(β, γ))' is a corresponding name of an unspecified value of it; we denote the totality of these functions with 'F [2,2] ';

48 Cf footnote 52, below. 49 These will be inductive in nature. At the time when Grundgesetze was published, inductive clauses and definitions did not have in syntax the common role they have acquired later and still have today. So we should view his informal indications as a pioneering achievement rather than as imperfect definitions.

50 Rendering the second-order fragment of FGGBS as a modern system of second-order predicate logic would allow one to avoid the presently unfamiliar distinction between these sorts of functions, by replacing all of them with logical constants (as in the case of quantifiers) or predicates, possibly of higher-order. This would certainly avoid a difficulty in understanding his system, but would be very unfaithful both to its general spirit and to many more particular aspects of it.

51 Cf. p. 8, above, especially footnote 18.

52 Here 'ϕ' is intended to hold a place open for the arguments of the second-level function, just like 'ξ' and 'ζ' do for the arguments of first-level functions. The double occurrence of 'β' is, instead, intended to mean that the argument-place of a first-level function providing this argument is not held open (since it is filled up either with an object-name, or with a letter bounded by a quantifier, or by the operator involved in the value-range functions). An analogous notation will also be used below.

F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]3] Third-level functions with one argument provided by a second-level function with one argument provided by a first-level function with one argument; an indeterminate name for such a function is 'Υ δ (µ β (δ (β)))'53 , whereas 'Υ δ (Ω β (δ (β)))' is a corresponding name of an unspecified value of it; we denote the totality of these functions with 'F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]3] ';

F [2,3] Third-level functions with one argument provided by a second-level function with one argument provided by a first-level function with two arguments; an indeterminate name for such a function is 'Υ δ (µ β,γ (δ (β, γ)))', whereas 'Υ δ (Ω β,γ (δ (β, γ)))' is a corresponding name of an unspecified value of it; we denote the totality of these functions with 'F [2,3] '.

For reasons we will not discuss here, related to his use of value-ranges, Frege did not need to go further or to complete this hierarchy by considering functions of level higher than the third, and other sorts of first-, second-, or third-level functions, or unequal levelled-functions. Functions like the latter-an indeterminate name of one of which is, for example, 'ϕ(ξ)'-are mentioned by Frege ([18], § I.22), but are, in fact, unnecessary for our task.

Higher-Level Basic Functions

This hierarchy having been fixed, in general, it is now time to introduce the basic functions of FGGL2 R . Among them, the only first-level ones are the same already involved in FGGPL, namely ξ, ¬ξ, ζ ⇒ ξ and ξ = ζ, which are then incorporated within FGGPL R , as said above (but note that the arguments of the function ξ = ζ are now to be intended to be objects in general, and not only values of the function ξ, as in FGGPL). To these first-level functions, three other basic functions are to be added: ∀aϕ (a), which is a second-level function with one argument provided by a first-level function with one argument; ∀fµ β (f (β)), which is a third-level function with one argument provided by a second-level function with one argument provided by a first-level function with one argument; and ∀fµ β,γ (f (β, γ)), which is a third-level function with one argument provided by a second-level function with one argument provided by a first-level function with two arguments.

To define them, let us admit that we know the truth conditions of any statement of the natural language of the following forms, provided that 'Γ' and '∆' are indeterminate object-names: -'∆ is T if Φ (ξ) is such that Φ (Γ) is T whatever object Γ might be, and it is F if Φ (ξ) is not such that Φ (Γ) is T whatever object Γ might be';

-'∆ is T if Ω β (ϕ (β)) is such that Ω β (Φ (β)
) is T whatever one-argument first-level function Φ (ξ) might be, and it is

F if Ω β (ϕ (β)) is not such that Ω β (Φ (β)) is T whatever one-argument first-level function Φ (ξ) might be'; -'∆ is T if Ω β,γ (ϕ (β, γ)) is such that Ω β,γ (Φ (β, γ)
) is T whatever two-arguments first-level function Φ (ξ, ζ) might be, and it is F if Ω β,γ (ϕ (β, γ)) is not such that Ω β,γ (Φ (β, γ)) is T whatever two-arguments first-level function Φ (ξ, ζ) might be'.

We can define the above-mentioned three basic functions as follows:

-Let ∀aϕ (a) : F [START_REF] Blanchette | Frege's Conception of Logic[END_REF][START_REF] Blanchette | Frege's Conception of Logic[END_REF] → {T, F} be such that

∀aΦ (a) is T if Φ (ξ) is such that Φ (Γ) is T whatever object Γ might be F if Φ (ξ)
is not such that Φ (Γ) is T whatever object Γ might be ;

-Let ∀fµ β (f (β)) : F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] → {T, F} be such that

∀fΩ β (f (β)) is        T if Ω β (ϕ (β)) is such that Ω β (Φ (β)
) is T whatever one-argument first-level function Φ (ξ) might be

F if Ω β (ϕ (β)) is not such that Ω β (Φ (β)
) is T whatever one-argument first-level function Φ (ξ) might be ; -Let ∀fµ β,γ (f (β, γ)) : F [2,2] → {T, F} be such that

∀fΩ β,γ (f (β, γ)) is        T if Ω β,γ (ϕ (β, γ)) is such that Ω β,γ (Φ (β, γ)) is T whatever two-arguments first-level function Φ (ξ, ζ) might be F if Ω β,γ (ϕ (β, γ)) is not such that Ω β,γ (Φ (β, γ)) is T whatever two-arguments first-level function Φ (ξ, ζ) might be .
Here the lower-case Gothic letters 'a' and 'f' have to be intended as changeable parts of the functionnames '∀aϕ (a)', '∀fµ β (f (β))', and '∀fµ β,γ (f (β, γ))'. We shall see that it will be convenient to endow them with an appropriate index, in order to avoid ambiguities.

The functions ∀aϕ (a), ∀fµ β (f (β)), and ∀fµ β,γ (f (β, γ)) render, of course, Frege's functions a ϕ (a) ( [18], § I.8), f µ β (f (β)), and f µ β,γ (f (β, γ)) ( [18], § I.19) 54 , under the assumption that the horizontal dashes on the two sides of the concavity in ' a ' and ' f ' are occurrences of the horizontal stroke that also occurs within ' -ξ', and can then be considered as a unique stroke by fusion of horizontals.

These functions having been introduced, it is clear how to use them to generate terms that do not include FGGPL object-letters, by only including symbols that (as we shall see latter, but can be easily understood already by analogy with FGGPL) are also allowed to enter FGGL2 R well-formed formulas. The function ξ can, for example, provide the argument of ∀aϕ (a), so as to give the value ∀aa, or (by fusion of horizontals) ∀aa, which is nothing but F, and whose name '∀aa' is clearly then a term. Analogously, the function ∀aϕ (a) can provide the argument of ∀fµ β (f (β)), so as to give the value ∀f∀af (a), which is, again, nothing but F, and whose name '∀f∀af (a)' is a term, too. Moreover, these two terms, can be taken as names of arguments of the function ζ ⇒ ξ, so as to get its value ∀aa ⇒ ∀f∀af (a), which is nothing but T, and whose name '∀aa ⇒ ∀f∀af (a)' is also a term. It should be also clear, however, that, by proceeding this way, one could never get something like '∀ff (∀aa)', which should be, instead, a genuine term of FGGL2 R , since it is nothing but the name of the value of the function ∀fµ β (f (β)) for the second-level function ϕ (∀aa) as argument, which is, in turn, a genuine second-level function with one argument provided by a first-level function with one argument 55 . The problem is that, proceeding in this way, there is no way to get the name of this second-level function, so as to use it to saturate '∀fµ β (f (β))'. To get the term '∀ff (∀aa)', one might rather proceed as follows: one begins from '∀aa ⇒ ∀f∀af (a)' and analyses it as the name of the value of the one-argument first-level function ξ ⇒ ∀f∀af (a) for ∀aa as an argument, which reduces to desaturating '∀aa ⇒ ∀f∀af (a)' with respect to '∀aa', so as to get 'ξ ⇒ ∀f∀af (a)'; then one considers '∀aa ⇒ ∀f∀af (a)' again, but analyses it, now, as the name of the value of the function ϕ (∀aa) for the function ξ ⇒ ∀f∀af (a) as an argument, which reduces to desaturating '∀aa ⇒ ∀f∀af (a)' with respect to 'ξ ⇒ ∀f∀af (a)', so as to get 'ϕ (∀aa)'; finally, 54 Frege's definition of these two latter functions is not detailed at all, in fact. He merely suggests it by introducing Gothic "function-letters"to be used in an analogous way as Gothic "object-letters" ( [18], § I.19; [22], pp. 341-351).

55 This is nothing but the function ϕ (Γ) under the condition that Γ is ∀aā, which, as said just above, is nothing but F. The appeal to this function is made perfectly rightful by having defined the function ∀fµ β (f (β)) on the whole totality F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] , in agreement with Frege's universalist conception, and independently of any restriction that this totality might plausibly be submitted to (since 'ϕ (Γ)' is a perfectly admissible function-name in any language suitable for rendering the language of FGGBS), which is made manifested, by the way, by Frege's appealing to the FGGL2R Roman function-marker 'ϕ (a) ⇒ ϕ (b)' in his derivation of theorem IIIa ( [18], § I.50; for the notion of Roman FGGL2R function-marker, cf. sections 4.4, below).

one takes the value of ∀fµ β (f (β)) for ϕ (∀aa) as an argument, which reduces to saturating '∀fµ β (f (β))' with 'ϕ (∀aa)', so as to get '∀ff (∀aa)', as required.

This example, should be enough to show the complexity of the process to be followed in order to get all the terms that one should be able to get within (the language of) FGGL2 R , by avoiding any provisional appeal to letters to be used to designate unspecified objects or functions. Such a process crucially differs both from the one that we followed to generate FGGPL R terms, for it involves no appeal to such letters, and from the one that is usually followed in a modern system of logic, since it depends on a continuous coming and going from object-to function-names and vice versa 56 .

St

T n+1 [FGGL2 R ]
A string of symbols θ to be included in T n+1 is generated at step n + 1 if and only if one of the following conditions obtains:

St T n+1 [FGGL2 R ] .i θ results from a string included in F [1,1]
0→n by replacing, in it all occurrences of 'ξ' with a string included in T 0→n ; 1] 0→n by respectively replacing in it all occurrences of 'ξ' and of 'ζ' with a string of symbols included in T 0→n ;

St T n+1 [FGGL2 R ] . ii θ results from a string included in F [2,
St T n+1 [FGGL2 R ] . iii θ results from a string υ 2 included in F [1,2]
0→n by replacing in it all occurrences of ϕ(ϑ), where ϑ is a C T [FGGL2 R ] string which involves the same number of opening and of closing parentheses, with the C T [FGGL2 R ] string ϑ , which results, in turn, from a string υ 1 included in F [1,1] 0→n by replacing in it all occurrences of 'ξ' with ϑ; if within ϑ a Gothic letter occurs, which also occurs within υ 1 with the same index, one has to preventively replace in υ 1 all occurrences of it with the same Gothic letter with another index such that this letter occurs with this latter index neither in ϑ, nor in υ 1 , nor in υ 2 ;

St T n+1 [FGGL2 R ] . iv θ results from a string υ 2 included in F [2,2]
0→n by replacing in it all occurrences of ϕ(ϑ, ϑ ), where ϑ and ϑ are C T [FGGL2 R ] strings which involve the same number of opening and of closing parentheses, with the C T [FGGL2 R ] string ϑ , which results, in turn, from a string υ 1 included in F [2,1] 0→n by replacing in it all occurrences of 'ξ' and 'ζ' respectively with ϑ and ϑ ; if within ϑ or ϑ a Gothic letter occurs, which also occurs within υ 1 with the same index, one has to preventively replace in υ 1 all occurrences of it with the same Gothic letter with another index such that this letter occurs with this latter index neither in ϑ, nor in ϑ , nor in υ 1 , nor in υ 2 ;

St T n+1 [FGGL2 R ] . v θ is a string like ∀f m ϑ, where ϑ is a C T [FGGL2 R ]
string that results from a string υ included in F [1,2] 0→n by replacing in it all occurrences of 'ϕ' with 'f m ', and m is any index such that 'f m ' does not occur within υ;

St T n+1 [FGGL2 R ] . vi θ is a string like ∀f m ϑ, where ϑ is a C T [FGGL2 R ]
string that results from a string υ included in F [2,2] 0→n by replacing in it all occurrences of 'ϕ' with 'f m ', and m is any index such that 'f m ' does not occur within υ;

St F [1,1] n+1 [FGGL2 R ] A string of symbols θ to be included in F [1,1]
n+1 is generated at step n + 1 if and only if θ results from a string υ included in T 0→n by replacing some (possibly all) occurrences of a C T [FGGL2 R ] string ϑ that forms a part of υ with 'ξ';

St F [2,1] n+1 [FGGL2 R ] A string of symbols θ to be included in F [2,1]
n+1 is generated at step n + 1 if and only if θ results from a string υ included in F [1,1] 0→n by replacing some (possibly all) occurrences of a C T [FGGL2 R ] string ϑ that forms a part of υ with 'ζ';

St F [1,2] n+1 [FGGL2 R ]
A string of symbols θ to be included in F [1,2] n+1 is generated at step n + 1 if and only if θ results from a string τ included in T 0→n by respectively replacing in it some (possibly all) occurrences of some C T [FGGL2 R ] strings ϑ i (i = 1, 2, . . . , n; where n is whatever natural number) with ϕ(ϑ i ), provided that ϑ i be some C T

[FGGL2 R ] strings such that a certain C T [FGGL2 R ]
∪ {ξ} string υ (the same for any value of i)

those that do not): no such name is such that the previous clauses allow to generate, out from it and from other FGGL2 R function-names or terms, a term naming an object other than a truth-value. Hence, though the functions that one can name using L T,FN [FGGL2 R ] (and that seem, then, to be unquestionably ascribable to the totalities F [i,j] n ) include functions other than concepts an relations, no value of these other functions other than a truth-value can be named using L T,FN [FGGL2 R ] . To form a name of an object other than a truthvalue, one has then, to go beyond L T,FN [FGGL2 R ] . One could do that by enriching L T,FN [FGGL2 R ] with indeterminate object-names, namely with FGGPL object-letters, by also admitting that the unspecified objects named by them include objects other than truth-values. By coming back, then to a situation close to that of FGGLP. This move would not be faithful to Frege, however, since, also in the language of FGGBS, indeterminate object-names enter only as preliminary tools. The good way to name such other objects in this language is rather by appealing to the value-range and the definite description functions. It is only the introduction of these functions that makes plausible the admission that the objects that FGGBS is dealing with go beyond T and F. This is certainly a reason why Frege did not think of the second-order fragment of his system as a separate system of logic. So conceived, it would have had a quite poor expressive power.

This having been said, let us come back to the formal presentation of FGGL2 R , namely to its particular statements. To to allow their formation, it is enough to add to L T,FN [FGGL2 R ] the symbol ' ', so as to get the language L PS

[FGGL2 R ] = L T,FN [FGGL2 R ] ∪
. The passage from FGGL2 R terms to FGGL2 R particular statements is, indeed, governed, mutatis mutandis, by the same stipulations that govern the passage from FGGPL R terms to FGGPL R particular statements:

St PS [FGGL2 R ] . i If θ is a FGGL2 R term, then θ is a FGGL2 R particular statement. St PS [FGGL2 R ]
. ii Nothing else is a FGGL2 R particular statement.

The understanding of FGGL2 R particular statements is, mutatis mutandis, the same as that of FGGPL R particular statements. If θ is a FGGL2 R particular statement, let us say that θ is its FGGL2 R term, and stipulate that:

St As.PS [FGGL2 R ]
A FGGL2 R particular statement asserts that the truth-value named by its FGGL2 R term is T;

St Hld.PS [FGGL2 R ] A FGGL2 R particular statement holds if its FGGL2 R
term is a name of T; and it does not hold if its FGGL2 R term is a name of F.

Concerning the way they are respectively connected to FGGPL R and FGGL2 R terms, FGGL2 R particular statements are, then, perfectly analogous to FGGPL R ones. The essential difference between FGGPL R and FGGL2 R particular statements merely depends on the essential difference between FGGPL R and FGGL2 R terms, which we have discussed in § 4.1, above. As a consequence, whereas FGGPL R particular statements cannot be considered as FGGL2 R well-formed formulas, there is no reason to stay away from taking FGGL2 R particular statements as FGGL2 R well-formed formulas. We shall come back to this in § 4.5, below.

Roman Object-and Function-Marks

Preliminary Explanations

The difference between FGGPL R and FGGL2 R terms has another important consequence on the difference between FGGPL R and FGGL2 R particular statements. Indeed, these statements have different roles in the derivations within FGGPL R and FGGL2 R , respectively. Since, the fact that in FGGL2 R particular statements involve neither FGGPL R object-letters, nor analogous function-letters (cf. p. 30, above) not only allows one to consider these statements as FGGL2 R well-formed formulas, but also forbids to define the relation of being an instance of, on these formulas, and to state the corresponding rule of substitution by relying on these object-and function-letters.

The problem concerns the expression of generality in FGGBS, and, consequently, in FGGPL R and in FGGL2 R . In FGGPL R , generality is expressed through Roman letters. These letters play an analogous role also in FGGL2 R , but generality is expressed, there, by the functions ∀aϕ (a), ∀fµ β (f (β)), and ∀fµ β,γ (f (β, γ)), that, as we have seen, essentially occur, through their values, within FGGL2 R particular statements. This second way of expressing generality is limited to a term or a statement, but does not extend to a derivation, since the scope of a quantification cannot go beyond FGGL2 R terms or FGGL2 R statements (and this independently of their being particular or general terms or statements, as will be clear below). The point is clearly made by Frege himself in § I.17 of the Grundgesetze: though both ' a a 4 = 1 . vi applies, provided that ' -a 2 = 1 ', ' -a 4 = 1 ' and ' -a 8 = 1 ' be taken as instances of ' -a', ' -b' and ' -c', for example.

a 2 = 1
Frege's example is quite simple, and his point quite clear. But the simplicity of the example hides the essential point. To present this example, Frege took the liberty to designate by '1' and 'ξ 2 ', 'ξ 4 ', 'ξ 8 ' an object (other than a truth-value) and three functions that are not introduced in the previous parts of his treatise. He clearly entrusted the informal knowledge of the reader the responsibility of giving a sense to these names. But this knowledge cannot force the statements ' a 4 = 1

a 2 = 1
' and ' a 8 = 1

a 4 = 1
' and their components ' -a 2 = 1 ', ' -a 4 = 1 ' and ' -a 8 = 1 ' to belong to the propositional fragment of FGGBS, and this not only since the object 1 and the functions ξ 2 , ξ 4 , and ξ 8 are not defined there, but also and overall, because these latter functions are not propositional in nature. In our rendering, this means that there is no way to extend FGGPL, while remaining in the limits of a propositional system, so as to make that the statements ' a 2 = 1 ⇒ a 4 = 1', ' a 4 = 1 ⇒ a 8 = 1' and their components 'a 2 = 1', 'a 4 = 1' and 'a 8 = 1' belong to the relevant extension of this system. These statements and components are inescapably non-propositional in nature. But, if, as we have seen, going beyond FGGPL entails also abandoning a non-purely informal use of FGGPL object-letters and of analogous function-letters, then one cannot hope to rely on these last letters to explain the passage from ' a 2 = 1 ⇒ a 4 = 1', ' a 4 = 1 ⇒ a 8 = 1' to ' a ⇒ b', ' b ⇒ c', and, then, the 64 Indeed a rule close to universal generalisation is admitted in FGGBS, and introduced, some line below, in § I.17 (we shall introduce its rendering in FGGL2R in § 4.5), but, alone, it is not suitable for this purpose. If an analogue of the theorem of deduction is admitted, his Basic Laws IIa and IIb are moreover close to the first-and second-order rules of universal instantiation (we shall come back to them in § 4.6). But their use in deduction depends on the definition of the relation of being an instance of, on the well-formed formulas of his system, which depends, in turn, on the solution of the difficulty that is here at stake. 65 Of course, Frege did not appeal to a notion such as that of proposition, and was quite elusive on this matter. Using this notion appears to us as the simplest way to make his point explicit, however.

FGGL2 R object-marker, one has to instantiate, in the latter, 'f (ξ)' with the function-name '∀aa = a ⇒ ξ'. Now, just like 'f (∀aa)' is a FGGL2 R object-marker, 'f (ξ)' is a FGGL2 R function-marker for first-level functions. This is also the case of 'g (ξ)' and 'g ξ ⇒ ∀aa ', since 'g' is another Roman letter for first-level functions. Both these last FGGL2 R function-markers can be used to instantiate 'f (ξ)', in 'f (∀aa)', again, so as to pass from this last FGGL2 R object-marker to its two new instances 'g (∀aa)' and 'g ∀aa ⇒ ∀aa '. It follows that also the FGGL2 R general statements ' g (∀aa) = g (∀aa)' and ' g ∀aa ⇒ ∀aa = g ∀aa ⇒ ∀aa ' are instances of ' f (∀aa) = f (∀aa)', and follow, then, from it.

Finally, it is enough to consider that the FGGL2 R term '∀f 1 ∀a 1 f 1 (a 1 )' is an instance of the FGGL2 R object-marker '∀f 1 M β (f 1 (β))' to conclude that the FGGL2 R particular statement ' ∀f 1 ∀a 1 f 1 (a 1 ) = ∀f 1 ∀a 1 f 1 (a 1 )' is, instead, an instance of ' ∀f 1 M β (f 1 (β)) = ∀f 1 M β (f 1 (β))', and follows, then, from it. To get this term from this FGGL2 R object-marker, one has to instantiate, in the latter, 'M β (f 1 (β))' with the function-name '∀a 1 ϕ (a 1 )'. Hence, so as 'f (ξ)' is a FGGL2 R function-marker for first-level functions, 'M β (ϕ (β))' is a FGGL2 function-marker for second-level functions.

Besides showing the nature of FGGL2 function-markers, these last examples should also make clear that FGGL2 function-markers play a crucial role in derivations within FGGL2. Insofar as they include the letters 'ξ', 'ζ', and 'ϕ', used to hold a place open for appropriate arguments (the absence of 'ζ' in the foregoing examples merely depends on the fact that, for the sake of simplicity, these examples are so chosen as to involve no two-arguments first-level function), this entails that also these last letters play a crucial role in derivations within FGGL2 R , in spite of the fact that they do not occur within FGGL2 R well-formed formulas. This induces a crucial structural difference between derivations within FGGL2 R and derivations within both FGGPL R and modern systems of logic.

Formal Treatment

Let be C OM [FGGL2 R ] = C T [FGGL2 R ]
∪ {a, b, c, d, . . . , f, g, h, . . . , M, . . . , β, γ, . . . , }, where the ellipses are intended to remain for the same letters 'a', 'b', 'c', 'd', 'f ', 'g', 'h', 'M ', 'β', 'γ' endowed with appropriate indexes. Call, for short, 'a', 'b', 'c', 'd',. . . 'FGGL2 R general letters for objects', 'f ', 'g', 'h',. . . 'FGGL2 R general letters for first-level functions' and 'M ',. . . 'FGGL2 R general letters for second-level functions', and 'β', 'γ', ,. . . 'FGGL2 R bounding letters' (these last letters are used as above67 ). We shall define FGGL2 R objectand function-markers respectively as C OM (i, j = 1, 2) progressively generated according to an inductive procedure that differs from that according to which the families T and F [i,j] (i, j = 1, 2) are generated, only in that it starts from larger bases, namely from six basic families TR 0 and FR as their proper sub-families. It results that also the whole families TR and FR [i,j] respectively contain T and F [i,j] as their proper sub-families, just as well as, for any n, TR n and FR as their proper sub-families. FGGL2 R object-and function-markers will be, more precisely, identified with the strings included in TR and FR [i,j] but not in T and F [i,j] Insofar as we have already defined the relation of being an instance of, on FGGL2 R terms and on FGGL2 R object-markers, we can easily extend this definition to FGGL2 R well-formed formula:

St Is.WWF [FGGL2 R ]
A FGGL2 R well-formed formula ϑ is an instance of a FGGL2 R well-formed formula ϑ if and only if ϑ is an instance of ϑ.

From these stipulations, it follows that any FGGPL R well-formed formula is also a FGGL2 R well-formed formula. One might also verify that the former is an instance of another FGGPL R well-formed formula according to St . It remains that, having defined FGGL2 R general statements in the previous way, it is no longer possible to explain what it means for such a statement to hold by appealing to something as its corresponding particular statements, as we did for FGGPL R general statements. Admitting that, if ϑ is a FGGL2 R general statement, ϑ is its FGGL2 R object-marker, all that can be stipulated is the following:

St As.GS [FGGL2 R ]
A FGGL2 R general statement asserts that any object-name that counts as an instance of its FGGL2 R object-marker is a name of T.

St Hld.GS [FGGL2 R ] A FGGL2 R general statement holds if and only if any object-name that counts as an instance of its FGGL2 R object-marker is a name of T.

Axioms and Theorems

According to this last stipulation and the meaning assigned to the functions ∀aϕ (a), ∀fµ β,γ (f (β, γ)), and ∀fµ β (f (β)), is it easy to see that the three following FGGL2 R general statements:

Ax These axioms having been stated, it is now time to define the relation of following from, on FGGL2 R well-formed formulas. This is to be done, of course, in a quite different way than for FGGPL R well-formed formulas, that is, without appealing to any sort of correspondence between two different sorts of FGGL2 R statements.

To this purpose, one has to begin by adapting the rules Rl PS [FGGPL R ] . i -viii so as to get new deductive rules applicable to FGGPL R well-formed formulas. This is easily done by simply replacing in these rules any occurrence of 'FGGPL R particular statement(s)' with an occurrence of 'FGGL2 R well-formed formula(s)', and any occurrence of 'FGGPL R term(s)' with an occurrence of 'FGGL2 R term(s) or object-marker(s)'. Call 'Rl WWF [FGGL2 R ] . i -viii ' the rules obtained in this way.

To these eight rules, two others are to be added:

Concluding Remarks

Both FGGPL R and FGGL2 R are not only quite different in nature from any modern system of propositional and second-order logic. They are also quite convoluted, even uselessly convoluted, one could think. This depends both on Frege's conception of logic, quite different with the one which is widely accepted today, and on the successive finding of a number of possible simplifications, many of which are connected to the abandonment of the use of functions to express predication, and could not have, then, been possible in Frege's setting, dominated by the primitive opposition of objects and functions. This is why we have not tried to simplify our systems. This would have made them unfaithful to Frege's conceptions, to which we have, rather, tried to stay as close as possible. Our aim was not to show how the propositional and second-order fragments of FGGBS could be amended (which is something that the successive development of logic has clearly shown), but to provide a reconstruction suitable for making the consequences of this conception as clear as possible for a modern reader, also, and overall, for the aspects of it that could today appear as quite archaic.

In discussing Frege's it is usual to emphasise its contentual nature and the absence of a clear distinction between its syntax and its semantics. We are far from undermining the importance of these aspects. We have discussed them, and they are reflected in our systems. Nonetheless, we have considered useful to focus on other features of this logic, most of which do not directly depend on them, being rather connected with more general views.

  -letter or a FGGPL R term, [θ] and [ϑ/θ] two FGGPL R terms such that θ occurs within [θ], and [ϑ/θ] results from [θ] by replacing in it all the occurrences of θ with ϑ, then [ϑ/θ] is an instance of [θ].30

  [FGGPL R ] .IV to Ax [FGGPL R ] .I as an axiom of FGGPL R -and consequently amending the stipulation St Th [FGGPL R ] so as to take as a theorem of FGGPL R any FGGPL R general statement that follows from Ax [FGGPL R ] .I and Ax [FGGPL R ]

1 a 4 = 1 '= 1 a 2 = 1 ' and ' a a 8 = 1 a 4 = 1 ' can also be expressed by ' a 4 = 1 a 2 1 a 4 = 1 '

 14112114112141 are particular statements, the latter cannot be derived from the former in agreement with any of the inference rules we rendered through Rl PS [FGGPL R ] . i -viii. The way Frege overcame the difficulty is not by introducing new inference rules concerned with the functions ∀aϕ (a), ∀fµ β (f (β)), and ∀fµ β,γ (f (β, γ)), analogous to the modern rules of universal instantiation and generalisation 64 . Frege, rather, argued that the general propositions 65 expressed by ' a a 4 , to which the inference rules we rendered through Rl GS [FGGPL R ]

  [FGGL2 R ] and C OM [FGGL2 R ] ∪ {ξ, ζ, ϕ} strings included in five families TR = ∞ n=0TR n and FR[i,j] =

  68 . We begin by stipulating that:St TR [FGGL2 R ] TR only includes C OM [FGGL2 R ]strings, and TR 0 = T 0 ∪ {a, b, c, d, . . .} = {a, b, c, d, . . .};

  [FGGL2 R ] .IIa ' ∀a 1 f (a 1 ) ⇒ f (a)' Ax [FGGL2 R ] .IIb ' ∀f 1 M β (f 1 (β)) ⇒ M β (f (β))' Ax [FGGL2 R ] .III ' g(a = b) ⇒ g ∀f 1 f 1 (b) ⇒ f 1 (a) ' hold. Since '∀a 1 Φ(a 1 ) ⇒ Φ(Γ)', '∀f 1 Ω β (f 1 (β)) ⇒ Ω β (Φ (β))' and 'Φ(Γ = ∆) ⇒ Φ ∀f 1 f 1 (∆) ⇒ f 1 (Γ)' all refer to T whatever objects, one-argument first-level function, and one-argument second-level function 'Γ', '∆', 'Φ (ξ)', and 'Ω β (ϕ (β))' might respectively designate. These statements render Frege's Basic Laws IIa, IIb and III ([18], § § I.20, I.25, and I.47) 74 Let us take them, together with Ax [FGGPL R ] .I, and Ax [FGGPL R ] .IV, as the axioms of FGGL2 R .

  replacing one or more of the occurrences of θ with θ then 35 : This renders Frege's rule of fusion of horizontals, intended as a deductive rule ([18], § I.48.1;[22], pp. 61 1 )[START_REF] Sandu | Ramsey and the notion of arbitrary function[END_REF] . PS [FGGPL R] .iii If κ i,1 , κ i,2 , . . . , κ i,n i (where i = 1, 2, 3 and n i is an arbitrary natural number), θ 1 , θ 2 , τ are FGGPL R terms, ' -→ κ i ⇒' (i = 1, 2) stand for 'κ i,1 ⇒ κ i,2 ⇒ . . .

	Rl ...
	[θ]		[θ]
	-----[θ/.θ]	and	-----[θ/.θ]	.

and [θ/.θ], [θ], and [θ/.θ] are five FGGPL R terms, such that θ occurs within [θ] either once or several times, θ occurs within [θ] either once or several times, [θ/.θ] results from [θ] by replacing one or more of the occurrences of θ with θ, and [θ/.θ] results from [θ] by ⇒ κ i,n i ⇒ ' (i.e. for nothing if n

  2; [22], pp. 22 1 and 61 1 ) 37 .

	Rl PS [FGGPL

R ]

.iv If κ i,1 , κ i,2 , . . . , κ i,n i (where i = 1, 2 and n i is an arbitrary natural number),

θ 1 , θ 2 are FGGPL R terms, ' -→ κ 1 ⇒' and '⇒ -→ κ 2 ' respectively behave like ' -→ κ 1 ⇒' and '⇒ -→ κ 3 ' in rule Rl PS [FGGPL R ] .

iii, and each of 'θ £ i ', 'θ ¡ i ' (i = 1, 2) stands either for 'θ i ' or for '¬θ i ', provided that 'θ ¡ i ' stands for '¬θ i ' if 'θ £ i ' stands for 'θ i ', and for 'θ i ' if 'θ £ i ' stands for '¬θ i ', then:

  PS [FGGPL R ] .vi If κ i,1 , κ i,2 , . . . , κ i,n i (where i = 1, 2 and n i is an arbitrary natural number), θ, τ are FGGPL R terms, ' -→ κ 1 ⇒' and '⇒ -→ κ 2 ' respectively behave like ' -→ κ 1 ⇒' and '⇒ -→ κ 3 ' in rule Rl PS [FGGPL R

  and I.48.6;[22], pp. XXVII 1 , 25-26 1 and 62 1 ).] .vii If κ i,1 , κ i,2 , . . . , κ i,n i (where i = 1, 2, 3, 4 and n i is an arbitrary natural number), θ, τ , ϑ are FGGPL

	Rl PS [FGGPL R R terms, ' -→ κ 1 ⇒', ' -→ κ 3 ⇒', ' -→ κ 2 ⇒', and ' -→ κ 4 ⇒' behave like ' -→ κ 1 ⇒' in rule Rl PS [FGGPL R ] . iii, while '⇒ -→ κ 2 ' and '⇒ -→ κ 4 ' behave like '⇒ -→ κ 3 ' in this same rule, then:

  If θ, ϑ and τ are FGGPL R particular statements, τ respectively follows from θ, or from θ and ϑ, if it immediately follows from them (according to the rules Rl PS[FGGPL R ] . i.viii ). ] .ii If τ , θ i (i = 1, 2, . . . , n), ϑ i (i = 1, 2, .. . , m) are FGGPL R particular statements, τ follows from θ 1 , θ 2 , . . . , θ n , and θ 1 follows from ϑ 1 , . . . , ϑ m , then τ follows from ϑ 1 , . . . , ϑ m , θ 2 , . . . , θ n .

	St Flw.PS [FGGPL R St Flw.PS [FGGPL

R ]

. iii No FGGPL R particular statement follows from any number of other FGGPL R particular statements if it does not follow from them according to St Flw.PS [FGGPL R ] . i and St Flw.PS [FGGPL R ] . ii. 38 In Frege's deductions, the appeal to rules Rl PS [FGGPL R ] . iii,v is not made explicit, while rule Rl PS [FGGPL R

  If θ is a FGGPL R particular statement and |θ| results from it by replacing each distinct FGGPL R object-letter in it with a distinct FGGPL R general letter for objects (so that any occurrence of the same FGGPL R object-letter is replaced by an occurrence of the same FGGPL R general letter for objects), then the latter is a FGGPL R general statement.

	St GS [FGGPL

R ]

.ii Nothing else is a FGGPL R general statement.

St WFF [FGGPL R ] FGGPL R general

statements are the only well-formed formulas of FGGPL R . If a FGGPL R general statement results from a FGGPL R particular one as |θ| is said to result from θ in stipulation St GS [FGGPL R ]

  1, 2, . . . , n) are FGGPL R general statements, then |τ | follows from |θ 1 |, . . . , |θ n | if and only if |τ |, |θ i | uniformly correspond to as many FGGPL R particular statements τ , θ i such that τ follows from θ 1 , . . . , θ n 41 .

  GS [FGGPL R ] . i -viii be the rules that are obtained this way. As for the rules Rl PS [FGGPL R ] . i -viii, let us say that the output of each of them immediately follows from its input or inputs. While the understanding and application of rules Rl GS [FGGPL R ] . ii -viii require no further explanation, this is not so for Rl GS [FGGPL R ] . i. To understand and apply it, a definition of the relation of being an instance of, on FGGPL R particular statements, is needed. To provide it, one could appropriately adapt stipulations St Is.T [FGGPL R ] and St Is.PS [FGGPL R] to FGGPL R object-markers and FGGPL R particular statements, respectively. Still, it is much easier (and perfectly equivalent) to adopt the following stipulation:

	St Is.GS [FGGPL

R

]

A FGGPL R general statement τ is an instance of a FGGPL R general statement θ if and only if a FGGPL R particular statement which corresponds to τ is an instance of a FGGPL R particular statement which corresponds to θ 42 .

At this point, stipulation St

Flw.PS [FGGPL R ] can be restated on the model of stipulations St Flw.GS [FGGPL R ] . i-iii, that is, as follows: St Flw.GS * [FGGPL R ] . i If θ, ϑ and τ are FGGPL R general statements, τ respectively follows from θ, or from θ and ϑ if it respectively immediately follows from them (according to the rules Rl GS

  1, 2, . . . , m) are FGGPL R general statements, τ follows from θ 1 , θ 2 , . . . , θ n , and θ 1 follows from ϑ 1 , . . . , ϑ m , then τ follows from ϑ 1 , . . . , ϑ m , θ 2 , . . . , θ n . St Flw.GS * [FGGPL R ] .iii No FGGPL R general statement follows from any number of other FGGPL R general statements if it does not follow from them according to St Flw.GS * [FGGPL R ] .i and St Flw.GS

* [FGGPL R

]

.ii.

At this point, it only remains to stipulate that:

St Th [FGGPL R ] A FGGPL R general

statement is a theorem of FGGPL R if and only if it follows from Ax [FGGPL R ] .I.

  Is.GS [FGGPL R ] if and only it is so according to St Is.WWF [FGGL2 R ]

This system results from a revision and extension of the system previously presented in Frege's 1879 booklet titled in same way ([START_REF] Frege | Begriffsschrift, eine der Arithmetischen nachgebildete Formelsprache des reinen Denkens[END_REF]). To avoid any confusion, we shall use, here, the acronym 'FGGBS' (for 'Frege Grundgesetze Begriffsschrift') to refer only to the former system. We use the whole word 'Begriffsschrift' (in italic) to refer to the 1879 booklet.

Notice, however, that whereas the theory of natural numbers should have merely required appropriate definitions, since those should have been enough for warranting the existence of these numbers, that of real numbers should have also required an existence proof for domains of magnitudes (these numbers being identified by Frege with ratios of magnitudes), since their existence would have not been warranted by their definition ([START_REF] Simons | Frege's theory of real numbers[END_REF];[START_REF] Dummett | Frege. Philosophy of Mathematics[END_REF], ch. 22;[START_REF] Schirn | Frege's approach to the foundations of analysis (1874-1903)[END_REF];[START_REF] Snyder | Frege on the real numbers[END_REF]).

In Frege's parlance-which we shall also adopt here-first-level functions are those whose arguments are required to be objects, while n-level functions (n = 2, 3, . . .) are those whose arguments are required to be n -1-level functions. As it will become clear later, Frege employed functions where we would rather employ predicates. Hence, his first-level functions often work, mutatis mutandis, as first-level predicates, and higher-level functions as higher-level predicates.

Cf. footnote 1, above. Though there are many relevant differences between the two systems, we avoid this matter here, and rather limit our attention to the (more mature) system of the Grundgesetze, namely FGGBS.

On the eliminability of the appeal to value-ranges from many of Frege's deductions in the Grundgesetze, cf.[START_REF] Heck | The development of arithmetic in Frege's Grundgesetze der Arithmetic[END_REF], pp. 581-584, and[START_REF] Heck | Reading Frege's Grundgesetze[END_REF], §

6.1. Notice, however, that eliminating value-ranges would often require the appeal to functions of third or even higher level, which results in formulas that have not a plain rendering within a second-order predicate language.6 Notice, however, that in the Foreword to the Grundgesetze, Frege remarks that a "dispute [Streit]" about the logical nature of his derivations "can arise only concerning my basic law of value-range (V)" and continues as follows: "I take it to be purely logical. At any rate, the place is hereby marked where there has to be a decision " ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], Vorwort, pp. VII;[START_REF] Frege | Basic Laws of Arithmetic[END_REF], p. VI1). This seems to suggest that Frege deemed questionable the logical nature of Basic Law V (and VI), or, at least, considered it less certain than that of his other laws.[START_REF] Demopoulos | Frege and the rigorization of analysis[END_REF] This part is plainly titled 'Exposition [Darlegung] of the Begriffsschrift'. It contains an informal presentation of Frege's system, namely its language, its Basic Laws (or axioms), its deductive rules, and its basic (explicit) definitions. The remaining part of the Grundgesetze (with the exception of § § II.55-II.164, offering a critical discussion of some alternative definitions of real numbers and advancing the desiderata that a suitable definition should have met, according to Frege) are devoted to prove theorems within this very system.

Frege is quite explicit on this point in the Introduction to the Grundgesetze ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], Einleitung, pp. 2-3).

This term occurs pervasively within the Grundgesetze. The first occurrence is within § I.1, where it refers to the expression ' `2 + 3ξ 2 ´ξ'.

As a matter of fact, Frege rejected any limitation to the domain of his functions. Hence, to say that a function is numerical, that is, only admits numbers as arguments, is quite inappropriate, according to his view. Still, we are here at the very beginning of the treatise and he seems to have felt free to fall into this impreciseness, which is signalled, by the way, by his following mathematicians in writing 'x' instead of 'ξ', as recommended by him just some lines later.

This is also what is suggested by Frege's mention of the paradox in the Grundgesetze ([18], § I.4, footnote (1), p. 8; [22],

Cf. footnote[START_REF] Dummett | Frege. Philosophy of Mathematics[END_REF], above.

The indispensability of a preparatory stage in the understanding of logic, according to Frege's conception, has often been pointed out by speaking of elucidation (Erläuterung), for example by Weiner in[START_REF] Weiner | Frege in Perspective[END_REF], ch. 6, and[START_REF] Weiner | Understanding Frege's project[END_REF], pp. 58-61. The term 'Erläuterung' appears only marginally in the Grundgesetze, without a clear defined meaning([18] , § § I.1, footnote (1), and I.[START_REF] Potter | Reason's Nearest Kin. Philosophies of Arithmetic from Kant to Carnap[END_REF][START_REF]The Cambridge Companion to Frege[END_REF], as well as in Über Begriff und Gegenstand ([START_REF] Frege | Über Begriff und Gegenstand[END_REF], p. 193). Still the idea that is generally associated with this term is expressed, by means of the term 'exposition [Darlegung]', in the following passage from the Introduction of the Grundgesetze ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], Einleitung, pp. 3-4;[START_REF] Frege | Basic Laws of Arithmetic[END_REF], pp. 31-41):

The role of functions in this rendering appears quite clearly when it is observed that these appropriate terms are names of values of appropriate functions, namely concepts or relations (that is, functions of one or more arguments whose values are truth-values).

The exception of Basic Law V does not depend, of course, on the fact that Frege was not taking this Law to hold, but rather on the fact that the meaning he attributed to the value-ranges function is just fixed by this Law ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], § § I.3, I.9, and I.20). This function having been introduced, Frege fixed, then, the meaning of the definite-descriptions function by appealing to it, in such a way that Basic Law VI promptly results from the way this meaning is fixed.

Semantically speaking, this could be understood as a consequence of Frege's view that any term purportedly refers, that is, designates an object: cf what we have said above (pp. 7, and 11 on Frege's distinction between indicating and designating). This is indeed what Frege openly claimed in the Foreword of the Grundgesetze ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], Vorworth, p. XII;[START_REF] Frege | Basic Laws of Arithmetic[END_REF], p. XII1):When one has reached the end, one should reread the entire exposition of Begriffsschrift [namely the first, expository part of the Grundgesetze, i.e. the system FGGBS: cf. footnote 1, above] with this as background, keeping in mind that those stipulations that will not be used later, and therefore appear unnecessary, serve to implement the principle that all correctly formed signs ought to refer to something -a principle that is essential for full rigour.

This is an example of analysis of an object-name: such a name being given, one analyses it by looking for the names of functions one can get from it, by desaturating (cf. footnote 46, below) it in different ways (a practice perfectly in line with the

Note the difference between the meaning that is here ascribed to these symbols and the one that they usually take in a contemporary set-theoretic setting (provided that speaking of objects in general makes sense in this setting). Note in particular that, here 'O 2 ' is not used to denote a domain of pairs (that is, the totality of pairs of objects), but merely to indicate that the relevant function has two arguments. In Frege's spirit, a two-arguments function, is, indeed, a function on the same domain (or totality), as a one-argument function of the same level, and not a function on pairs of elements of this domain.

Frege took this to be the case also of the symbol ' ', used to form statements, whose vertical stroke is called 'judgementstroke [Urtheilstrich]' by him ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], § I.5;[START_REF] Frege | Basic Laws of Arithmetic[END_REF], p. 91).

Note that, in our notation, the occurrence of the horizontal stroke before the vertical one, in ' ', can be disregarded.

Note, also, that requiring that θ and τ be FGGPLR terms entails requiring that these terms present at least one occurrence of the symbol ' --' such that no part of such a term falls outside its scope. So, whereas θ and τ can, for example, stand for 'Γ', '¬Γ' and 'Γ ⇒ ∆', they cannot stand for '¬Γ' and 'Γ ⇒ ∆'.

Note, again, that, according to this stipulation, and to stipulation St Is.T [FGGPL R ] , any FGGPLR particular statement is an instance of itself: cf. footnote 30, above.

Frege makes his replacement rules explicit only with respect to Roman letters ([START_REF] Frege | Grundgesetze der Arithmetik[END_REF], § I.48.9). He clearly applies, however, analogous rules also to upper-case Greek letters.

The dot placed after '/', both in ' [θ/.θ]' and in ' [θ/.θ]' is intended to signal that the replacement is not to be done for all the occurrences on the relevant term, but for some of its occurrences (possibly for only one of them, possibly for several, possibly for all). Note also that here, as well as in all the following rules, it applies the same notational convention spelt out in footnote 32. So, whereas θ can stand, for example, for 'Γ', '¬Γ' and 'Γ ⇒ ∆', it cannot stand for '¬Γ' and 'Γ ⇒ ∆'. Hence, whereas this rule implies, for example, that from 'Λ ⇒ Θ', it follows 'Λ ⇒ Θ', from 'Γ ⇒ ∆ ⇒ Θ', follows 'Γ ⇒ ∆ ⇒ Θ', and from '¬Γ ⇒ ∆' follows '¬Γ ⇒ ∆', it implies neither that from 'Γ ⇒ ∆ ⇒ Θ', follows 'Γ ⇒ ∆ ⇒ Θ', nor that from '¬Γ ⇒ ∆' follows'¬Γ ⇒ ∆', and, indeed, neither 'Γ ⇒ ∆ ⇒ Θ', nor '¬Γ ⇒ ∆' are FGGPLR terms. It follows that θ is nothing but what stands under the symbol ' --' in θ.

In stating this rule, we could have omitted both ' -→ κ2 ⇒' and '⇒ -→ κ3', without any relevant consequence for its deductive strength. Some of the inferences that the rule, as we state it, licences in only one step, would be, indeed, also licensed by the rule so simplified in several reiterated steps. We state the rule as we do only for sake of perspicuity. Mutatis mutandis, the same also holds for the rules Rl PS [FGGPL R] . iv-viii

Concerning this stipulation, cf.[START_REF] Heck | Reading Frege's Grundgesetze[END_REF], pp. 60-64.

Note that, according to this stipulation, any FGGPLR general statement is an instance of itself, just as it happens for FGGPLR particular statements: cf. footnotes 30 and 33, above.

This raises the problem of the role of Basic Law IV in Frege's system. The question is quite delicate and we cannot enter it, here. We simply refer the reader to Landini's subtle scrutiny of it, leading to the conclusion that this role only appears in a larger context, involving both the whole FGGBS and the definition of natural numbers within it, namely the proof of (Frege's version of) Hume's principle: cf.[START_REF] Landini | Frege's Notations: What They Are and How They Mean[END_REF], § § 2.4, 2.7, and 4.3.

Here 'µ' is intended to hold a place open for the arguments of this third-level function. The double occurrence of 'δ' is intended to mean that the argument-place of a second-level function providing this argument is not held open, instead. Though third-level functions play an essential role in FGGBS because the second-order universal quantifier is such a function, Frege did neither emphasise this role, nor explicitly mention these functions. As a consequence, neither the symbols 'Υ' and 'δ' nor any other symbol playing the same role as them enter his formal language.

Note that here the symbol '=' pertains to the function ξ = ζ, not to the function ξ = ζ involved in the extension of FGGPLR considered in § 3.6.

Cf footnote (52) above.

The reason for proceeding this way, by first extending Tn and F [i,j] n an then taking away these same families from their extensions is, of course, that FGGL2R terms and function-names enter the process of generation of FGGL2R object-and function-markers at any step.

On Basic Laws IIa and IIb, cf. footnote 64, above.

Terms and Particular Statements

All this being said, it is now time to leave any preliminary apart and proceed to fix the system FGGL2 R , by beginning with fixing its terms. The best way to do it is not by stating the clauses according to which the elements of a certain formal language, intended as a collection of atomic symbols having a certain arity, can be composed with each others so as to get such a term, as we have done for FGGPL R terms. It is much more appropriate to identify these terms with the elements of a stratified family T of strings of symbols generated step by step according to a codified procedure involving six other stratified families F [i,j] (i = 1, 2; j = 1, 2, 3) of strings of symbols, also generated step by step according to this same procedure, which are intended to include, in turn, names of functions respectively belonging to F [i,j] . What is to be done is, then, to describe this procedure and the way in which the families T, F [i,j] are progressively constituted according to it.

To this purpose, let us look at each of these families as the indefinite union of the sub-families of its strings which are generated at the different steps of the procedure. More precisely, let us set that T = ∞ n=0 T n and

n , where, for any n, T n and F [i,j] n are, respectively, the sub-families of T and F [i,j] including the strings generated at step n. Supposing that C is any collection of symbols, let us, then, call 'C string' a string of symbols composed only by symbols belonging to C, and focus, in particular, on the collection C T [FGGL2 R ] = {a i , f i , (, ), --, ¬ --, --⇒ --, =, ∀} (i = 1, 2, . . .). Let us also admit that, for that which pertains to the functions ¬ξ and ζ ⇒ ζ (and their values, or the relative FGGL2 R Roman object-or function-markers : cf. string: cf. § 4.4.2, below) within another such string meets the same conditions informally explained in § 3.2 for FGGPL R object-letters or terms, together with the two other following ones: if '∀a i θ' and '∀f i θ' are such a string (for any i), then the sub-string θ occurs in them, whereas θ does not. This having been stated, let us stipulate that:

strings, and T 0 = ∅;

∪ {ξ} strings, within which 'ξ' actually occurs at least once, and

∪ {ξ, ζ} strings, within which 'ξ' and 'ζ' actually occurs at least once each, and

56 Another thing to be noted is that, in this way, a term can be generated in several different ways starting from other terms, which is different from what happens in modern systems of logic.

57 Parentheses in '(ξ) = (ζ)' are used to avoid any ambiguity relative to the scope of '='. If no ambiguity is possible they can be omitted.

St F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] [FGGL2 R ] F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] only includes C T [FGGL2 R ] ∪ {ϕ} strings, within which 'ϕ' actually occurs at least once and always within a sub-string ϕ(ϑ) 58 , where ϑ is a C T [FGGL2 R ] string 59 , and

F [2,2] only includes C T [FGGL2 R ] ∪ {ϕ} strings, within which 'ϕ' actually occurs at least once and always within a sub-string ϕ(ϑ, ϑ ), where ϑ and ϑ are C T [FGGL2 R ] strings, and

Both F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]3] and F [2,3] only include one string each, namely F [START_REF] Blanchette | Frege's Conception of Logic[END_REF]3] =

, and F [2,3] =

These families having been so described, in general, in order to describe the procedure allowing to generate the strings that are to be included in them, besides those included in 3] 0 , one has to clarify Frege's notion of a name forming a part of another name (cf. p. 31, above).

St

Fr.Pt.(T,F)

If, for any n, τ and υ are two strings respectively included in T n and F No other case is to be considered in order for us to proceed with our description. Let us fix, now, the way the strings included in T n+1 , F

at step n + 1 of the procedure, for any n. This is done through the following stipulations, where we write, for short, 'T 0→n ' and 'F [i,j] 0→n ', respectively for '

58 For the sake of simplicity, again, in the present section, we follows a policy analogous to that followed in section 3, above concerning meta-variables (cf. footnote 29, above): we take the liberty of using some meta-variables intended to range over C T [FGGL2 R ] ∪ {ξ, ζ, ϕ, µ, β, γ} strings, in order to form other strings of symbols involving, together with these meta-variables, also some symbols of this same collection. In this case, we assume, anew, that these last symbols refer to themselves as symbols of the object-language, and avoid any use of quotation marks.

59 Note that this is not the same as requiring that ϑ is included in T, since it is not only obvious that T does not include any

string, but also that some of the C T [FGGL2 R ] strings, that are not included in T could play the role of ϑ in the present condition. To take a simple example, 'a1' is a C T [FGGL2 R ] string but is not included in T, and 'ϕ (a1)' is a rightful instance of ϕ (ϑ).

60 These two families of strings, including a string each, could, in fact, be eliminated without any consequence on the procedure of the generation of terms and of function-names. We include them here only for sake of completeness, since the strings they include are names of the two second-order quantifiers.

forms a part of τ through ϑ i and ϑ i 61 ;

St

A string of symbols θ to be included in

n+1 is generated at step n + 1 if and only if θ results from a string τ included in T 0→n by respectively replacing in it some (possibly all) occurrences of some

where n is whatever natural number) with ϕ(ϑ i , ϑ i ), provided that ϑ i and ϑ i be some

∪ {ξ, ζ} string υ (the same for any value of i) forms a part of τ through ϑ i , ϑ i and ϑ i 62

These stipulations having been stated, we can now formalise, what we have informally announced above:

n , for some n (i.e., it is included in F [i,j] ).

These two last stipulations, together with the previous ones concerning the strings to be included in T n and F [i,j] n (i = 1, 2: j = 1, 2, 3) implicitly fix the rules according to which the symbols of C T [FGGL2 R ] ∪ {ξ, ζ, ϕ, µ, β, γ} have to be composed to give rise to FGGL2 R terms and function-names, by also determining their arity. It follows that these stipulations transform this collection in a formal language. Let L T,FN

be this language.

The stipulations concerning the strings of symbols to be included in

), together with the definitions of the basic functions entail that the function-names that are allowed to be formed within this language do not necessarily designate a function with values in {T, F}, that is, a concept or a relation, in Frege's parlance. A simple example is given by the one-argument first-level function ξ (namely the one-argument identity function, whose value is the same object as its argument, for whatsoever argument), whose name is included in

2 , since it is obtained, according to stipulation St

(and working as υ in this stipulation). It does not follow, however, that FGGL2 R terms include names of objects other than the truth-values. To obtain such a term from this last function, as a name of a value of it, one should already have this same term available among FGGL2 R terms, and, mutatis mutandis, the same happens for any other FGGL2 R function-name (either for those that designate a concept or a relation or for 61 Let us suppose that, in this clause, one takes τ and υ to be, respectively, '∀a1a1 ⇒ ∀a2a2 ⇒ ∀a2a2' and 'ξ ⇒ ∀a2a2', and i = 1.

One can, then, take ϑ1 to be '∀a1a1 ⇒ ∀a2a2 ⇒ ∀a2a2', so that ϑ 1 will be '∀a1a1 ⇒ ∀a2a2' and θ will be 'ϕ(∀a1a1 ⇒ ∀a2a2)'.

But one might also take ϑ to be '∀a1a1 ⇒ ∀a2a2', so that ϑ will be '∀a1a1' and θ will be 'ϕ (∀a1a1) ⇒ ∀a2a2'. Note that, though both these two options are allowed, one cannot begin by the first one, so as to get 'ϕ(∀a1a1 ⇒ ∀a2a2)' and then observe that the C T [FGGL2 R ] ∪ {ξ} string 'ξ ⇒ ∀a2a2' occurs again within this function-name and then apply anew the same clause to get 'ϕ `ϕ(∀a1a1) ´', since this clause only allows one to get function-names from FGGL2R terms, and not from other function-names. More generally, no string ϕ(θ), such that 'ϕ' occurs in θ can be generated according to this or any other of our clauses. No such string is, then, a function-name admissible in FGGL2R. This agrees with Frege's rejection of direct composition of functions.

62 Here also, one can have different possible choices for the application of this clause on two given strings taken as τ and υ, as in the case of clause St

: cf. footnote 61, above. 63 It is easy to verify that, according to this stipulation, any FGGL2R term is a particular term, just as it happens with FGGPLR terms, as observed above, p. 22.

application to the former statements of the rule Rl GS [FGGPL R ] . vi. To account for Frege's simple argument, one then has to, either admit a formal (though preliminary) use of FGGPL object-letters and of analogous function-letters within FGGL2 R , or to look for a way other than that involved in FGGPL of conceiving the relation of being an instance of, on FGGPL well-formed formulas, and the corresponding rule of substitution. If the former option is discarded (in agreement with what was said above), then the latter only remains, which means that, within FGGL2 R , this relation and this rule are to be fixed by directly appealing to Roman letters.

Frege gave an hint about how to do this when he introduced the notions of a Roman object-marker and of a Roman function-marker ( [18], § § I.17 and I.26; [22], pp. 33 1 and 44 1 ). We have already appealed to the former in § 3.3.2 (p. 24), and explained it by having recourse to FGGPL R object-letters. Still, if these letters are no longer available, this explanation cannot be maintained. In § I. 26 Frege defined these markers as that which "we obtain", if "we replace", respectively in an object-and in a function-name, object-names and function-names that "form a part" of the former names with appropriate Roman letters. Though apparently quite simple, this definition is, in fact, far from clear, when it is transposed in FGGL2 R . Clarifying it requires fixing a new generating procedure for FGGL2 R Roman object-and function-markers (or merely FGGL2 R object-and function-markers, for short), parallel to the one expounded above for FGGL2 R terms and function-names. This is what we shall do in the next § 4.4.2. Before doing it, some other examples are in order to help in understanding both the nature and role of FGGL2 R object-and function-marker and the way this generating procedure works.

Consider the general statement ' a = a' 66 . If one replaces 'a' with any object-name 'Γ', one gets ' Γ = Γ', which is a particular statement. But one can also replace , which allows a FGGPL R general statement to be an instance of another such statement. A difference with the case of FGGPL R is, instead, that within FGGL2 R , general statements also admit instances provided by particular statements, so that the latter can follow from the former. For example, the particular statement ' ∀a 1 a 1 = ∀a 1 a 1 ' is an instance of ' a = a', and follows from it. Another difference is that, within FGGL2 R , general statements can also involve Roman letters for functions. These work as Roman letters for objects, but indicate functions, rather than objects. Among them, there are the letters 'f ', used to indicate first-level functions, and 'M ', used to indicate second-level functions. For example, ' f (a) = f (a)', ' f (∀aa) = f (∀aa)', and '

general statements involving these letters. Now, like FGGPL R object-markers are components of FGGPL R general statements, FGGL2 R objectmarkers are components of FGGL2 R general statements. In particular, the FGGL2 R general statements ' a = a' and '

It is, then, enough to consider that 'f (a)', 'f (∀aa)' and '∀f 1 M β (f 1 (β))' are all instances of 'a' to conclude that all these last three statements are instances of ' a = a', and follow from it.

It is, moreover, enough to consider that the FGGL2 R term '∀aa = a ⇒ ∀aa' is, in turn, an instance of the FGGL2 R object-marker 'f (∀aa)', to conclude that the FGGL2 R particular statement ' ∀aa = a ⇒ ∀aa = ∀aa = a ⇒ ∀aa' is an instance of ' f (∀aa) = f (∀aa)', and follows from it. To get this term from this

FR [START_REF] Blanchette | Frege's Conception of Logic[END_REF][START_REF] Blanchette | Frege's Conception of Logic[END_REF] only includes C OM [FGGL2 R ] ∪ {ξ} strings, within which 'ξ' actually occurs at least once, and

∪ {ξ, ζ} strings, within which 'ξ' and 'ζ' actually occurs at least once each, and FR

FR [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] only includes C OM [FGGL2 R ] ∪ {ϕ} strings, within which 'ϕ' actually occurs at least once and always within a sub-string ϕ(ϑ), and FR

FR [2,2] only includes C OM [FGGL2 R ] ∪ {ϕ} strings, within which 'ϕ' actually occurs at least once and always within a sub-string ϕ(ϑ, ϑ ), where ϑ and ϑ are C T [FGGL2 R ] strings, and

As we have just said, the strings included in TR n+1 , FR

at step n + 1 of the procedure, for any n, in the same way as for the families

n+1 . So, to fix the relevant procedure, it is enough to repeat stipulations St

, by replacing in them all occurrences of 'R' with 'TR', all occurrences of 'F' with 'FR', and all occurrences of 'C T

', so as to get the new stipulations St ] . This enables us to define FGGL2 R object-and or function-markers as we have announced:

string is an FGGL2 R object-marker if and only if it is included in the family TR but not in T;

∪ {ξ, ζ, ϕ} string is an FGGL2 R function-marker if and only if it is included in one of the families FR [i,j] (i; j = 1, 2), but in none of the families F [i,j] .

We are now able to define the relation of being an instance of, on FGGL2 R terms and object-markers 70 : 69 The ellipses here and in the previous stipulation St FR [START_REF] Blanchette | Frege's Conception of Logic[END_REF]2] [FGGL2 R ] stand for the same strings that precede them, in which 'M ', 'β', 'γ' are endowed with appropriate indexes. Hence, indexation apart, the strings 'M β (ϕ (β))', . . . and 'M β,γ (ϕ (β, γ))', . . . , respectively added to F and F [2,3] , by omitting '∀f1' and replacing 'µ' with 'M ', which corresponds to pass from a way to express generality to another. This is another reason that suggested us to include the families . i, which we shall introduce in section 4.6 below, the following stipulations St Is.T [FGGL2 R ] and St Is.OM,T [FGGL2 R ] i-vi render, with some slight differences and a more important generalisation, Frege's rules 9 and 10 of § I.48, namely the rules of citation of statements relative to replacement of Roman and Gothic letters, respectively. The generalisation depends on the possibility, licensed by stipulations St Is.OM,T [FGGL2 R ] v -vi, of replacing FGGL2R general letters for second-level functions with appropriate function-names in whatever FGGL2R object-markers and general statements in which such a letter occurs, which contrasts with Frege's licensing this replacement (through his rule 9 of § I.48) only in Basic Law IIb (cf. § 4.6, below). This restriction depends, indeed, on no intrinsic necessity relative to FGGBS, and is merely motivated by the fact that no other such replacement is necessary to perform the derivation included in Frege's treatise. . iii, then:

These rules are rules of transformation of FGGL2 R well-formed formulas, and are close to the modern rules of first-and second-order universal generalisation respectively. They render Frege's rule of "transformation of a Roman letter to a Gothic letter"( [18], § § I.17, I.20 and I.48.5; [22], pp. 32 1 , 35 1 , and 62 1 ).

At this point, one can proceed just as for FGGL2 R particular statements, and generalise the relation of following from, so as to allow a FGGL2 R well-formed formula to follow from any number of such formulas, and fix the notion of a theorem of FGGL2 R in the obvious way: . i-viii, any theorem of FGGPL R is also a theorem of FGGL2 R . Hence, insofar as FGGPL R is complete, and FGGL2 R is clearly sound, the latter can be taken as a conservative extension of the former, though we have not come to it by mere extension. This apparently cumbersome situation depends on FGGPL R including as its well-formed formulas only its general statements, which do not include terms, in turn, whereas the essential difference between FGGPL R and FGGL2 R is just concerned with the generation of terms.