On defining the notion of complete and immediate formal grounding

The aim of this paper is to provide a definition of the the notion of complete and immediate formal grounding through the concepts of derivability and complexity. It will be shown that this definition yields a subtle and precise analysis of the concept of grounding in several paradigmatic cases.

Introduction

Consider the following sentences:

1. In Europe well-functioning thermometers are higher in summer than in winter because in Europe it is warmer in summer than in winter.

2. The action is wrong because it was performed with the sole intention of causing harm.

3. The ball is red and round because the ball is red and the ball is round.

Each of these sentences contains the expression because and each of them can be divided into an antecedent, i.e. what comes after the because ("in Europe it is warmer in summer than in winter", "the action was performed with the sole intention of causing harm" and "the ball is red and the ball is round"), and a consequent, i.e. what comes before the because ("in Europe well-functioning thermometers are higher in summer than in winter", "the action is wrong", "the ball is red and round", respectively). In each case not only can we say that the consequent is entailed by the antecedent, but also, and more importantly, that the consequent is determined or explained or accounted for the antecedent. In other terms, in each of the sentences listed above, the antecedent constitutes a reason for or a ground of the consequent.

Sentences 1-3 are sentences standardly used to exemplify the concept of grounding, a concept that has been the subject of increasing interest in the contemporary philosophical and logical literature (e.g. [START_REF] Correia | Grounding and truth-functions[END_REF][START_REF] De Rosset | What is weak ground? Essays in Philosophy[END_REF][START_REF] Fine | Some puzzles of ground[END_REF][START_REF] Litland | On some counterexamples to the transitivity of grounding[END_REF][START_REF] Rumberg | Bolzano's theory of grounding against the background of normal proofs[END_REF][START_REF] Schnieder | A puzzle about 'Because[END_REF]). Grounding is often described as an objective relation that is explanatory in nature. The relata of this relation are, for some authors, truths, for others, facts (e.g. see [START_REF] Correia | Grounding: an opinionated introduction[END_REF]); in this paper we take grounding to be a relation amongst truths. 1The linguistic expression because represents one way of conveying the grounding concept; another common way of conveying it is given by the expression in virtue of.

Several scholars have stressed the importance of the grounding concept for philosophical inquiry. Correia and Schnieder [START_REF] Correia | Grounding: an opinionated introduction[END_REF] clearly state that "it is a phenomenon of the highest philosophical importance"; Fine [START_REF] Fine | Guide to ground[END_REF] goes even further and claims, "Once the notion of ground is acknowledged, then I believe that it will be seen to be of general application throughout the whole of philosophy." This paper aims to contribute to the debate concerning this notion.

Our starting point will be a distinction, first introduced by a pioneer in the study of grounding -the Bohemian thinker Bernard Bolzano -between material and formal grounding. In [3, §162, p. 257] Bolzano defines the distinction between formal and material grounding by exploiting his famous concept of variable-ideas. In this paper, following the tradition in contemporary logic, we rather take formal grounding to be grounding in a logical sense, material grounding being the complement of formal grounding. Thus, according to our distinction, sentences 1 and 2 are examples of material grounding, while sentence 3 is an example of formal grounding.

In this paper we do not aim to analyze both material and formal grounding; rather, we will restrict our attention to the concept of formal grounding. Our goal is to give a definition of this notion. This goal, we claim, is both original and important. On the one hand, the recent literature on grounding contains discussions of the properties that grounding satisfies (e.g. see [START_REF] De Rosset | What is weak ground? Essays in Philosophy[END_REF][START_REF] Litland | On some counterexamples to the transitivity of grounding[END_REF]) or of the very existence of the notion of grounding (e.g. see [START_REF] Daily | Scepticism about grounding[END_REF]), but, as far as we know, little has been said on how to define such a concept (Bolzano [START_REF] Bolzano | Theory of Science: A Selection, with an Introduction[END_REF] represents a notable exception to this trend and we will actually rely on some of his intuitions). On the other hand, not only does it seem crucial per se to have a definition of formal grounding, but also, such a definition could offer new perspectives on how to develop a logic of formal grounding.

The paper will be organized as follows. In Section 2 we will introduce classical logic as the background framework of our research and then investigate the relationship between the classical notion of derivability and formal grounding. Section 3 will serve to present the concept of complete and immediate formal grounding that will be the specific object of our study; in Section 4 we will examine the relationship between grounding and complexity and introduce a precise definition of complexity. Section 5 will be used to analyze the case of disjunction and argue for the need for another element, other than derivability and complexity, in the definition of formal grounding. In Section 6 we will finally state our definition of complete and immediate formal grounding. In Section 7 we will outline some differences between our approach to the concept of grounding and the most prominent approaches (see [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | The pure logic of ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF]) in the contemporary literature. Finally, in Section 8, we will draw some conclusions and sketch some directions for future research.

Classical logic, derivability and formal grounding

In what follows classical logic will be the framework in which we will study the notion of formal grounding.

Definition 2.1. The language L c is composed of a denumerable stock of propositional atoms (p, q, r, . . . ), the logical operators ¬, ∧ and ∨ and the parentheses (, ). Formulas are constructed as usual and the set of well-formed formulas of L c is denoted by F.

Semantically, classical logic is defined by means of the standard truth-tables containing the two truth values, truth and falsity. Syntactically, by relying on the means of a formal system (e.g. see [START_REF] Troelstra | Basic Proof Theory[END_REF]), the notion of classical derivability can be easily introduced and, following the common usage, be denoted by the symbol . More precisely, we will write M A for: there exists a derivation from the multiset2 of formulas M to the formula A. The notion of classical derivability will be central throughout the paper.

Here we are interested in understanding the link between classical derivability and formal grounding. At the first glance, these concepts seem to be closely connected. But what is the exact nature of their relationship? Certainly, if A is derivable from the multiset of formulas M , it does not follow that M formally grounds A. To see this, consider the case of conjunction. While A is derivable from A ∧ B, nobody would ever say that A ∧ B is the formal ground of A. What about the inverse then? If M formally grounds A, does this imply that A is derivable from M? Intuitively, the answer seems to be affirmative: it is difficult to imagine a case of formal grounding where the conclusion is not derivable from its premises. Note, moreover, that there exists a significant volume of literature (e.g. see [START_REF] Berg | Bolzano's Logic[END_REF][START_REF] Buhl | Ableitbarkeit und Abfolge in der Wissenschaftstheorie Bolzanos[END_REF][START_REF] Casari | Matematica e verità[END_REF][START_REF] Rumberg | Bolzano's theory of grounding against the background of normal proofs[END_REF]) dedicated to the assimilation of normal derivations of classical logic with formal grounding proofs and that, by doing so, assume, directly or indirectly, that formal grounding is nothing but a particular sort of classical derivability. Finally, an explicit association between derivability and formal grounding can also be found in Bolzano [3, §162, p. 257], even if Bolzano used the terms formal and derivable in a different, though related and compatible, way from ours. In the light of these observations, we can reasonably claim that formal grounding is indeed a special type of derivability; in other words, formal grounding is grounding amongst truths that are also derivable. This claim is extremely important for our project. Indeed, if we seriously think that formal grounding is a special sort of classical derivability, then the task of defining formal grounding amounts to that of finding those criteria distinguishing, among the relations of classical derivability, those which constitute relations of formal grounding from those which do not. The following sections will be dedicated to this task.

We can summarize this section with the following general picture: the background framework of our research is constituted by classical logic, its two truth values and a notion of derivability which typically formalizes proofs by means of which we demonstrate that something is true. On this basis, by imposing certain specific and adequate criteria, we aim to draw out a notion of formal grounding that deals only with truths and that is supposed to represent proofs by means of which we demonstrate why something is true.

Complete and immediate grounding

According to what we have said in the previous section, in the search for a definition for the notion of formal grounding, our starting point should be the classical notion of derivability. Now a derivation is usually seen as a tree in which every edge corresponds to an inferential step. Likewise, even a formal grounding proof can be seen as a (special) tree (see [START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF][START_REF] Paoli | Bolzano e le dimostrazioni matematiche[END_REF][START_REF] Rumberg | Bolzano's theory of grounding against the background of normal proofs[END_REF][START_REF] Tatzel | Bolzano's theory of ground and consequence[END_REF]) in which every edge corresponds to a single grounding step. We are going to call the single grounding step of a grounding tree immediate grounding. Mediate grounding is usually taken to be the transitive closure of the relation of immediate grounding. Thus, every truth occurring in a grounding tree, looking at the tree from the bottom upwards, is a mediate ground of the tree root. This terminology has been firstly introduced by Bolzano [START_REF] Bolzano | Contributions to a more well founded presentation of mathematics[END_REF] and then taken up (with slight modification) by Fine [START_REF] Fine | Guide to ground[END_REF].

The immediate-mediate distinction is not the only one that we can make concerning the concept of (formal) grounding. There is another central distinction to be drawn which appears to correspond to what Bolzano called complete and partial grounding and which is related to what is referred to nowadays as the difference between full and partial grounding.

According to Fine [START_REF] Fine | Guide to ground[END_REF] A is a partial ground of C if A on its own or together with some other truths is a ground of C. Thus, given that A and B are the full ground of A ∧ B, each of A and B will be a partial ground of A ∧ B. The notion of full ground is never explicitly defined but it is suggested that A is a full ground of C if the truth of A is sufficient to guarantee the truth of C. Bolzano's distinction between complete and partial ground is slightly different. Following the analysis of Sebestik [START_REF] Sebestik | Logique et mathematique chez Bernard Bolzano[END_REF] and Tatzel [25, p.13], for Bolzano the (multi)set of all, and only, those truths each of which contributes to ground the truth C is a complete ground of C. On the other hand, each of the truths that compose the complete ground of C is said to be a partial ground of C.

It seems that Bolzano and Fine are both aiming at the same -or at the least very similar -distinction, although the way they draw the line between the two concepts is different. For Fine a partial ground of a truth C can also be a full ground of C, while for Bolzano this can never be the case, since partial and complete grounds are two disjoint concepts [3, §198, p. 268]. Moreover, while for Fine, the full ground of a truth C does not need to correspond to the (multi)set that gathers together all and only the truths that ground Cfor Fine full ground is just a sufficient condition -for Bolzano this is precisely what characterizes the complete ground of a truth C. Note moreover that this difference between complete and partial ground and full and partial ground is directly linked to different viewings on the uniqueness of grounding. While Bolzano aimed to investigate the complete grounds of a truth, Fine concentrates on the concept of a full ground of a truth.

In what follows we will focus on the notion of complete and immediate formal grounding in the Bolzanian sense; the precise goal of this paper will be to give a definition of it. This restriction to what might seem a narrow object of study is actually a common strategy in the literature. Indeed, this is very close to Bolzano's own approach: he took the concept of complete and immediate formal grounding as central and thought this was the concept to be characterized first. The definitions of the other concepts would have followed as consequences (see [START_REF] Tatzel | Bolzano's theory of ground and consequence[END_REF]).

Fine expresses a similar attitude. On the one hand he claims that The agreement of these two illustrious philosophers on the centrality of the concept of complete and immediate grounding is a very good reason for focussing on this notion.

Complexity and complete and immediate formal grounding

Let us now get at the heart of the matter and consider what conditions are needed to pass from classical derivability to the concept of formal grounding.

In particular, since we focus on the notion of complete and immediate formal grounding, we will have to find those conditions that allow us to pass from a singular inferential step to the concept of complete and immediate formal grounding.

In the past as well as in the recent literature on grounding, one of the oft noted characteristics of this notion is complexity (e.g. see [START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF][START_REF] Casari | Matematica e verità[END_REF][START_REF] Correia | Logical grounds[END_REF] ). Bolzano was the first to explicitly claim that in a formal (in his sense of formal, see Section 2) grounding relation the grounds cannot be more complex than their conclusion (e.g. [3, §221.2, p. 288]) 3 . In none of [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF] is it ever the case that a truth B is grounded by a truth A which is more complex than B. Thus, seemingly, we can assume that in a formal grounding chain, complexity decreases as one goes from the conclusion to its grounds. In particular, in the case of complete and immediate grounding, the grounds must be completely and immediately less complex than their conclusion. But what exactly does being completely and immediately less complex mean? Can we have a precise definition of this notion? While intuitively it might seem easy to decide when a truth is (completely and immediately) less complex than another, to draw the formal counterpart of such a notion is not straightforward. The rest of the section will be dedicated to this task. The result will play a crucial role in our definition of complete and immediate formal grounding.

Anyone who is acquainted with classical logic will certainly know that in this framework there already exists a way of associating to a formula A a number representing its complexity, and a notion, that of subformula, that might be seen as describing the relation of being less complex. So one might think that we actually already have the tools needed for a definition of being completely and immediately less complex. In order to avoid any confusion, let us present these two notions and then explain why, in fact, they do not work in the grounding framework. This will also shed light on the features required from a notion of being completely and immediately less complex that is appropriate for grounding.

Definition 4.1. The complexity of a formula A, cm(A), is inductively defined in the following way:

-cm(p) = 0 -cm(¬A) = cm(A) + 1 -cm(A • B) = cm(A) + cm(B) + 1 4
Thus the complexity of a formula is measured by counting the occurrences of its logical connectives. Definition 4.2. A is a subformula of B if, and only if, one of the following holds:

-A = B -B = ¬C and A is a subformula of C -B = (C • D) and A is a subformula of C or a subformula of D
Given these two definitions it seems straightforward to define the notion of being completely and immediately less complex in the following way. Definition 4.3. In the classical logical framework, a multiset M is completely and immediately less complex than a formula C if, and only if: Figure 1: Three grounding principles which are generally accepted in the literature, (e.g. (see [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF])).

-{A} is the full (or complete) and immediate grounds of ¬¬A -{A, B} is the full (or complete) and immediate grounds of A ∧ B -{¬A, ¬B} is the full (or complete) and immediate grounds of ¬(A ∨ B)

-C = ¬B and M = {B}, or -C = B • D and M = {B, D}
This seems to be a very natural way to define the novel notion of completely and immediately less complex, in the light of the well-known notions of complexity and subformula that have been introduced above, see Definitions 4.1 and 4.2 respectively. The multiset M is less complex than the formula C since cm(M ) < cm(C) (where cm(M ) is the sum of the complexities of its members). The multiset M is immediately less complex than the formula C since it contains only subformulas that can be immediately obtained from the formula C by removing its main connective. The multiset M is completely less complex than the formula C since it contains all subformulas that are precisely at one level below the formula C.

The question now is: does Definition 4.3 work in the grounding framework? In order to answer this question, let us point out the virtues of this Definition before turning to its problems. As for the virtues, in the case of (certain) conjunctions and disjunctions, it seems to work fine. (Let us call this virtue V.) Consider for example the formula p ∧ q (the case of a disjunctive truth can be treated anagously). According to Definition 4.3 the multiset {p, q} is completely and immediately less complex than p ∧ q; since p, q are standardly (see Figure 1) taken to be the complete and immediate formal grounds of p∧q, this is precisely what we would like to have.

As for the problems, they are three. The first (we will call it P1) concerns conjunction and disjunction. We will illustrate this problem with a formula in conjunctive form. Analogous examples can provided with formulas in disjunctive form. Consider a formula of the form (p∧q)∧r. Then it seems that we would like to claim that, not only the multiset {p ∧ q, r} is completely and immediately less complex than (p ∧ q) ∧ r, but that also each of the multisets {q ∧ p, r}, {r ∧ p, q}, {p ∧ r, q}, {q ∧ r, p}, {r ∧ q, p} is completely and immediately less complex than (p ∧ q) ∧ r. Of course Definition 4.3 does not allow us to draw such a conclusion.

The other two problems linked with Definition 4.3 concern negation. Consider for example the formulas A and ¬¬A: A is taken to be (see Figure 1) the complete and immediate formal ground of ¬¬A, thus it also needs to be completely and immediately less complex than ¬¬A; however, according to Definition 4.3, it is ¬A, and not A, that is completely and immediately less complex than ¬¬A. (We will call this problem P2.) A similar situation arises with ¬(A ∨ B): ¬A, ¬B are considered (see Figure 1) the complete and immediate formal grounds of ¬(A ∨ B), thus they also need to be completely and immediately less complex than ¬(A ∨ B); however, according to our definition, it is A ∨ B that is completely and immediately less complex than ¬(A ∨ B). (We will call this problem P3.)

Given this situation, we can conclude that Definition 4.3, which draws naturally upon Definitions 4.1 and 4.2, does not work in the grounding framework. Thus we need an alternative notion that has the same virtue V as Definition 4.3, but that overcomes problems P1 -P3. In order to achieve the desired result, we will proceed in three steps (that are analogous to those that we have just seen in the classical framework): we will introduce a new way of measuring the complexity of a formula A that is adequate for the grounding framework; then, we will explain what counts as a subformula A of a formula B in the grounding framework. Finally, by exploiting the first two notions in a way analogous to that seen above, we will define the notion of being completely and immediately less complex in the grounding framework.

We start by defining a notion of complexity appropriate for the grounding framework.

Definition 4.4. The g-complexity of a formula A, gcm(A), is defined in the following way:

-gcm(p) = gcm(¬p) = 0 -gcm(A • B) = gcm(¬(A • B)) = gcm(A) + gcm(B) + 1 -gcm(¬¬A) = gcm(A) + 1
So now we have two different ways of counting the complexity of a syntactic object A ∈ F of the language L c : the first way, introduced in Definition 4.1, is simply called complexity, the second way, introduced in the definition above, is called g-complexity, for grounding complexity. These two notions are two different technical devices, two different mechanical ways of counting the complexity of a syntactical object A ∈ F and, as such, they could be just taken for granted without any further explanation. Nevertheless we are led to think that each of these notions is in its respective context (i.e. a classical context on the one hand, and a grounding context on the other hand) very natural and therefore should be preferred over the other imaginable measures of complexity of the object A ∈ F. We will now clarify the reasons behind this claim; this will shed light on both notions of complexity.

Let us start by analyzing the standard notion of complexity of a formula. According to Definition 4.1, the complexity of a formula is calculated by systematically counting the occurrences of its logical connectives. Thus the complexity of the formula ¬A corresponds to the complexity of A plus one; the complexity of A ∧ B corresponds to the complexity of A plus the complexity of B plus one, and so on. A prominent reason why this is the natural definition of complexity for classical logic is that this logic is concerned with propositions, and the relations between formulas which are "counted" in this definition track those between propositions. The formula ¬p is constructed from the formula p by the addition of a connective, just as the proposition expressed by the formula ¬p can be obtained from that expressed by p by the application of the operation of negation. Counting the former formula as of a complexity one greater than the complexity of the latter formula thus seems to correctly capture the appropriate aspect of the relationship between the propositions. Analogously, the construction of the formula A ∧ B from the formulas A and B mimics the operation on propositions that would yield the proposition expressed by A ∧ B from those expressed by A and B, and Definition 4.1 reflects this.

Things are different when we move to the grounding framework, for grounding, as we noted above, is concerned entirely with truths. Accordingly, the appropriate notion of complexity should track relationships among the truths expressed by the formulas if they were true. We suggest that the notion of gcomplexity does just this. As concerns conjunction and disjunction, it coincides with the classical notion of complexity. If A and B express truths, then the truth expressed by A ∧ B is obtained from the previous truths using a single operation, just as the formula A ∧ B is constructed from the formulas A and B using a single connective. Counting the connective in this case (as in Definition 4.4) is faithful to the relationships of interest among truths. However, this is not so for the case of negation. Since (at most) one of p and ¬p will express a truth, the relationship between the pair of formulas p and ¬p cannot correspond to any relationship between a pair of truths. From the point of view of grounding, which deals solely in truths, this relationship between formulas is irrelevant: only one of the formulas will ever be an object of the grounding framework. In this framework, there thus seems to be no reason to count ¬p as more complex than p. Indeed, since only one of them will express a truth, and the other the corresponding falsehood, it would seem most sensible to count them on the same level, when formulating a notion of complexity that tracks relationships between truths. This is precisely what Definition 4.4 does, by setting the complexity of both p and ¬p at 0.

Analogous reasoning can be applied to the g-complexity of more complex formulas like ¬(A ∧ B) or ¬(A ∨ B). Even in these cases, since only truths have a role, we can no longer claim, as in the classical case, that their complexity is equivalent to cm(A ∧ B) +1 and cm(A ∨ B) + 1, respectively; instead, their complexity will be the same as the complexity of A ∧ B and A ∨ B, respectively.

Let us then move to the case of double negation. In this case, the negation counts since gcm(¬¬A) = gcm(A) + 1. A similar argument supports this way of counting double negation. Let us consider the truths expressed by ¬¬A and A. Not only are we concerned with a relationship between truths -if one of these formulas expresses a truth, then so does the other -but, more importantly, this relationship is direct: there is no "intermediate" truth that one passes through to obtain the former from the latter. Thus, it makes sense to count the g-complexity of ¬¬A as equal to that of A plus one.

We now have a measure of complexity which seems natural and adequate for the grounding framework. In order to formulate an appropriate notion of subformula -from now on we will call this type of subformula g-subformula, to distinguish it from the classical one -we need two further notions: the notion of the converse of a formula D, denoted by D * , and the relation ∼ =.

Let us start by introducing the notion of the converse of a formula.

Definition 4.5. The converse of a formula D, written D * , is defined as follows:

D * = ¬ n-1 E, if D = ¬ n E and n is odd ¬ n+1 E, if D = ¬ n E and n is even
where the main connective in E is not a negation, n 0 and 0 is taken to be an even number.

The notion of converse of a formula is quite simple; the basic motivation is that a formula A and its converse A * are two objects that only differ by one occurrence of a negation symbol but have the same g-complexity. The converse of a formula is calculated differently depending on whether it starts with an odd or an even number of negations. Suppose that the formula D is of the form ¬¬E where the main connective of E is not a negation, i.e. D is a formula with an even number of outer negations. Both ¬E and ¬¬¬E differ from D by one negation; however, while ¬¬¬E has the same g-complexity as D, ¬E has a lower g-complexity. Thus ¬D (i.e. ¬¬¬E) is the converse of D. On the other hand, by similar reasoning, if D is of the form ¬E where the main connective of E is not a negation, i.e. D is a formula with an odd number of outer negations, then its converse is not ¬D (i.e. ¬¬E) but rather E.

The second notion required to formulate the definition of subformula in the grounding framework, i.e. the notion of g-subformula, is the relation ∼ =. We firstly introduce the formal definition of ∼ = and then we explain the intuitive idea behind it.

Consider a formula A. We will say that A is a-c equiv (for associatively and commutatively equivalent) to B, if, and only if, A can be obtained from B by applications of associativity and commutativity of conjunction and disjunction. 5 For example, if A is of the form E ∧ F , then the formula F ∧ E is a-c equiv to it. To take another example, if

A is of the form ¬((B ∨ C) ∧ (D ∨ F )) the formulas ¬((C ∨ B) ∧ (D ∨ F )), ¬((B ∨ C) ∧ (F ∨ D)), ¬((C ∨ B) ∧ (F ∨ D)) are a-c equiv to it. Finally, if A is of the form ((B ∨ C) ∨ (D ∨ F )), then the formulas ((B ∨ D) ∨ (C ∨ F )), ((D ∨ B) ∨ (F ∨ C)), ((B ∨ F ) ∨ (D ∨ C)) are all a-c equiv to it. Definition 4.6. A ∼ = B if,

and only if:

A is a-c equiv to B or A is a-c equiv to B * 5 We omit the formal definition of this notion for the sake of brevity.

Let us explain the relation ∼ = in intuitive terms. First of all note that each formula is a-c equiv to itself, so we have that not only each formula enters into the relation ∼ = with itself, but also that each formula and its converse enter into the relation ∼ =. But what relation does a formula entertain with itself but also with its converse? The answer we propose is: the relation of being about, or pertaining to, or concerning the same issue. Of course given two formulas A and A, since they are identical, it is trivial to say that they also are about the same thing. The same holds for the more interesting case of a formula and its converse. Consider for example the formula p ∧ q for "it is cold and it is raining" and the formula ¬(p ∧ q) for "it is not the case that it is cold and it is raining". In this case one can either focus on the fact that these formulas express contradictory propositions since either "it is cold and it is raining" is true or "it is not the case that it is cold and it is raining" is true; or one can focus on the fact that these two formulas share some essential features: they have the same g-complexity, the same atomic formulas and the same connective used in the same way and a same number of times (as explained in the previous paragraph, the presence of negation in this case does not make any difference). In sum, these two formulas concern the same issue: they both are about the cold and the rain irrespectively of any truth value. This is accurately reflected by the relation ∼ =.

Let us now consider two different formulas A and B which are a-c equiv ; then we have that even these two formulas are related by ∼ =. This captures the following intuitive idea. Consider the formulas p ∧ q for "it is raining and it is cold" and q ∧ p for "it is cold and it is raining"; these formulas share some essential features: the same g-complexity, the same atomic formulas and the same connectives used in the same way and a same number of times. Thus, even of "it is raining and it is cold" and "it is cold and it is raining" we would like to say that they are about the same thing, i.e. namely the conjunction of it is raining and it is cold irrespectively of the order in which they are considered. Therefore even "it is cold and it is raining" and "it is raining and it is cold" are in the relation ∼ =.

Finally we have the case of two different formulas A and B such that A is a-c equiv to B * . In order to understand this case, we can easily adapt the explanation proposed for the other ones.

We have thus finished introducing the relation ∼ =. 6 We now have all the elements to define our notion of g-subformula, which is the analogue of the notion of subformula in the grounding framework. Definition 4.7. A is a g-subformula of B if, and only if, one of the following holds:

-A ∼ = B -B ∼ = ¬¬C and A is a subtruth of C, -B ∼ = (C • D) and A is a subtruth of C or a subtruth of D.
This definition is analogous to the definition of the notion of subformula with each of the concepts specific to the notion of subformula and to classical logic being adapted to the grounding framework. The first item of the definition of subformula, namely Definition 4.2, states that, if A = B, then A is a subformula of B. The first item of the definition of g-subformula is built analogously but with the substitution of the notion of identity with the notion of ∼ =, that can be thought of as the grounding counterpart of the identity. This yields: if A ∼ = B, then A is a g-subformula of B. This implies that not only A is a g-subformula of itself, but also A * is a g-subformula of A, as is any formula C, together with its converse, such that C is associatively and commutatively equivalent to A.

Let us pass to the second item. The second item of the definition of subformula states that if A is a subformula of B, then B = ¬C and A is a subformula of C. The second item of the notion of g-subformula is built analogously with identity substituted by the relation ∼ =, the formula ¬C substituted by the formula ¬¬C because, as we have explained previously, in the grounding framework only a double negation counts as a relationship between truths, and the notion of subformula substituted by the notion of g-subformula. We thus have: if B ∼ = ¬¬C and A is a g-subformula of C, then A is a g-subformula of B. This implies that given a formula ¬¬C, not only C is a g-subformula of ¬¬C, but also C * is a g-subformula of ¬¬C, and so is any formula D, together with its converse, such that D is associatively and commutatively equivalent to C.

The parallel between the third items of the definition of subformula and the definition of g-subformula is easily drawn in the light of what we have said for the previous two. Therefore, we have a notion of g-subformula that seems adequate for the grounding framework; we can use it to define the notion of being completely and immediately less complex in the grounding framework, in a way analogous to the Definition 4.3 for the case of classical logic. Definition 4.8. In the grounding framework, a multiset M is completely and immediately less g-complex than a formula C, if, and only if:

-C ∼ = ¬¬B and, M = {B} or M = {B * }, or -C ∼ = (B • D) and, M = {B, D} or M = {B * , D} or M = {B, D * } or M = {B * , D * }.
Analogously to the classical case, this seems to be a very natural way to define the notion of completely and immediately less g-complex, in the light of the notions of g-complexity and g-subformula introduced above, see Definitions 4.4 and 4.7, respectively. The multiset M is less g-complex than the formula C since gcm(M ) < gcm(C) (where gcm(M ) is the sum of the g-complexity of its members). The multiset M is immediately less g-complex than the formula C since it contains only g-subformulas that can be immediately obtained from C by appropriately removing its main connective(s). The multiset M is completely less g-complex than the formula C since it contains all g-subformulas that are precisely at one level below C.

We finally have the notion of being completely and immediately less g-complex in the grounding framework. This notion has been built in several steps, each of which has been motivated. So we hope that Definition 4.8 does not come as a surprise but, instead, looks like the straightforward conclusion of all we have said in the last paragraphs.

Let us end the section by (i) giving some examples of formulas that are completely and immediately less g-complex than another formula, and (ii) checking whether the notion introduced in Definition 4.8 meets all the desiderata that we have enumerated in Section 3.

Let us start with task (i). We will give examples that are also useful to understand the role of the notion of converse of a formula and the relation ∼ = in the definition of the notion of being completely and immediately less gcomplex. Let us start with the formula ¬p ∧ ¬q; the multisets of formulas that are completely and immediately less g-complex than ¬p ∧ ¬q are {¬p, ¬q}, {p, ¬q}, {¬p, q}, {p, q}. Consider now the formula ¬¬p ∧ ¬¬q; the multisets of formulas that are completely and immediately less g-complex than ¬¬p ∧ ¬¬q are {¬¬p, ¬¬q}, {¬¬¬p, ¬¬q}, {¬¬p, ¬¬¬q}, {¬¬¬p, ¬¬¬q}. Note that it is thanks to the notion of the converse of a formula that we can indicate in a uniform way the formulas that are immediately and completely less g-complex than ¬p ∧ ¬q and ¬¬p ∧ ¬¬q. In order to obtain such formulas, we should in one case erase a negation, and in the other case add a negation: the operator * takes both these cases into account.

Consider now the formula ¬¬((p∧q)∧r). Amongst the multisets of formulas that are completely and immediately less g-complex than ¬¬((p ∧ q) ∧ r), there are: {(p ∧ q) ∧ r}, {¬((p ∧ q) ∧ r)}, but also {(q ∧ p) ∧ r}, {¬((q ∧ p) ∧ r)}, {(q ∧ r) ∧ p}, {¬((q ∧ r) ∧ p)}, {(q ∧ p) ∧ r}, {¬((q ∧ p) ∧ r)}. The role of the relation ∼ = is to allow all these different multisets.

Let us now turn to task (ii): we should check whether the notion of being completely and immediately less g-complex introduced in Definition 4.8 has the virtue V and overcomes the problems P1 -P3 discussed in Section 3 with Definition 4.3. As for the virtue V, this is satisfied; to see this, consider a truth like p ∧ q. According to Definition 4.8, amongst the multisets which are completely and immediately less g-complex than p ∧ q there is {p, q} (the others are {¬p, q}, { p, ¬q} and {¬p, ¬q}) and this is precisely what we wanted.

Let us now pass to problems P1 -P3 and let us start by analyzing problem P1. This problem has been overcome by Definition 4.8: indeed, amongst the multisets that are completely and immediately less g-complex than a formula like (p ∧ q) ∧ r, there are the following ones {p ∧ q, r}, {q ∧ p, r}, {p ∧ r, q}, {r ∧ p, q}, {q ∧ r, p}, {r ∧ q, p} and this is precisely what we wanted. Let us now move to problems P2 and P3, which both concerned the negation. On the one hand, we have that, according to our Definition 4.8, amongst the multisets that are completely and immediately less g-complex than a formula like ¬¬p, there are both {p} and {¬p}. Thus problem P2 has been overcome. On the other hand, we have that, according to our Definition 4.8, amongst the multisets that are completely and immediately less g-complex than a formula like ¬(p ∧ q) there is {¬p, ¬q} (the others are {p, q}, {¬p, q} and { p, ¬q}). Thus problem P3 has also been solved. So all our desiderata have been satisfied; this could be taken as an additional sign of the adequateness of the proposed notion of being completely and immediately less g-complex for the grounding framework.

5 The paradigmatic case of disjunction (or why we need another ingredient to define formal grounding)

We have seen some salient features of the notion of formal grounding that partly come from the literature and partly have been developed in this paper. More precisely, in the previous sections, we have argued that the notion of classical derivability and the notion of being completely and immediately less g-complex are two necessary conditions for complete and immediate formal grounding. The question now is whether they also are sufficient. In this section we will show that they are not. In the next section we will introduce the final missing ingredient in the definition of formal grounding.

In order to show why the notions of classical derivability and being less gcomplex are necessary but not sufficient for the definition of formal grounding, we will use the paradigmatic case of disjunctive truths. Let us then consider a disjunctive truth like A ∨ B and suppose that A is true. A is then a ground for A ∨ B. But is A the complete ground for A ∨ B? The answer would seem to depend on the truth value of B. If B is true, then A and B together are the complete grounds of A ∨ B. And if B is false? In this case, A would seem to constitute the complete ground of A ∨ B: but this is only because B is false. Indeed, as just noted, if B were true, A would no longer constitute the complete ground of A ∨ B (it would merely be a partial ground). Hence, in the case where B is false, it still has a role to play in determining the grounds of A ∨ B: its falsity ensures that, or is a condition for A to be, the complete ground for A∨B.

To capture this role, we shall say that A is the complete ground for A ∨ B under the robust condition that B is false, or equivalently, we will say that A is the complete ground for A ∨ B under the robust condition that the converse of B is true. Thus, according to this analysis of disjunctive truths, in order to give the complete and immediate grounds of A ∨ B, a distinction between grounds and robust conditions is required: indeed either both disjuncts are the complete grounds of the disjunctive truth, or if only one of them is, this can only happen under the condition that the converse of the other one is true. 7This treatment of disjunctive truths seems reasonable and adequate. To illustrate the complete and immediate grounds of a disjunctive truth, let us consider the sentence "I take the umbrella or the coffee is good". According what we have said up to now, the complete and immediate grounds of "I take the umbrella or the coffee is good" are the following:

-either "I take the umbrella" and "the coffee is good"; -or "I take the umbrella" under the robust condition that "the coffee is not good";

-or "the coffee is good" under the robust condition that "I do not take the umbrella".

Each of the two disjuncts "I take the umbrella" and "the coffee is good" always has a role to play in determining the complete grounds of "I take the umbrella or the coffee is good". If it is true, it belongs to the complete grounds of "I take the umbrella or the coffee is good". If it is false, then its falsity in itself is a condition for the other disjunct to be a complete ground for "I take the umbrella or the coffee is good": after all, if "the coffee is good" were true, "I take the umbrella" would no longer be the complete grounds for "I take the umbrella or the coffee is good".

Let us now consider whether a definition of grounding in terms of derivability and the notion of being completely and immediately less complex -let us call this definition D-C def -can properly deal with the disjunction case discussed above. More precisely, let us try to understand whether D-C def is powerful enough to render the distinction between grounds and robust conditions that we have just introduced and that is specific to the disjunctive case. To answer these questions, let us consider the disjunctive truth "I take the umbrella or the coffee is good" and let us suppose that "I take the umbrella" and "the coffee is not good" are both true. Then, according to D-C def, we have that both "I take the umbrella" and "the coffee is not good" are the complete and immediate grounds of "I take the umbrella or the coffee is good". Indeed from "I take the umbrella" and "the coffee is not good" "I take the umbrella or the coffee is good" is derivable, and "I take the umbrella" and "the coffee is not good" are completely and immediately less g-complex than "I take the umbrella or the coffee is good" according to our Definition 4.8. Thus, if we define formal grounding just in terms of derivability and complexity, we cannot make any distinction between grounds and robust conditions. Moreover, we obtain the mistaken conclusion that "the coffee is not good" is a ground of "I take the umbrella or the coffee is good". This means that D-C def is not powerful enough to render the subtle distinctions specific to the grounding framework; we are lacking an ingredient in our definition of complete and immediate formal grounding.

A definition of the notion of complete and immediate formal grounding

In this section we will introduce and discuss the third and final ingredient in our definition of complete and immediate formal grounding. Our intuitive idea can be explained as follows. Let us begin with the claim that in a grounding relation the consequent is strictly connected to its grounds: this claim sounds rather unproblematic (the reader can find similar claims in [START_REF] Correia | Grounding: an opinionated introduction[END_REF][START_REF] Fine | The pure logic of ground[END_REF]), but is also quite vague. The question is then that of making it more precise, i.e. of clarifying this idea of strict connection. In order to clarify the idea of strict connection, we will use the concept of variation; we will say that in a grounding relation the consequent varies together with each variation of its grounds. This new claim seems to present the same characteristics as the previous one: on the one hand, it sounds acceptable (the idea of explaining a connection within a variation is certainly not new, see [START_REF] Lewis | Causation[END_REF][START_REF] Nozick | Philosophical explanations[END_REF]), but is still in need of further clarification. Indeed, if we really want to understand what grounding is about, we need to specify what kind of variations are relevant and what exactly it means for the consequent to vary with its grounds. Recall firstly an important point that has already been emphasized several times: in a grounding framework we only deal with truths and grounding is a relation amongst truths. We then might want to say that there is only one way a ground could vary: its negation, rather than itself, could be true. Though on the right lines, this claim still needs to be refined for our case. For we are interested in complete grounds, that is a bunch of truths that only together constitute the ground of another truth. The analogous variation to that just described for such a collection of truths would involve the negation of the collection en bloc: that is, the negation of each of its members, rather than the members themselves, being true. How should the consequence vary with such a variation of a collection of truths for it to constitute its complete (and immediate) grounds? We suggest that for a consequent to vary with its complete grounds is the same as for the consequent to track the truth of its complete grounds: if each of its grounds is true, then the consequent is true too; but also, if the negation of each of its grounds were true, the negation of the consequent would be true too. Adapting Nozick's [START_REF] Nozick | Philosophical explanations[END_REF] famous statement about knowledge to the case of grounding:

To ground a sentence is to have that sentence track the truth of its reasons. Grounds and their consequence are connected in a particular way, the latter tracks the truth of the former.

We have thus clarified the idea of a consequent varying together with its grounds by means of the idea of a consequent tracking the truth of its grounds. To transform this into a formal definition, we will use the concept of classical derivability. Therefore, not only, as we have already seen, we will say that in a grounding relation the consequent is derivable from its grounds, but also, and this is the third and final ingredient in the definition of formal grounding, that the negation of the consequent is derivable from the negation of each of its grounds. By specifying both these types of derivability, we finally have a proper account of the notion of formal grounding. Indeed, it is only by specifying both these types of derivability that we have the full formal counterpart of the idea of strict connection that lies at the heart of the notion of (formal) grounding.

Let us denote robust conditions with the notation [C], where C is a formula of the language L c ; moreover we will adopt the following convention ¬(M ) := {¬B|B ∈ M }. The preceding discussion motivates the following definition. Definition 6.1. For any consistent multiset of formulas C ∪M , we say that, under the robust condition C (which could be empty), the multiset M completely and immediately formally grounds A, [C] M |∼ A, if and only if:

-M A -C, ¬(M ) ¬A
-C ∪ M is completely and immediately less g-complex than A, in the sense of being completely and immediately less g-complex given in Definition 4.8.

Under the robust condition C, the multiset M completely and immediately formally grounds A if, and only if, (i) A is derivable from M -we call this item positive derivability; (ii) ¬A is derivable from ¬(M ) and C -we call this item negative derivability; (iii) C ∪ M is completely and immediately less g-complex than A -we call this item g-complexity. The notion of g-complexity describes the grounding hierarchy in which formulas are organized; in particular, the notion of being completely and immediately less g-complex gives an exhaustive description of each step of this hierarchy. The notions of positive and negative derivability tell us which formulas in each step of this hierarchy enter into a grounding relation.

Let us make two remarks concerning robust conditions. On the one hand, although in a complete and immediate grounding relation, there might be more than one ground, there never is more than one robust condition. This is the reason why in Definition 6.1 there is no need to use multisets to denote robust conditions, while multisets are useful to denote grounds. On the other hand, in certain complete and immediate grounding relations, there is no occurrence of robust condition. This is the case for the grounding relation between {A} and ¬¬A, {A, B} and A ∧ B, {A, B} and A ∨ B. Thus, in Definition 6.1, it is specified that the robust condition C may be empty.

We finally have the definition of complete and immediate formal grounding. Let us test this definition on the problematic case of disjunction. The capacity to deal with this case could be taken as a sign of the adequacy of the definition itself.

Consider again the truth "I take the umbrella or the coffee is good" and, for the sake of brevity, let us formalize it with p ∨ q. According to what we have said in the previous section, the complete and immediate formal grounds of p∨q are:

• either p and q,

• or [¬q] p,

• or [¬p] q.

Let us check whether this is the case according to Definition 6.1. As for the case of p and q, these are indeed the complete and immediate grounds of p ∨ q according to Definition 6.1: from p and q, p ∨ q is derivable; from ¬p and ¬q, ¬(p ∨ q) is derivable; and finally p, q are completely and immediately less g-complex than p ∨ q. Let us now consider the case of [¬q] p; from p, p ∨ q is derivable; from ¬p and ¬q, ¬(p ∨ q) is derivable and, finally, p and ¬q are completely and immediately less g-complex than p ∧ q. So, according to Definition 6.1, p is the complete and immediate ground of p ∨ q under the robust condition ¬q. A similar conclusion holds for the case [¬p] q. Thus Definition 6.1 correctly captures the case of disjunction. In particular, thanks to the notion of negative derivability, the missing ingredient introduced in this section, we are finally able to take into account the distinction between grounds and robust conditions: while grounds cover a role in both positive and negative derivability, robust conditions only appear in negative derivability. This can be taken as an indication that robust conditions and negative derivability are the two sides of the same coin, the latter being the formal counterpart of the former.

Comparisons between our approach and other approaches to the notion of grounding

In this section we analyse the differences between our account of the notion of complete and immediate formal grounding and those proposed in three articles recently published by Correia [START_REF] Correia | Logical grounds[END_REF], Fine [START_REF] Fine | Guide to ground[END_REF], Schnieder [START_REF] Schnieder | A logic for 'Because[END_REF]. This will shed light not only on the originality of our approach, but also, and more importantly, on its most noteworthy features.

The main points of comparison will concern aspects that are common to the three aforementioned theories. In fact they concern three kinds of cases: the case of disjunction and negation of conjunction; the case of formulas that are equivalent by associativity and commutativity of conjunction and disjunction, and the case of negation. We will analyze them one by one.

Let us start by the case of disjunction and negation of conjunction. In order to analyze this case, we will mainly focus on disjunctive truths, leaving aside truths that have the form of the negation of a conjunction. We will do this for the sake of brevity, since everything that can be said about disjunction can also be said about the negation of a conjunction.

Let us then come back to the disjunctive truth "I take the umbrella or the coffee is good". Consider three distinct situations: (i) in the first both "I take the umbrella" and "the coffee is good" are true; (ii) in the second only "I take the umbrella" is true; (iii) in the last situation only "the coffee is good" is true. Let us compare our approach to that adopted by Correia, Fine and Schnieder with respect to each of these situations. In situations (ii) and (iii), while they claim that "I take the umbrella" on the one hand and "the coffee is good" on the other hand are, respectively, the full and immediate grounds of "I take the umbrella or the coffee is good", according to our analysis, robust conditions should also be taken into account in order to get the complete and immediate grounds of such a truth. Thus, in situations (ii) and (iii) the two approaches diverge and one might want to say that our approach is actually a refinement of that of Correia, Fine and Schnieder, since we put forward an element that they neglect. Let us then move to situation (i). In this situation, Correia, Fine and Schnieder consider there to be three sets of full and immediate grounds: "I take the umbrella" by itself, "the coffee is good" by itself, but also "I take the umbrella" and "the coffee is good" together. By contrast, according to our approach, only "I take the umbrella" and "the coffee is good" together can be considered as the complete and immediate grounds of "I take the umbrella or the coffee is good". Thus, in this case, the two types of analysis are quite distant one from the other. This difference is due to the different notions of grounding that are at stake. Indeed, while our approach focuses on the notion of complete and immediate grounding, the aforementioned authors concentrate on the notion of full and immediate grounding. The two concepts, though similar, are not the same (see Section 3); in particular, a little reflection suffices to realize that it is precisely in the case of disjunction (and negation of conjunction) in circumstances like situation (i) that they diverge.

Let us now turn to the second difference between our account and those of Correia, Fine and Schnieder: this difference concerns formulas that are equivalent by associativity and commutativity of conjunction and disjunction. In order to explain this difference, we will focus and use formulas that have a conjunctive form. However, we note that this is not limitative in any way: everything that will be said about these formulas can easily be adapted to any other type of propositional formula. Let us then start our analysis. It is generally accepted in the contemporary literature on grounding [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF] that, given a formula of the form A ∧ B, {A, B} is the only full and immediate ground of A ∧ B. In this paper we claim something different, namely that not only {A, B} is a complete and immediate ground of A ∧ B, but so is any multiset {C, D} such that C ∧ D is associatively and commutatively equivalent to A ∧ B. Given that this difference is quite significant, further justification and explanation of our position are in order.

For this let us focus on the specific example (that is closely related to problem P1 of Section 4) of the truth (p∧q)∧r. According to the way we have defined our notion of complete and immediate formal grounding (Definition 6.1), not only the multiset {p∧q, r} is a complete and immediate formal ground of (p∧q)∧r, but so are each of the multisets {q∧p, r}, {p∧r, q}, {r∧p, q}, {r∧q, p} and {q∧r, p}. 8As already explained in the paragraph above, this is a quite big departure from the current literature, since, according to Correia, Fine and Schnieder, only the multiset {p ∧ q, r} is the full and immediate ground of (p ∧ q) ∧ r. So why should each of the following multisets {q ∧ p, r}, {p ∧ r, q}, {r ∧ p, q}, {r ∧ q, p} and {q ∧ r, p} be considered as a complete and immediate ground of the truth (p ∧ q) ∧ r? In order to answer this question, we will only concentrate on the multiset {q ∧ p, r}; what is said about this multiset holds for the others.

When taken together {q ∧p, r} and (p∧q)∧r undoubtedly stand in a grounding relation; in particular, it seems natural to claim that the multiset {q ∧p, r} is a ground of (p ∧ q) ∧ r. This grounding relation appears so straightforward that it would be up to the one who denies it to argue against it; the issue is therefore to understand what type of grounding relation is involved. We recall that there are only four possibilities: either it is a relation of complete (or full) and immediate grounding, or a relation of complete (or and mediate grounding, or of partial and immediate grounding or of partial and mediate grounding. Let us consider the two distinctions complete-partial and immediate-mediate in turn.

Let us start by the distinction complete-partial, which is the easiest one. Whatever version of this distinction one uses -be it the full-partial distinction used by Fine or the complete-partial one used by Bolzano and adopted in this paper (see Section 3) -the conclusion is the same: {q ∧ p, r} cannot but be a complete or full ground of (p ∧ q) ∧ r. Indeed in {q ∧ p, r} each of the atomic formulas that compose (p ∧ q) ∧ r appear and nothing is missing. Thus we have ruled out the option of partial grounding. Let us now then move to the distinction immediate-mediate. Even in this case the situation does not seem too complicated. In a formal grounding framework, the introduction of a new conjunction corresponds to a new grounding step; but {q ∧ p, r} and the truth (p ∧ q) ∧ r precisely differs by one conjunction. Thus only one grounding step separates them and they stand in an immediate grounding relation.

Given what we have just seen, we can draw the conclusion that, whatever approach to grounding one adopts, one is committed to accept that the multiset {q ∧ p, r} is a complete (or full) and immediate ground of (p ∧ q) ∧ r; actually we are committed to accept that each of the multisets {q ∧p, r}, {p∧r, q}, {r ∧p, q}, {r ∧q, p} and {q ∧r, p} is a complete (or full) and immediate ground of (p∧q)∧r. The situation is so because of two things; on the one hand, it cannot be denied that between the multisets {q ∧ p, r}, {p ∧ r, q}, {r ∧ p, q}, {r ∧ q, p} and {q ∧ r, p} and (p ∧ q) ∧ r there is a grounding relation. But, once this is acknowledged, the only possibility as type for this grounding relation this grounding relation is as complete (or full) and immediate grounding. Therefore this is an important feature of the concept of grounding that has not been emphasized before. Our account, by contrast, properly takes it into account and adequately treats it.

Let us now move to the analysis of the third and final difference between our approach and that presented in the papers [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF]. This difference is quite easy to explain. Consider a formula of the form ¬(A ∨ B): while in our account a complete and immediate ground of this truth is the multiset {A * , B * }, according to [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF] the full and immediate ground of this truth is the multiset {¬A, ¬B}. Thus, once again, the two accounts differ and it seems necessary to explain this difference.

Let us consider the case where ¬(A ∨ B) has the form ¬(¬p ∨ ¬q): it is important to consider this case, i.e. a case where the two members of the disjunction has as principal connective a negation, since it is precisely in this type of situation that the difference between our approach and Correia, Fine and Schnieder's comes to the fore. Suppose for example that the formula ¬(¬p ∨ ¬q) stands for the truth "it is not the case that it is not raining or it is not cold" and consider the question of which of the following are its complete and immediate grounds: "it is raining" and "it is cold" or "it is not the case that it is not raining" and "it is not the case that it is not cold" on the other hand. Any intuitive idea of what grounding is would suggest that they are "it is raining" and "it is cold". Unlike the other truths, these are less g-complex than the grounded truth and thus constitute the best candidate for the role of complete and immediate grounds.

Let us now show how our approach takes these intuitions into account. For the sake of brevity, let us formalize "it is not the case that it is not raining or it is not cold" by ¬(¬p∨¬q). According to our account, the complete and immediate grounds of ¬(¬p ∨ ¬q) are (¬p) * and (¬q) * , i.e. p and q. Indeed from p and q, ¬(¬p ∨ ¬q) is derivable, from ¬p and ¬q, ¬¬(¬p ∨ ¬q) is derivable, and p and q are completely and immediately less g-complex than ¬(¬p ∨ ¬q). According to our approach, and contrary to [START_REF] Correia | Logical grounds[END_REF][START_REF] Fine | Guide to ground[END_REF][START_REF] Schnieder | A logic for 'Because[END_REF]'s approach, ¬¬p and ¬¬q are not the grounds of ¬(¬p ∨ ¬q): indeed, despite the fact that from ¬¬p and ¬¬q, ¬(¬p∨¬q) is derivable, and from ¬¬¬p and ¬¬¬q, ¬¬(¬p∨¬q) is derivable (and thus positive and negative derivability are satisfied), ¬¬p and ¬¬q are not less g-complex than ¬(¬p ∨ ¬q); actually, according to our measure of g-complexity, they are more g-complex. Thus, our approach, and in particular our measure of g-complexity which has been carefully introduced and motivated in Section 4, reflect more accurately some very natural intuitions concerning the use of negation in the grounding framework. We consider this to be an important contribution of our notion of grounding.

Conclusions

In this paper we have focused on the notion of complete and immediate formal grounding, providing a definition for this notion. The two key ingredients of the definition are: the classical notion of derivability and a notion of complexity that has been built specifically for the grounding framework. Thanks to this definition, we have developed an original and accurate analysis of several typical grounding cases.

We think that the results of this paper could serve as a starting point for several different directions of future research. Here we outline three of the most significant ones. First of all, it would be important to adapt our definition of complete and immediate grounding to the cases of complete and mediate, partial and immediate and partial and mediate grounding. Secondly, it would be interesting to extend our analysis of grounding from the propositional case to the first-order predicate case. Finally and most crucially, the results of this paper could guide the development of a logic of grounding, which may differ from those that already exist in the literature.

For the sake of clarity, let us note that grounding might also be seen as a sentential operator, rather than a relation. For a detailed discussion of these issues see[START_REF] Correia | Grounding: an opinionated introduction[END_REF].

We work with multisets rather than with sets because, as will become evident later on, we need to take into account the number of occurrences of each formula of M .

For a detailed analysis of Bolzano's complexity constraint see[START_REF] Rumberg | Bolzano's theory of grounding against the background of normal proofs[END_REF].

From now on • = ∧, ∨.

The relation ∼ = as defined only captures some aspects of the informal notion of "being about the same thing". A more thorough attempt at capturing this notion would perhaps add an item stating that formulas of the form A, A ∧ A, A ∧ A ∧ A, ... , as well as formulas of the form A, A ∨ A, A ∨ A ∨ A, ..., fall under the relation ∼ =, since they clearly concern the same issue. Doing so would not be difficult, and involve minimal changes in the discussion and points made below. However, we prefer not to do it for the following reason: formulas of the form A ∧ A, A ∧ A ∧ A . . . , as well as formulas of the form A ∨ A, A ∨ A ∨ A, . . . , are rather peculiar formulas, not very significant in the framework of a theory of grounding. Therefore, adding to Definition 4.6 an item concerning them would just burden the definition without providing any new significant insight.

In Bolzano a similar idea of condition can be found, see[4, §222, p. 389].

Let us note that in[START_REF] Correia | The impure logic of conceptualistic grounding[END_REF] we can find a similar idea for the logic of conceptual grounding.


Yewan Wang

David Nörtershäuser

Stéphane Le Masson

Jean- Marc Menaud

Potential effects on server power metering and modeling

Keywords: Server Benchmarking, Power Estimation, CPU Temperature

Cloud datacenters are compute facilities formed by hundreds or even thousands of servers. With the increasing demand of cloud services, energy efficiency of servers in data center has become a significant issue. The knowledge of the energy consumption corresponding to hardware and software configuration is important for operators to optimize energy efficiency of a data center. We currently work on a predictive model for energy consumption of a server, with inputs as service provided, hardware material equipped (type and quantity of processor, memory and hard drive) and technical environment (energy conversion and cooling). In this article, we characterize some potential factors on the power variation of the servers, such as: original fabrication, position in the rack, voltage variation and temperature of components on motherboard. The results show that certain factors, such as original fabrication, ambient temperature and CPU temperature, have noticeable effects on the power consumption of servers. The experimental results emphasize the importance of adding these external factors into the metric, so as to build an energy predictive model adaptable in real situations.

Introduction

Data Centers are facilities composed of a large amount of servers, they are the cornerstones of the Internet that support data traffic transaction and storage for different cloud service, such as real-time video streaming, online gaming and mail service. However, with the rapid growth of the cloud service in recent years, data centers have become a huge energy consumer, their power densities are 538-2153 W/ m2 and sometimes can be as high as 10 KW/ m2 [START_REF] Beaty | Internal IT load profile variability[END_REF]. The study of the configuration of suitable information system in data center becomes indispensable to make good use of the hardware resources [START_REF]Energy Efficiency -European Commission[END_REF]. Therefore, a simulation model for energy consumption is useful for designing data centers satisfying the current need and in the same time, without causing too much waste in hardware resources. A such model should be able to predict energy consumption with the following inputs: information service provided (performance throughput), server hardware and software configuration as well as the associated technical environment (cooling system, room space, etc.). Much work has been done on building accurate power pre-dictive models for servers in data centers. Some of them proposed high-accuracy software-level solutions as replacements to physical analyzers in order to allocate efficiently physical resources and make the system more energy-aware [3][4]. However, during our experimental measurements, we find that some factors may cause unexpected power variation in servers. We compare the difference of power among 15 identical servers by using an industrial-standard benchmark. Several potential factors in real data centers that may affect servers' power in physical experiments are evaluated, such as: original fabrication process, way of placement in racks, fluctuating neighboring temperature, source voltage variation. Especially, we design tests to evaluate and characterize the influence of temperature variation of CPU and of the other components to the power, as well as the performance of servers, in precisely controlled experiment conditions. Normally, the consumption of CPU depends mainly on IT load. As the power increases with the load, CPU works harder and dissipates more heat, if the heat is not evacuated in time by the cooling system, the temperature surround CPU becomes higher and leads to the rise of leakage current, which will in reverse increase the power of CPU [5][6]. However, the influence of this thermal effect to the power consumption in system level hasn't been precisely characterized.

The paper is organized as follows: Firstly, we briefly introduce the related work in Section 2. In Section 3, we explained how physical measurements are performed to 15 identical servers in using an industrial standard test tool. This aims to clarify how power varies among identical servers in a real data centers. Then, in Section 4 we study the influence of temperature on power consumption and performance of servers in system level. Temperature is varied separately on CPU and the other components than CPU in the motherboard. Conclusions are given in Section 5.

The goal of this paper is to identify and characterize the impact factors contributing to the power variation of servers, in order to help correcting the precision of existing theoretical models built from mathematical analyses. The major contributions of this paper are: ─ We compare the power consumption of 15 nominally identical servers. An industrial-standard benchmark has been used to stress different components of the servers at different target levels. ─ We explore several potential factors that may contribute to the power variation of servers in real data centers, including: server fabrication, way of placement in racks, fluctuating neighboring temperature and variation of source voltage to the server power. ─ We characterize separately the impact of temperature by components on power and performance of servers equipped with CPUs in different generations.

Related work

Some recent studies concluded that other than IT load applied to the components (CPU, memory, network and storage), the power of servers can be affected by external factors, such as original fabrication process [START_REF] Coles | Comparing Server Energy Use and Efficiency Using Small Sample Sizes Coles[END_REF][8], ambient temperature [START_REF] Orgerie | Demystifying energy consumption in grids and clouds[END_REF][10] [START_REF] Sampath | Thermal Analysis of High End Servers Based on development of detail modeland experiments[END_REF], way of placement in a rack. Henry C Cole et al. [START_REF] Coles | Comparing Server Energy Use and Efficiency Using Small Sample Sizes Coles[END_REF] conducted several tests among three server manufacturers (three from Intel, one from Dell and one from Supermicro) with similar mechanical and electronic specifications, in order to determine whether the energy use and efficiency of server had the relationship with their brands. 5% difference of power consumption was observed among three identical Intel servers. They switched their main components in the motherboard in order to identify the source of the difference. The results showed that the difference was mainly brought by CPU. However, these tests were performed within only three servers and the conclusion was suggestive rather than definitive. In a thermodynamic analysis of Patterson et al. [START_REF] Patterson | The effect of data center temperature on energy efficiency[END_REF], the ambient temperature affects server power in two ways: through temperature sensitive components (i.e. CPU) and through server internal cooling fans. They draw the conclusion theoretically by analyzing a typical data center configuration. CPU temperature draws much attention, as a lot of work has confirmed the strong relationship between CPU temperature and server power [START_REF] Haywood | The relationship among CPU utilization, temperature, and thermal power for waste heat utilization[END_REF][14] [START_REF] Garraghan | A Unified Model for Holistic Power Usage in Cloud Datacenter Servers[END_REF]. Mair et al. [START_REF] Mair | Myths in PMC-Based power estimation[END_REF] observed the power latency when running unchanged system load in the server. Moreover, the duration of power latency follows tightly the CPU warm-up period, and the system's fan speed remained steady at 3600 rpm during the test. Therefore, the power latency in this case was not due to the consumption of fan but to the rise of CPU temperature. The conclusion was that the CPU temperature can result in notable variation of power consumption before and after the stable state. They suggested to prolonger the execution time to eliminate this thermal impact and increase the model precision. However, the correlation between the CPU temperature and the server power hasn't been discussed and only the AMD architecture servers are concerned in their studies.

Do identical servers under the same load always have the same energy consumption?

IMT Atlantique in Nantes (France) is one of the sites of Grid5000 [START_REF]Ubuntu Manpage: cpuburn, burnBX, burnK6, burnK7, burnMMX, burnP5, burnP6a collection[END_REF], an experiment-driven platform grouped in homogeneous clusters from 8 cities across France. It provides open access to geographically distributed resources for researches in computer science domain. The site located in Nantes disposes of 4 racks and each rack stores 12 identical servers (Dell PowerEdge R630 20CPU@1.8GHz), as shown in Fig. 1.

Experiments setup

Five micro-workloads in the SERT [START_REF] Lange | The Design and Development of the Server Efficiency Rating Tool (SERT)[END_REF] are chosen as the test suite. SERT (Server Efficiency Rating Tool) is an industrial standard rating tool for evaluating energy-efficiency for server systems, developed by SPEC committee. It contains a number of micro-workloads, called Worklets that exercise different components of the SUT (Server Under Test) at different target load levels (except idle). In our experiment, we chose 5 typical worklets in SERT to stress CPU, memory and storage system of the SUT, in order to analyze the power consumption variations for identical servers. The details of these worklets are shown in Table 1. Firstly, we run SERT on S1 twice, the power and performance (operations throughput) variation is within 1%, which means the result of SERT is reproducible.

The system diagram shown in Fig. 2 includes three parts: Measurement system, Controller and SUT. ─ The measurement system is composed by two devices: Yokogawo WT330: a power analyzer measuring AC (alternative current) power provided to PSU (power supply unit) of server, with maximum measurement error less than 1%.

Testo176 + Thermocouple: a thermometer with two thermocouples connected (type K, with 0.1mm diameter) ─ Controller: controls SUT by sending commands via a network cable. Controller also gathers measurement data recorded by power and temperature analyzers with 1Hz sampling frequency. ─ SUT: installed with Linux OS compatible to SERT, systems are configured according to the guidelines described in the SPEC Methodology [START_REF]Standard Performance Evaluation Corporation (SPEC) Power and Performance Benchmark Methodology V2[END_REF] Table

Power variation for 12 identical servers in the same rack

The test suite is repeated on S1-S12 in sequence in rack 1. Fig. 3 shows the mean power of S1-S12 in running different worklets and Fig. 4 precises the maximumminimum percentage of variation on server power and performance.

It can be observed that under the same load, power variation among identical system in the same rack can reach up to 7.8%. According to our observations and previous state-of-the-art study, this variation may be caused by different potential factors, such as fabrication process, fluctuating neighboring temperature, way of placement in the rack and source voltage variation. However, we are not allowed to open or to move the servers belonging to Grid5000, the impact of construction will be completed in further research. In the following tests, we investigate the influence of ambient temperature, way of placement in the rack and variation of source voltage on power consumption of servers.

Power variation for 4 servers in the same altitude of the racks in two circumtances

SUTs are four servers at the same altitude in four racks: S6, S18, S30 and S42 (cf figure 1). Servers are placed in two ways: for S6 and S18, they are placed loosely and keep some distance between each other in rack 1 and 2. While for S30 and S42, they are placed next to other servers in rank 3 and 4. Different way of server placement affects the air circulation and heat distribution in racks. This allows us to compare the impact of placement density to the energy consumption of servers. Test suite is repeated twice in two cases. In case one, only the SUT is turned on in the rack. In case two, we increase the neighboring temperature by turning on the other servers. Fig. 5 shows the percentage of power variation in two cases for four SUTs. The results turned out that, for the same server under different neighboring temperatures, the power varies from 0 (idle, S42) to 5.6% (LU25%, S30). Comparing the percentage of variation between S6, S18 and S30, S42, we find that the server placement density has no obvious impact on power consumption.

Fig. 5. Percentage of power variation for servers under two circumstances

The impact of source voltage variation on server power consumption

While performing the tests in section 3.2 and 3.3, source voltage provided by grid varies from 230V to 240V. In order to eliminate the number of variables in this study, we perform another test in a laboratory, where the ambient temperature is controlled and remained at 23°C. The power supplied to the SUTs is delivered by an AC power generator, which can configure stable AC voltage. The tests are performed to two servers with very different characteristics: Gigabyte mw50-sv0 and Dell PowerEdg-eR630, details can be found in table 2. Test suite SERT is repeated for each server on 3 different voltages: 207V, 230V and 253V. For Gigabyte, the power variation is less than 2% for all the worklets. For Dell, the variation is less than 1.5% for worklets except the "Sequential" (storage, 2.8 %). For conclusion, the voltage variation from power supply doesn't introduce evident influence on the server power.

-2,0 %

0,0 % 2,0 % 4,0 % 6,0 % S6 S18 S30 S42 4
How thermal effect impacts on the consumption of servers?

Results of the experiments in Section 3 show that, apart from the system load, ambient temperature is the greatest contributor to the server power variation. However, the impact cannot be characterized without controlling precisely the neighboring temperature surrounding the server. In this section, we focus on the thermal impact on the power consumption of servers in system level. The impact of CPU temperature (leakage current) and the other components are studied separately in section 4.2 and 4.3. Fans, DC power generator and climatic cabins are provided to help controlling precisely the temperature of different components in the motherboard.

Experiments setup

Four servers equipped with different generations of CPUs from Intel are tested as shown in Table 2 In order to take away the additional electricity consumed by integrated fans, they are removed from motherboard and replaced by external fans powered by a separated DC power supply. The test diagrams are shown in Fig. 6 and Fig. 7, including four parts: measurement system, controller, SUT and temperature control system ─ The measurement system: Fluke 430T a power meter, allows measuring AC (alternating current) power provided to PSU (power supply unit) of server, with maximum measurement error less than 1%. ─ Controller: controls SUT by sending commands via a network cable. Power analyzer are connected to controller via USB cables, controller gathers power readings on server power with a sampling frequency at 1Hz. ─ SUT: installed with Linux OS. ─ Temperature control system: Fan powered by independent DC generator and climatic cabin.

Impact of CPU temperature (leakage current) to the server power and performance

Benchmark cpuburn [START_REF]Ubuntu Manpage: cpuburn, burnBX, burnK6, burnK7, burnMMX, burnP5, burnP6a collection[END_REF] was used to stress the SUT in this test. It is a CPU intensive benchmark that keeps the load level at 100% and maximizes the heat production of CPU. We vary the surface temperature of CPU via the external fan by adjusting the air flow between fan and heat sink1. Results of four different servers are shown in Fig. 8 -Fig. 11. It can be observed that under a constant load, the instant data of CPU temperature and server power are highly correlated with spearman coefficient larger than 0.93 for all the SUTs. The power varied more than 10 Watt for servers Gigabyte and Dell PowerEdgeR630, R740.

Conclusion

This paper addresses the question: whether identical servers delivery the same energy consumption under the same load. Physical experiments have been conducted in order to investigate the variation and reveal the causes. In Section 3, 7.8% power variation is observed among 12 identical servers running the same test suites. For the same server, fluctuating neighboring temperature can contribute to 5.6% power variation. Thermal effect, turned out to be one of the most contributors to the power variation, is investigated in precisely controlled experiments in Section 4. The results prove that CPU temperature can introduce very important power variation: for the server Gigabyte equipped with an Intel Xeon E5-2609v3 CPU, the power is increased by 16% when the temperature of CPU varies from 37.7°C to 74.5°C. However, the server power barely varies when the CPU temperature remains the same. Therefore, CPU is supposed to be the most temperature sensitive component in servers. The ambient temperature affects the power consumption of servers in two ways: the consumption of fans and CPU (leakage current).

The results presented here are significant for the development of a predictive model to estimate the power consumption of servers. Thermal effect, especially for CPU is turned out to have great impact on server power. This result also emphasize the importance of adopting more efficient cooling solutions like liquid cooling, in order to increase the energy efficiency for data centers. In the future work, the study will be completed by charactering the difference brought by fabrication process as mentioned in Section 3. The efforts are also encouraged to propose a method of controlling CPU temperature intelligently to balance the performance and cooling cost.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Mean power of 12 identical servers and variation of power and performance between different worklets

Fig. 8 .Fig. 6 . 7 .Fig. 9 .Fig. 10 .Fig. 11 . 13 .

 8679101113 Fig. 8. Relationship between CPU Temperature and server power-Gigabyte

Fig. 12 .Fig. 13 .Fig. 14 .

 121314 Fig. 12. Relationship between temperature of other components and server power -Gigabyte

Fig. 2. System diagram Fig. 1. Position of SUT in the room

		220
	Power ()Watt	120 140 160 180 200
		100
		S1	S2	S3	S4	S5	S6	S7	S8	S9	S10	S11	S12
		LU100 %			LU50 %			SHA100 %			SHA50 %
		Seq100 %			CapMax			Idle
	9,0 % 8,0 % 7,0 % 6,0 % 5,0 % 4,0 % 3,0 %											LU100 % LU75 % LU50 % LU25 % SHA100 % SHA75 % SHA50 % SHA25 %
	2,0 %											Seq100 %
	1,0 %											Seq50 %
	0,0 %											CapBase
			Power variation		Performance variation		CapMax
												Idle
	Worklet	Component	Description						Load level
	LU	CPU			Dense Matrix operations			100%, 75%, 50%, 25%
	SHA256	CPU			SHA-256 hashing transformation		100%, 75%, 50%, 25%
	Sequential	Storage		Reads and Writes data to/from file		100%, 50%
	Capacity3	Memory		XML validation					Base, Max
	Idle	system		No load on SUT					None

1. Test suite information.

Table 2 .

 2 : Characteristics of the SUTs.

	SUT	Gigabyte mw50-sv0	SuperMicro x10sdv-tln4f	PowerEdge R630
	Processor	Intel Xeon E5-2609v3,	Xeon D-1540, 2.0 GHz,	2 x Intel Xeon E5-2650L
		6 coeurs, 1.9GHz	20 coeurs	v4, 56 coeurs, 1.7GHz
	Release date	Q3 2014	Q1 2015	Q1 2016
	Memory	4 x 16Go DDR4	4 x 16Go DDR4,	4 x 32 Go DDR4
		2133MHz	2400MHz	2400MHz
	Storage	480Go SSD	400Go SSD	400Go SSD