Francesca Poggiolesi
email: poggiolesi@gmail.com

This paper studies internal (or intra-)mathematical explanations, namely those proofs of mathematical theorems that seem to explain the theorem they prove. In particular, the goal of the paper is to attempt to provide a rigorous analysis of these explanations. This will be done into two steps. First, we will show how to move from informal proofs of mathematical theorems to a formal presentation that involves proof-trees together with a decomposition of their elements into assumptions, conclusion and rules; secondly we will show that those mathematical proofs that are regarded as having an explanatory power all have the same formal presentation: they display an increase of conceptual complexity from the assumptions to the conclusion.

Introduction

Explanation is one of the cornerstone notions of philosophy and it involves a wide and rich literature. Among the several types of explanations, the most well-known, probably because of their centrality in empirical sciences, are causal explanations, namely explanations that rely on a causal relation between cause and effect. Studies on causal explanations are a wide area of research and several different models -from the DN-model to the structural equation framework -have been proposed.

More recently, another type of explanations has been gaining attention: they are the so-called non-causal explanations, i.e., explanations that do not rely (at least not entirely) on a causal relation. Several types of non-causal explanations have been identified and studied; amongst them particular attention has been dedicated to noncausal explanations related to mathematics, also called "mathematical explanations." However, the expression "mathematical explanations" is ambiguous: it could refer to explanations as they are given in mathematics, but it could also refer to explanations that make use of mathematics. The two meanings lead to a distinction of two classes. The first class gathers those explanatory practices that take place within mathematics; the second class involves those explanations of, for example, physical facts that use mathematics (see [START_REF] Mancosu | Mathematical explanation[END_REF]. The former are called internal or intra-mathematical explanations, the latter external mathematical explanations. The main aim of this paper is to investigate mathematical explanations in the first sense, namely internal mathematical explanations: these are by far the least studied amongst mathematical explanations and more generally non-causal explanations; hence they definitely deserve further attention.

However, the expression "internal mathematical explanation" covers an impressive range of different phenomena: an internal mathematical explanation could amount to the recasting an entire area of mathematics as well as to an explanation in a classroom, it could also be the explanation of the meaning of a symbol as well as an explanation on how to carry out a certain mathematical construction (e.g. see D'alessandro 2020). In this paper, we will focus on those internal mathematical explanations that take the form of proofs of mathematical theorems that not only prove that the theorem is true but also show why it is true. In other terms, for us internal mathematical explanations will only amount to explanatory proofs, namely proofs that explain the theorem that they prove.

Even restricting our attention to explanatory proofs, there are different ways a mathematical proof might explain: for instance, it might explain by relying on a diagram, or it might explain by drawing on an analogy. In this paper, continuing a trend that has so far received not too much of attention,1 we will only concentrate on those proofs that explain the theorem they prove by revealing the reasons why the theorem is true. In other words, as scientific explanations are explanations that display the cause of the phenomenon they want to explain, here we focus on those mathematical explanations (that have the form of proofs and) that explain the theorem they prove by revealing its grounds or reasons2 .

There exist several different approaches to internal mathematical explanations; here we quote the best-known. The oldest and probably most famous is the one proposed by [START_REF] Steiner | Mathematical explanation[END_REF], according to whom an internal mathematical explanation is a mathematical proof that uses a characterizing property, where a characterizing property is a property unique to a given entity or structure within a family or domain of such entities or structures. More contemporary accounts are the following. Lange (2017)'s account presents an impressively rich and varied choice of examples, which leads him to argue that most likely mathematical explanations do not fall under a general pattern, but that there are interesting classes of explanations. Another wide discussion has been offered by Pincock (2015a,b), who defends an abstractionist point of view on explanations. Finally, one of the most recent approaches has been proposed by [START_REF] Baron | A counterfactual approach to explanation in mathematics[END_REF], who analyze mathematical explanations by adapting the famous counterfactual account of causal explanations to the conceptual case.

In this paper we aim at proposing a novel approach to mathematical explanations, and this approach consists of two steps. The first amounts to the formalization of mathematical explanations with logical tools coming from proof-theory. In other words, we will study mathematical explanations by rewriting them with proof-trees 3 and by thus dwelling on their inner structure. Once this step is accomplished, we will move to the second one and show that all mathematical explanations re-arranged as proof-trees are such that their (undischarged) assumptions are conceptually less complex than their conclusion. In other words, we will take conceptual complexity to be the ingredient of our approach that provides the directionality or asymmetry which is typical of explanations, hence also of mathematical explanations. The interest and advantages of this approach with respect to previous ones will emerge naturally as we present it and will be anyway discussed in the course of the exposition.

The paper is structured as follows. We will use Section 2 to clarify how to move from informal mathematical proofs to proof-trees, while in Section 3 we will introduce the notion of conceptual complexity's increase in detail. Section 4 will serve to merge together proof-trees and the increase of conceptual complexity so to obtain our approach. In Section 5 we will put our model to a test on several cases-study of mathematical explanatory proof. Section 6 will finally serve to draw some conclusions.

2 From informal mathematical proofs to prooftrees

Internal mathematical explanations are mathematical proofs that seem to explain the theorems that they prove. However these proofs are often presented in an informal way, as is proper for the mathematical practice. One of the main features of our approach precisely consists in moving the analysis of mathematical explanations on a more structural level: our first step is thus to translate them into formal proofs. There exists a wide literature centered on rigor in mathematics that deals with the translation of informal mathematical proofs to formal ones, where formal proofs are thought of in terms of decomposition and verification processes. 4 Since our purposes are different from those of this literature, here we will adopt a conception of formal proofs which is closer to that which can be found in formal deductive systems. More precisely, we will look at formal proofs as trees in which the assumptions or premises of the mathematical proof are the leaves of the tree, the conclusion of the mathematical proof is the root of the tree, and each rule applied in the proof links the nodes corresponding to the premises of the rule to the node corresponding to the conclusion of the rule. Let us list some examples of proofs as tree-objects, where the nodes need to be substituted by sentences that are connected by the corresponding rule, indicated by ri.

Example (i)

• • r 5 • • • • r 4 • r 6 • • • r 2 • • • r 1 • r 3 • r 7 • r 8 Example (ii) • • • • r 4 • • r 5 • r 3 • • r 7 • • r 8 • • r 9 • • • r 10 • r 6 • r 2 • • r 16 • • • • r 14 • r 13 • • r 15 • r 12 • r 11 • r 1
In the case where the nodes are substituted by formulas of a formal language and the ri by appropriate logical rules, this notion of proof coincides with that of derivation in logic.

¬D

A B A ∧ B ∧I (A ∧ B) ∨ C ∨I ((A ∧ B) ∨ C) ∧ ¬D ∧I ¬¬(((A ∧ B) ∨ C) ∧ ¬D) A → ¬¬(((A ∧ B) ∨ C) ∧ ¬D) →I ¬¬
In this example we have a tree with two leaves, namely the assumptions B and ¬D; the root of the tree is the formula A → ¬¬(((A ∧ B) ∨ C) ∧ ¬D), and each logical rule (namely the rules ∧I, ∨I, ¬¬, → I) applied in the proof links the nodes corresponding to the premises of the rule to the node corresponding to the conclusion of the rule. We note, since it will be important later, that in this formal proof, by means of the rule → I, we have discharged the assumption A which has become the antecedent of the implication that occurs as the conclusion of the derivation. 5 We now turn to the illustration of two examples on how to move from mathematical explanations as informal proofs to mathematical explanations as proof-trees. To do so we choose as a case study one coming from Bernard Bolzano, a great if underestimated philosopher and mathematician, who can be seen as one of the pioneers in the study of mathematical explanations. 6 Amongst the numerous examples that can be found in his monumental Theory of Science (see [START_REF] Bolzano | Theory of Science[END_REF]), one which is at the same time simple 7 and illustrative for our purposes, concerns a property of quadrangles, and for this reason we call it the Quadrangle Theorem; it has the following form.

Quadrangle Theorem. The sum of the angles of any quadrangle is equal to 360 • . Explanatory proof. Consider the quadrangle ABCD. By Theorem (i), which says that any quadrangle can be divided into two triangles that have a common side, we can consider ABCD as the sum of the two triangles ABD and BCD. 8 But the sum of the 5 See for example [START_REF] Troelstra | Basic Proof Theory[END_REF]. 6 E.g. see Kitcher (1975). 7 In this paper we choose case studies which are fairly simple so that the reader can focus on the model we want to propose, rather than on the case studies themselves. This seems a common strategy in the literature, e.g., see [START_REF] Baron | A counterfactual approach to explanation in mathematics[END_REF], [START_REF] Weber | Explanatory proofs in mathematics[END_REF], [START_REF] Wilhelm | Comparing mathematical explanations[END_REF]. However, we believe that in order to ultimately evaluate the strength and robustness of any approach, the approach should be tested with more intricate examples, e.g. see [START_REF] Colyvan | Two flavors of mathematical explanation[END_REF]. Hence, a major path for future research is to test the approach with notable more complex examples, such as Desargues' theorem in projective geometry (see [START_REF] Lange | Because without cause[END_REF]) or the proof that there is no general solution in radicals for fifth-degree polynomial equations (see [START_REF] Pincock | The unsolvability of the quintic: A case study in abstract mathematical explanation[END_REF]).

8 See Figure 1. Hence the sum of the angles of the quadrangle ABCD is 180 According to Bolzano's analysis, we can argue that this proof displays the reason why the theorem is true; accordingly, we can draw the conclusion that this is an explanatory proof. In what follows, we use this proof as an example of how to formalize mathematical explanations by means of logical tools, in particular by means of proof-trees.

Generally speaking, a formalization can be developed in more than one way. One way could be radical: we could introduce a formal language which translates the sentences used in the informal proof and then use a natural deduction calculus in which we construct a derivation that reflects the form or the structure of the proof. Although this radical move could be revealing and interesting, it is not strictly necessary for our purposes. In particular, we can do without using a formal language; the only important feature for us is the tree structure that underlies the mathematical explanation, and to simplify our task, we will focus on it.

However, even restricting attention to the structure of proof-trees leaves open several possibilities, for it is always possible to formalize an informal proof with several different proof-trees, depending on the role assigned in the proof-tree to the components of the informal proof. Our approach relies on choosing a formalization that displays two features. On the one hand, the formalization needs to involve proof-trees with undischarged assumptions conveying properties that are linked and determine the truth of the theorem to prove. Why do we need undischarged assumptions to have such a specific form? If we think of an explanatory proof in informal terms, the only elements in it that could play the role of the grounds explaining why the theorem is true are the premise(s) on which the proof itself relies. In other terms, it seems quite natural to think that, in informal explanatory proofs, not only does the theorem follow from some premises, but also, and most importantly, the premises become the grounds or the reasons why the theorem is true. Now, if this is so, then in our formalization, undischarged assumptions -that typically correspond to premises of the proof -need to be such that they preserve this crucial role in a correct way. In other words, our formalization will involve undischarged assumptions that convey properties which are linked to those occurring in the theorem to prove: in this way, undischarged assumptions, in appropriate proofs, will play the role of the grounds or reasons why the theorem is true.

The second feature that the chosen formalization needs to display requires some previous notions to be properly introduced. To do so, we refer to the literature on scientific explanations, where there seems to be a wide consensus on what the keyingredients of an explanation are. Not only, as we would expect, cause and effect are necessarily part of an explanation, but also, laws or, as they are standardly called, generalizations need to be part of an explanation for it to count as such. So, for example, a (scientific) explanation of the fact that there is a fire in the forest is composed by the very same fact that there is a fire in the forest -the effect -the fact that a cigarette was lit in the forest -the cause -and the law of combustion which links the two and corresponds to the generalization. This view is shared by many different approaches on scientific explanation including the Deductive-Nomological model put forward by [START_REF] Hempel | Aspects of Scientific Explanation and Other Essays in the Philosophy of Science[END_REF], the Unionist account proposed [START_REF] Kitcher | Explanatory unification[END_REF], and the Counterfactual account defended by [START_REF] Woodward | Making Things Happen: A Theory of Causal Explanation[END_REF]. The main difference between these approaches does not concern the importance of laws or generalizations in scientific explanations but their precise role in the structure of explanations. So, for example, in the Deductive-Nomological account, as well as in the counterfactual account, both the cause and the generalization constitute the explanans of the explanation, while the effect the explanandum.

Mathematical explanations are a special kind of scientific explanation and as such they arguably share the same key components: ground(s) and conclusion, as analogue of cause(s) and effect, but also some type of generalizations. [START_REF] Poggiolesi | Conceptual (and hence mathematical) explanations, conceptual grounding and proof[END_REF] have discussed at length the need for generalizations in mathematical explanations, noting that generalizations are in a mathematical context different from laws; they rather amount to theorems or definitions which connect the ground and the conclusion of the mathematical explanation in question. In the explanatory proof of the Quadrangle Theorem, for example, the generalization at issue corresponds to Theorem (i), which states that any quadrangle can be seen as the sum of two triangles. The examples that we will treat in the next sections involve other generalizations.

What do generalizations have to do with the formalization of mathematical explanations as proof-trees? Our formalization will privilege proof-trees where at least some generalizations are used as rules. Whilst perhaps rare in studies of explanations,9 the idea that generalizations can fruitfully play roles analogous to rules is intuitively very natural. In an informal explanatory proof, certain generalizations are what connect the ground of the explanation to its conclusion. But if this is so, a formalization that aims at being faithful to the aspects of the informal proof is a formalization where generalizations play the role of rules, since rules have the function of justifying the connection between different elements of a proof. In other words, rules seem to be a perfect and solid way to reflect at the formal level the role that generalizations play in explanations.

Moreover, this potential role for generalizations has been put forward in related fields. There is an active and novel area of proof theory10 whose aim is to correctly transform theorems and definitions, written as statements, into rules. The idea of incorporating (some) generalizations as rules in our analysis of mathematical explanations is inspired by this research stream and relies on these results.

Finally, as we shall see shortly, the idea of capturing generalizations as rules is a central novel insight of our approach, with a subtle and deep relationship to some other parts of our model for mathematical explanations that shall be presented below. We shall return to them in this wider perspective in Section 4.

Taking into account the previous remarks, and given the following abbreviations -Qu(x) stands for x is a quadrangle, T r(x) stands for x is a triangle, and s.i.a(x) for the sum of the angles of x -this is the way we formalize the explanatory proof of the Quadrangle Theorem via a proof-tree:

( ( ( ( ( (

Qu(ABCD) T r(ABD) q-t T r(ABD) → s.i.a(ABD) = 180 • s.i.a(ABD) = 180 • M P π s.i.a(BCD) = 180 • s.i.a(ABCD) = 180 • + 180 • q-t+ Qu(ABCD) → s.i.a(ABCD) = 180 • + 180 • → I
where π is symmetric to the part of the proof-tree to its left:

( ( ( ( ( (

Qu(ABCD) T r(BCD) q-t T r(BCD) → s.i.a(BCD) = 180 • s.i.a(BCD) = 180 • M P
Let us now discuss the structure of the proof-tree with respect to the informal proof presented above. We begin our analysis with the top left inference in the proof-tree. This inference step is used to derive the fact that ABD is a triangle from the fact that ABCD is a quadrangle, via the rule that states that any quadrangle can be divided into two triangles. Then, the conclusion of this inference, which states that ABD is a triangle, is used along with the implication stating that, if ABD is a triangle, then the sum of its internal angles is 180 • , in order to conclude that the sum of the internal angles of ABD is 180 • . In the symmetric part of the proof-tree, the one above the formula s.i.a.(BCD) = 180 • , we have exactly the same kind of proof-tree, but applied to the triangle BCD. The proof-tree then proceeds, just as the informal proof does, by combining the two statements about the sum of the internal angles of ABD and BCD in order to conclude that the sum of the internal angles of ABCD is 360 • . We then discharge our assumption by means of the rule that introduces an implication and we obtain that if ABCD is a quadrangle, then the sum of the angles of ABCD is 180

• + 180 • .
The formalization of the informal explanatory proof of the Quadrangle Theorem seems to respect both desiderata: the generalization occurring in the informal proof occurs in the proof-tree not as a theorem, rather under the form of the two rules q-t and q-t+. Moreover, the proof-tree has two undischarged assumptions that convey properties linked to that conveyed by the conclusion of the proof-tree.

Le us now move to another example that yet again comes from [START_REF] Bolzano | On the Mathematical Method and Correspondence with Exner[END_REF]. In particular Bolzano used it to talk about the relation between ground and conclusion and illustrate its importance for mathematics. The example concerns a property of circles and for this reason we will call it the Circle Theorem.

Circle Theorem. Given two circles A and B, one with center a and radius ab, and Explanatory proof. Consider the circle A with center a and radius ab. 11 Since by definition a center is a point, then we have that there exists a point a. For the same reasoning applied to the circle B, we have that there exists a point b. But given a point a and a point b, there always exists a point c such that l(ab) = l(bc) = l(ac) (where l(xy) stands for the length of the segment xy). Hence we have a point c such that l(ab) = l(bc) = l(ac). Since the distance between c and the centre of the circle A is the radius of A, and the same holds for B, c is a point where the two circles A and B intersect.

Bolzano claims that this proof displays the reason why the theorem is true and thus constitutes an explanation of the theorem itself. We now formalize this proof by paying particular attention to its undischarged assumption as well as to the generalization. We will abbreviate as ϕ the formula Circ(A, a, ab) ∧ Circ(B, b, ab) while we will use Circ(X, x, xy) to stand for the statement that X is a circle with center x and radius xy. We also use P oint(x) to denote that x is a point. Consider the following proof-tree:

ϕ Circ(B, b, ab) ∧e P oint(b) c-p π P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc) ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc) →E ∃c P oint(c) ∧ c ∈ A ∧ c ∈ B ∧ l(ab) = l(ac) = l(bc) c-p+ ϕ → ∃c P oint(c) ∧ c ∈ A ∧ c ∈ B ∧ l(ab) = l(ac) = l(bc) → i 11 See Figure 2.
where π is ϕ Circ(A, a, ab) ∧e

P oint(a) c-p P oint(a) → (P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc)) P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc)

→E

Let us now discuss the structure of the proof-tree with respect to the informal proof presented above. The informal proof begins by considering the two points a and b mentioned in the statement of the theorem. In the proof-tree, this corresponds to the two uppermost inference steps concluding that a is a point and that b is a point, respectively, from the assumption ϕ. The informal proof proceeds then by employing the statement that, for any two points a and b, there exists a point c such that the distance between c and a and the distance between c and b is equal to ab. The proof-tree formalizes this step of the informal argument by the two consecutive applications of the rule that eliminates the implication.12 The premise of the uppermost right inference is indeed the statement P oint(a)

→ (P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc)).
The informal step arguing that c is the intersection point of the two circles A and B is formalized in the proof-tree by the inference marked as c-p+ and exploits the definition of circle as a set of points all equidistant from the centre. Finally, the last inference in the proof-tree enables us to explicitly integrate in the obtained statement the assumption ϕ of the theorem. Now we have a proof-tree that formalizes the informal proof in a way that meets our desiderata: the undischarged assumption conveys a property which is linked to the property conveyed by the root of the proof-tree. Moreover, the generalization occurring in the informal proof, and which amounts to the definition of a circle as the set of all points in a plane equidistant from another, called center (and where the segment from the center to any of them is called radius) is used in the proof-tree as a rule.

We conclude this section with two remarks on the links between informal and formal proofs. The first remark concerns the advantages of dealing with formal proofs rather than with informal ones, which are worth underlining. The move to formal proofs allows us to systematize, in a rigorous and clear manner, key elements of the informal proof: indeed, the conclusion of the informal proof becomes the root of the proof-tree, whilst the premises of the informal proof become the undischarged assumptions of the proof-tree. As for the role attributed to generalizations, they become the rules of the proof-tree. As already stressed, this is a natural role for generalizations in explanations and it represents a key element of our approach.

Secondly, let us analyze the structure of proof-trees formalizing explanatory mathematical proofs. [START_REF] Poggiolesi | On constructing a logic for the notion of complete and immediate formal grounding[END_REF][START_REF] Poggiolesi | Grounding rules for relevant implication[END_REF] proposes an account of explanatory (grounding) proofs in logic, identifying a strict dependency between the main logical connective of the root of the proof-tree, the structure of the proof-tree, and the explanatory steps that compose an explanation. We submit that a similar structure applies to the explanatory proofs of interest here, namely those in mathematics. The clarification of these dependencies in general requires technical notions that are spelled out in [START_REF] Poggiolesi | On constructing a logic for the notion of complete and immediate formal grounding[END_REF][START_REF] Poggiolesi | Grounding rules for relevant implication[END_REF]; we refer the reader to those papers for details, though the examples of the next sections should clarify the relevant points. For now, note that if we restrict our attention to roots of proof-trees whose main connective is an implication -this is often the case since many mathematical theorems have the form of implications -then proof-trees have the following form:

A, C1, . . . , Cn . . .

B A → B

where C1, . . . , Cn form a non-empty set of undischarged assumptions. If we look at the proof-trees formalizing the explanations of the Quadrangle Theorem or the Circle Theorem, they precisely display this structure, namely a derivation going from A, C1, .., Cn to A → B, where the A has been discharged, whilst the C1, ...Cn form a non-empty set of undischarged assumptions.

Let us stress once more the requirement of having a non-empty set of undischarged assumptions in a derivation formalizing an explanatory proof. Indeed, in this paper we target explanatory proofs that provide the grounds or the reasons why the theorem is true. In informal explanatory proofs, the role of the reasons why the theorem is true is played by the premises on which proofs rely. But in formal proof-trees, premises of proofs correspond to undischarged assumptions. Hence, if the set of undischarged assumptions were empty, namely if all assumptions in a derivation were discharged, then the derivation would not display the reasons why the theorem is true: it would correspond to a proof without premises, and therefore grounds. Hence, in our account the presence of undischarged assumptions is necessary.13 However, it is not sufficient: not any undischarged assumption can count as providing the reason why the theorem is true, but only those that can be shown to be conceptually less complex than the theorem itself. In the next section we will clarify what we mean by the expression conceptual complexity, whilst in Section 4 we will formulate our account in its final form.

Conceptual complexity

One of the central problems facing accounts of scientific explanation is the problem of explanatory asymmetries. The inability of several models of scientific explanation, amongst which is the famous Deductive-Nomological model, to handle the asymmetric structure of scientific explanations was a major reason for their rejection and the search for new accounts. As concerns mathematical explanations, the situation seems to be no different: as explanations, mathematical explanatory proofs have a directionality or asymmetry and any philosophical model should account for this feature. To see the challenge, consider the Circle Theorem where a property of the points explains a property of the circles. It does not take much to reverse the proof in such a way that from the property of the circles, we can infer a property of the points. Indeed we have:

Point Theorem. Given two points a and b, there always exists a third point c such that ab = bc= ac.

Proof. Consider the two points a and b and draw two circles A and B having as centre respectively a and b and both as radius ab. Given two circles of this sort, by the Circle Theorem, we have that they always intersect in a point c such that l(ca) = l(cb) = l(ab). Hence, there always exists a point c such that l(ab) = l(bc) = l(ac).

At the first glance the explanatory proof of the Circle Theorem and the proof just presented of the Point Theorem seem analogous: they both are short and simple, they both use the definition of circle as a set of points as one main ingredient, and they both explain a property by means of another property. However, their premises and conclusions are reversed and because of the asymmetry of explanations, the proofs cannot both be explanatory. The literature only indicates the proof of the Circle theorem as having an explanatory power, but the question remains: why this one and not the other? In other words, why is it the property of the points that explains the property of the circles and not the contrary? The answer to these questions is far from trivial: previous accounts of mathematical explanations might ignore the issue of the directionality of mathematical explanations -as for example the account of Steiner -or they might struggle to properly treat it. 14In this section, we propose a solution to this problem. It is neither novel nor original: on the contrary, it comes from a long and illustrious tradition of philosophers and mathematicians such as Aristotle,15 Proclus,16 Leibniz, 17 Bolzano, 18 Frege,19 to name but a few. According to this tradition,20 what determines the directionality or asymmetry of mathematical explanations amounts to an increase of conceptual complexity from its grounds to its conclusion; in other words, simpler grounds determine or explain a more complex conclusion whilst the opposite does not hold. This idea is natural and compelling; however, it displays two weaknesses. The first is that it crucially relies on the correct identification of the ground and the conclusion of a mathematical explanation. As we have already hinted, it is natural to think that in informal mathematical proofs, the grounds correspond to the premises on which the proofs rely. However, whilst it is relatively easy to identify the premises, and thus the grounds, on which proofs rely in simple mathematical proofs, in more complicated proofs this task turns out to be laborious and intricate. The formalization of mathematical explanations as proof-trees straightforwardly remedies this first weakness. Indeed, each element of the informal proof finds a rigorous formal counterpart: the premises, and hence the grounds of the mathematical explanation, become the undischarged assumptions, while the conclusion is its root. Moreover, the proof-tree structure itself provides a solid base to support the link between these elements.

The second weakness of the idea of conceptual complexity, as we inherit it from the tradition, lies in its generality and vagueness. What does it mean for the grounds to be simpler than their conclusion? How do we compare these elements? How do we compare the concepts that occur in them? Is the notion of (conceptual) complexity absolute or relative? Restricting the attention to the logical structure of formulas, we already have an answer to these questions via the elegant notions of logical complexity and related subformula property, which are cornerstones in proof theory. 21 It would be ideal to have the same rigorous notions in the mathematical context. However this is not possible: in a mathematical context what is at stake does not boil down to the structure of our sentences, but it mainly consists in the concepts we employ. Therefore, we will introduce a method to establish whether in a proof-tree there is an increase of conceptual complexity from its undischarged assumptions to its conclusion; in so doing we will encompass the notion of subformula and mimic it at the informal level.

Before introducing the method in detail, we first present the general insights that motivate it. The methods aims at comparing a set of sentences M and a sentence B occurring as undischarged assumptions and conclusion of a proof-tree, respectively; it does that by decomposing these sentences into their (basic) elements and drawing links among these elements. Now, there seems to be three sorts of ways in which elements, and more specifically concepts, can be related amongst each other. The first amounts to the situation where no link can be drawn because very simply the conclusion contains more elements than the undischarged assumptions. This is for example the case in any logical inferential step where a new logical constant is introduced. In these cases, we witness an increase in conceptual complexity (which encompasses logical complexity!), because all other elements being equal, a new concept tout court is introduced.

On the other hand, when relations amongst elements belonging to undischarged assumptions and conclusion of proof-trees can be drawn, we connect to a long tradition in philosophy,22 in considering them to be either intensional or extensional. In the mathematical case under study here, the intensional level taps into the way elements have been defined and thus considers two (or more) elements as related if there is a definition that links them. The extensional level, on the contrary, looks at the set of objects that the elements denote and thus considers two (or more) elements as related if there is a theorem that establishes a connection between the sets of objects that these concepts denote. Definitions and theorems are thus crucial to establish links amongst elements occurring in sentences under scrutiny, at the intensional and extensional level, respectively. But where do we find definitions and theorems that establish conceptual links amongst the elements of interest? And how can a concept be said to be more complex than another, once the connection is established? As for the first question, here is where generalizations in mathematical explanations become handy. Generalizations that occur in the proof-trees as rules provide the definitions or the theorems that connect the elements of the sentences under scrutiny. As for the second question, at both the intensional and extensional levels, it is the relation of containment that establishes an increase in conceptual complexity, although it works differently in each case. Indeed, at the intensional level, when a concept x is defined in terms of other concepts y1, ..., y1, then the concept x contains the concepts y1, ...yn as its components and the former is said be more complex than the latter. At the extensional level, on the other hand, when a concept x denotes a set of objects X which contains as a subset a set of objects Y that is related to the concept y, then y will be said to be more complex than x, because it is more specific.

The method that we will present provides indications on how to establish relations of increase of conceptual complexity amongst sentences occurring in proof-trees via their elements and in one or several of the ways just mentioned: intensional, extensional, or by means of the introduction of a novel element. In order to illustrate the method in the simplest way, we will divide it into steps and clarify each step on the following three examples. Each example is nothing but a proof-theoretic step with undischarged assumptions and conclusion since, as we have already said, but it is useful to repeat, our method can only compare sentences that occur in these roles in proof-trees.

Example (I) corresponds to the following proof-tree:

2 is an even number 2 is a prime number 2 is an even and prime number ∧I

In the above proof-tree the undischarged assumptions are the sentences "2 is an even number" and "2 is a prime number", and the conclusion is the sentence "2 is an even and prime number." The rule that allows the inference is the canonical rule that allows us to introduce the conjunction in the natural deduction calculus.

The second example, namely example (II), corresponds to the following proof-tree:

ABCD is a quadrangle ABCD is a polygon P ol

In the above proof-tree the undischarged assumption is the sentence "ABCD is a quadrangle," whilst the conclusion is the sentence "ABCD is a polygon." The rule that allows the inference is a rule based on the definition of polygon as the disjunction of any type of polygon, namely quadrangle, triangle, rectangle and so on.

The third example that we consider, namely example (III), corresponds to the proof-tree formalizing the explanation of the Quadrangle Theorem, constructed in the previous section. Its undischarged assumptions correspond to the sentences "if ABD is a triangle, then the sum of its angles is 180 • " and "if BCD is a triangle, then the sum of its angles is 180 • ", whilst the conclusion amounts to the sentence "if ABCD is a quadrangle, then the sum of its angles is 180 • + 180 • ."

We now have all the elements to introduce our method.

(1m) The first step of our method consists in dividing the sentences we aim at comparing, namely undischarged assumption(s) and conclusion occurring in a proof-tree, in their basic elements.

(I) We divide into basic elements the undischarged assumptions and conclusion of example (I); we thus have:

-2, even number, 2, prime number, -2, even number, and, prime number.

(II) We divide into basic elements the undischarged assumptions and conclusion of example (II); we thus have:

-ABCD, quadrangle, -ABCD, polygon.

(III) We divide into basic elements the undischarged assumptions and conclusion of example (II); we thus have:

if-then, ABC, triangle, the sum of its angles, 180 • , if-then, BCD, triangle, the sum of its angles, 180 • , if-then, ABCD, quadrangle, the sum of its angles, 180 • , +, 180 • .

(2m) The second step of our method consists in erasing those elements that are the same in each of the undischarged assumption(s) and the conclusion. 23(I) We consider the elements enumerated before and we erase those which are the same; we thus have:

-2, even number, 2, prime number, -2, even number, and, prime number.

(II) We do the same for the second example:

-ABCD, quadrangle, -ABCD, polygon.

(III) We do the same for the third example:

if-then, ABC, triangle, the sum of its angles, 180 • , if-then, BCD, triangle, the sum of its angles, 180 • , if-then, ABCD, quadrangle, the sum of its angles, 180 • , +, 180 • .

(3m) The third step of our method consists in examining which of the following scenarios holds, after the deletion of identical elements.

(3mA)-Intensional level. There exists an element x occurring in the conclusion, and elements y1, ..., yn occurring in the undischarged assumption(s) such that a definition occurring (explicitly or implicitly) in the proof-tree links them together; in particular, the definition establishes that x contains the elements y1, ..., yn as its components. If this is the case, then we can conclude that x is more complex than each of the y1, ..., yn.

Let us consider example (II), where the concept polygon occurs in the conclusion, while the concept quadrangle occurs in the (undischarged) assumption. According to the definition of polygon which is used in the proof-tree (in the form of a rule), polygon is seen as the disjunction of several geometrical figures amongst which is the quadrangle. Hence the concept of polygon contains the concept of quadrangle (at least in the proof-tree where the two concepts occur), and it is therefore more complex. This is also the case in (III) where the element ABCD occurs in the conclusion, while the elements ABD and BCD occur in the (undischarged) assumptions. But, according to the way these figures have been defined, both ABD and BCD are part of ABCD. Hence the element ABCD contains the elements ABD and BCD and it is therefore more complex.

(3mB)-Extensional level. There exists an element x occurring in the conclusion and an element y occurring in the undischarged assumption(s) such that, although there is no definition occurring in the proof-tree that links them together, there is a theorem occurring in the proof-tree as a rule that links the set of objects they denote, let us call them X and Y respectively. In particular, it can be established that Y is a subset of X , where X is a set generated from the elements of X. If this is the case, we claim that the element y is more complex than the element x because it is more specific as shown by the objects it denotes.

Let us clarify (3mB) by means of an example (others will follow in the forthcoming sections). Consider (III) where the conclusion contains the concept of quadrangle, while the undischarged assumptions contain the concept of triangle. There is no definition occurring in the proof that relates these two concepts, so it seems that there is no reason for us to consider the concept of quadrangle as more complex than the concept of triangle. However, things are different when we evaluate these concepts at the level of the objects they denote. According to Theorem (i), which occurs in the proof-tree as a rule, any quadrangle can be considered as the union of two triangles that share a side. Hence, according to this theorem, the set of all quadrangles is a subset of the set of all pairs of triangles, namely the subset of pairs of triangles with a common side. Note that the set of all pairs of triangles is generated by the set of triangles. As a result, the concept of quadrangle can be seen as more complex than the concept of triangle because more specific.

Another fruitful way to think of the extensional level is in terms of generality. A concept x is more general than a concept y when the set of objects Y denoted by the concept y is a subset of the set of objects X , which is generated from X, the set of objects denoted by x. Complexity and generality have long been seen as strictly related (see for example [START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF]. Indeed, according to Kant, complexity and generality are inversely related (see [START_REF] Ginammi | Bolzano, Kant, and the traditional theory of concepts, a computational investigation[END_REF]): less general concepts are, in a sense, more complex. As discussed in detail by Bolzano (see [START_REF] Roski | Bolzano's Conception of Grounding[END_REF]), this turns out to not be always true. It is, however, true in those cases covered by (3mB); for those concepts which are related at the extensional level, there is a natural way of thinking of them in terms of an increase of complexity, but also in terms of a decrease of generality. Consider the triangles -quadrangles example again. In this case, we move from the set of pairs of triangles to the set of pairs of triangles with a common side (i.e. quadrangles): not only do we read this relation in terms of an increase of complexity, but also it seems to involve a decrease of generality. Although a detailed discussion lies beyond the scope of this paper, there are plenty of examples of this sort in the literature on mathematical explanations, including:24 the concepts of product of imaginary numbers -product of two integers squares, Euler graph -Euler path, correlated equilibrium -Nash equilibrium, expressions of the form 10 5 a + 10 4 (a + d) + 10 3 (a + 2d) + 10 2 (a + 2d), where a, a + d, a + 2d are three integers in arithmetic progression -calculator numbers. In Section 5.2 dedicated to Pythagoras' theorem, we will encounter and discuss another notable example of this relation, namely that between similar triangles and right-angled triangles divided into two by the height.

(3mC)-Novelty level. The conclusion contains an element which is absent from the undischarged assumption(s) and cannot be related to any remaining element of the undischarged assumption either intensionally or extensionally. This is the case in (I), where the conclusion contains an and which is absent from the undischarged assumptions. This is also the case in (III), where the conclusion contains a + which is absent from the undischarged assumptions and cannot be related nor intensionally nor extensionally to any remaining element of the undischarged assumption.

(4m) The fourth and last step of our method consists in establishing that the conclusion is conceptually more complex than the undischarged assumption(s) if the third step is successful.

We have finished illustrating the method that indicates how to evaluate, from a perspective of increase in conceptual complexity, a set of sentences M and a sentence B, which occur as undischarged assumptions and conclusion, respectively, in a proof-tree. The method proposes an evaluation that passes through the elements of these sentences. First of all, the method only focuses on those elements that are worth comparing, getting rid of the others. Secondly, the method erases those elements that are the same between M and B: since they are identical, they need not to be taken into account. Finally, the method establishes links between the remaining elements either at the intensional or at the extensional level. The method also envisages the possibility of introducing new elements tout court. Although the dichotomy intensional-extensional is quite well-known in the philosophical literature, it is often the intensional side that has attracted philosophers' attention: starting from Aristotle (1984) -whose method has often been associated to the tree-like diagrams of [START_REF] Porphyry | Introduction, translated with a Commentary by Jonathan Barnes[END_REF] -we can find reflections on intensional relations amongst concepts in Proclus or Kant,25 as discussed in [START_REF] Harari | Methexis and geometrical reasoning in Proclus commentary on Euclides Elements[END_REF], [START_REF] Martijn | Proclus on the order of philosophy of nature[END_REF][START_REF] Ginammi | Bolzano, Kant, and the traditional theory of concepts, a computational investigation[END_REF]. However, in mathematics a great number of interesting cases of comparison among concepts do not seem to run along these lines. On the contrary, interesting mathematical results often connect concepts that, although unrelated at the intensional level, have an extensional connection. Moreover, this extensional connection can also be considered in terms of generality, where generality is a feature often associated with mathematical explanations, e.g. see [START_REF] Lange | Because without cause[END_REF]. Our method also encompasses this dimension.

Note that the notion of conceptual complexity that we use in our approach is not an absolute and objective measure (as notable supporters of the notion had imagined it to be, e.g., see [START_REF] Mancosu | Bolzano and Cournot on mathematical explanation[END_REF], but rather a notion relative to the mathematical theory in which the proof-tree is developed. Indeed, in order to check whether there is an increase of conceptual complexity from undischarged assumptions to conclusion, one needs to use theorems and definitions that occur in the proof-tree as rules. As we have clarified, it is precisely these theorems and definitions that establish relations of conceptual complexity between the elements contained in the undischarged assumptions and the conclusion of a proof-tree. But theorems and definitions presuppose a background theory they naturally belong to; therefore, the increase of conceptual complexity under our approach is ultimately relative to a theory in the context of which the mathematical explanation under consideration is formulated. 26Let us consider once more the example of the Circle Theorem to further clarify this point. In this example we take the concept of circle to be more complex than the concept of point. We establish such a relation because of the definition of a circle as a set of points, which occurs in the mathematical explanation of the Circle Theorem: under it, the concept of circle contains that of point, while the converse does not hold. It is of course possible to conceive of an alternative geometric theory containing a definition which establishes a different link between circles and points. In such a theory these concepts have different relationships as concerns complexity and the proofs which count as explanatory will also differ. However, this is not problematic for our approach precisely because it relies on a conception of complexity, and relatedly of mathematical explanation, which is relative to a mathematical theory. A mathematical explanation proceeds in a certain direction in virtue of the definitions and the theorems of the mathematical theory where it is developed and by means of which it is constructed.

Note that the case of the concept of circle and that of point is one of many. If for example we take the concept of line and the concept of point, we can either define a line as a set of points, or a point as the intersection of two lines. In the former case, the concept of line is more complex than that of point, in the latter case the concept of point is more complex than that of line. Does this mean that the notion of complexity we use is not asymmetric, i.e., that it is possible for a concept to be both more and less complex than another? As long as we think of complexity as relative to a mathematical theory, the answer is no. Indeed, as clarified in de Jongh and [START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF], each mathematical theory embraces and relies on one and only one order of concepts. Hence, each of the two previous definitions is contained in a different geometric theory in which it reflects the relation of complexity between the concepts of point and line. These relations 'order' the concepts of point and line differently, but each is asymmetric. In other words, although the order of concepts and thus complexity might shift from one theory to the other, there is no ambiguity about these notions inside a single theory.

Of course one might also be tempted to object that our relation of conceptual complexity is symmetric inside one and the same theory. 27 Consider the example of the triangle-quadrangle, that we have examined before. We have said that in the explanatory proof which contains these concepts, the relation of conceptual complexity between them is regulated by a theorem -that we called Theorem (i) -which states that any quadrangle can be seen as the sum of two triangles that share a side. In particular, following the instructions of point (3mb), we can use Theorem (i) to establish the complexity relation between quadrangles and triangles in the following way. We start from the concept of triangle (concept x), from which we generate the set of all pairs of triangles (set X ). Thanks to Theorem (i), we know that the set of all quadrangles (set Y ) is a subset of set X , namely it is the set of all pairs of triangles that share a side. This subset relation allows us to conclude that the concept of quadrangle is less general, and hence more complex, than the concept of triangle, via the objects that these concepts denote.

But, the objection would go, there is also another theorem (provable in the same theory!) -let us call it Theorem (ii) -stating that any triangle is the intersection of two suitably chosen quadrangles. Could Theorem (ii) not be used to establish that triangles are more complex than quadrangles? To see whether it can, it is enough to check whether the conditions of point (3mb) apply. We start from the concept of quadrangle (concept x), from which we generate the set of all pairs of quadrangles (set X ). Then we consider the set of all triangles (set Y ). For one to conclude that quadrangles are less complex than triangles according to (3mb), it needs to be shown that the set Y is a subset of X . However, Theorem (ii) only shows that triangles can be generated from a subset of X -namely, it can be generated from the subset of all pairs of quadrangles that intersect in a triangle, by mapping each pair of quadrangles to their intersection. In other terms, via Theorem (ii), it does not follow that the set Y of triangles is a subset of X : at most it follows that Y is isomorphic to a subset of X . That, however, is not sufficient to show that triangles are more complex than quadrangles; moreover, any other "method" for generating triangles from quadrangles comes up against a similar obstacle: it does not establish the claimed complexity relation between the two. Hence, analysis of this kind of case does not falsify the claim that the relation of conceptual complexity proposed in this paper is asymmetric inside a single theory.

We have started this section citing the problem of how to account for the directionality of scientific explanations in general, and of mathematical explanations in particular. As an example, we have used the Circle theorem and its explanatory proof. This proof relies on a definition of circle as a set of points and uses a property of points to explain a property of circles; however, we have shown that it is also possible to construct a proof that still relies on a definition of circle as a set of points, but uses a property of circles to explain a property of points. Beyond the fact that mathematicians only recognize the former proof as explanatory, is there anything else that allows us to make such a distinction? In this section, we have moved the first steps towards a solution: the increase in conceptual complexity from the undischarged assumptions to the conclusion of a proof-tree is what distinguishes an explanatory proof from one that it is not. As we will show in detail in Section 5, this solution fits with our example: while in the proof of the Circle theorem, we can witness an increase in conceptual complexity from top to bottom of the proof-tree that formalizes it, this is not so in the proof-tree that formalizes the Point theorem.

Proof-trees with increase of conceptual complexity

In Section 2, we have shown how to formalize mathematical proofs by means of prooftrees and in Section 3 we have introduced a method that indicates how to establish an increase in conceptual complexity from undischarged assumptions to conclusions of proof-trees. Armed with these ingredients, we can now formulate our account for mathematical explanations: a mathematical proof is explanatory, in the sense that it provides the reasons why the theorem it is proving is true, if, and only if, there exists a way to formalize it as a proof-tree with an increase in conceptual complexity from the (non-empty) undischarged assumptions to the conclusion.

As with every position expressed by an existential statement, this implies an asymmetry between the task of showing that a proof is explanatory as opposed to that of showing that it is not. In the former case, it suffices to find one formalization of the proof satisfying the desired characteristics; in the latter case, one needs to find arguments suggesting that there is no such formalization. Though the former task is at times far from trivial, the latter is clearly typically more difficult. This does not mean that it is impossible, since the informal proof places limits to the possible formalizations that need to be considered; indeed, in Section 5, we shall discuss an example that our account correctly identifies as non-explanatory proof. Note that we do not think of this asymmetry, nor the general difficulty in identifying explanatory or non-explanatory proofs, as a shortcoming of our approach; a philosophical model for mathematical explanations does not necessarily aim to distinguish specific mathematical proofs that explain from those that do not. This is rather a task for mathematicians. A philosophical model of mathematical explanation rather aims to clarify what makes certain proofs that mathematicians find explanatory so. With respect to this task, our model is satisfactory in that it says that a proof is explanatory as long as it can be formalized as a proof-tree where the undischarged assumption(s) is (are) conceptually less complex than the conclusion.

Our model is based on and unites a proof-theoretic approach to mathematical proofs and the idea of increase in conceptual complexity from top to bottom of proof-trees. It is important to emphasize that these two ideas go hand in hand. A proof-theoretic approach without the insight of an increase of conceptual complexity would just display the structure of mathematical proofs, without identifying where their explanatory power lies. Likewise the idea of conceptual complexity could not be successfully implemented without the support of the proof-theoretic machinery. Indeed, the increase of conceptual complexity only comes through the rules, and it is visible precisely because the relevant generalizations are present as rules rather than undischarged assumptions. But the focus on rules is exactly what characterizes the proof-tree structure approach to reasoning. Hence the symbiosis of rules-generalizations-complexity vindicates the proof-theoretic framework adopted here.

Finally, note that our model reproduces in the mathematical case some insights of the literature on scientific explanations. Just as scientific explanations are backed up by the relation of causation, here we take mathematical explanations to be backed by a grounding relation; in the same way as scientific explanations rely on laws that link causes and effect, here we take mathematical explanations to rely on relevant definitions and theorems that connect grounds and conclusion. In scientific explanations, the explanans is taken to be composed by the causes plus the law that link them to the effect, whilst the explanandum by the effect. Similarly here we might assume the explanans of mathematical explanations to be composed by the grounds plus the relevant definitions or theorems that link them to its conclusion, whilst the explanandum by the conclusion. Although grounds and generalizations both constitute the explanans of the mathematical explanations, thanks to the proof-theoretical framework, they can be differentiated: in proof-trees grounds have the role of undischarged assumptions, whilst generalizations the role of rules.

Putting our model to the test

We use this section to test our method with proofs of mathematical theorems that are thought of as explanatory. Firstly we will consider the proof of the Quadrangle Theorem, as well as the proof of the Circle Theorem, that we have already formalized in Section 2. In this section we will show that the trees that formally capture these proofs are indeed such that their undischarged assumptions are conceptually less complex than their conclusion. We will then move to Pythagoras' theorem. As it is famously known, there are several proofs of this theorem, but only the one that exploits the similarity of triangles is considered explanatory. We will show that we can formalize this proof by means of a proof-tree where the undischarged assumptions are conceptually less complex than the conclusion.

Quadrangle Theorem, Circle Theorem and Point Theorem

In Section 2 we have introduced the Quadrangle Theorem and the Circle Theorem together with their respective explanatory proofs. We have illustrated how to formalize these proofs using proof-trees. Now we have all the means to complete our analysis and show that in both these proof-trees, the undischarged assumptions are conceptually less complex than their respective conclusion. Indeed, if this is the case, then the informal proofs can be considered as explanatory.

Let us start with the Quadrangle Theorem. Recall that the proof-tree formalizing its explanatory proof (see Section 2) has the following undischarged assumptions:

(i) if ABD is a triangle, then the sum of its angles is 180 • , (ii) if BCD is a triangle, then the sum of its angles is 180 • , as well as the following conclusion (iii) if ABCD is a quadrangle, the the sum of its angles is 180

• +180 • .
Sentences (i)-(iii) constituted our example (III) in Section 3. In that context, we have observed that sentences (i) and (ii) either contain the same elements as (iii) (if-then, the sum of the angles, 180 • ), or they contain elements that by definition are simpler than elements of sentence (iii) (ABC, BCD and ABCD), or they contain elements that are extensionally less complex than elements of sentence (iii) (triangle, quadrangle). Hence, sentences (i) and (ii) are conceptually simpler than sentence (iii). As a conclusion, we have that the proof of the Quadrangle Theorem that Bolzano considered as explanatory, is actually explanatory according to our account, since there exists a formalization of this proof as a proof-tree where the undischarged assumptions are less complex than the conclusion.

Thanks to our analysis, not only can we confirm Bolzano's insight, but also we are able to identify, with clarity and rigor, the grounds and the conclusion of this explanation: they correspond to the undischarged assumptions and conclusion of the proof-tree, respectively. The fact that the sum of the angles of a triangle is 180 • is the reason why the sum of the angles of a quadrangle is 360 • ; in other words, a property of triangles grounds or is the reason why a property of quadrangles holds, via the theorem stating that any quadrangle can be divided into two triangles.

Let us now move to the explanatory proof of the Circle Theorem. The undischarged assumption of the proof-tree formalizing this explanation (see Section 2) is the following sentence:

(i) if a and b are points, then there exists another point c such that l(ab) = l(ac) = l(bc),

as well as its conclusion, which is the sentence:

(ii) if A is a circle with center a and radius ab, and B is a circle with center b and radius ab, then there exists an intersection point c such that l(ab) = l(ac) = l(bc).

We need to establish whether the conclusion is more complex than the undischarged assumption, and for this goal we use our method. Hence, first of all, we divide the two sentences into their basic elements; we thus have:

(i) if-then, a, if-then, b, point, there exists, c, point, l(ab) = l(ac) = l(bc), (ii) if-then, A, and, B, a, b, circle, radius, center, there exists, intersection point, c, l(ab) = l(ac) = l(bc).

Then we erase those elements which are identical:

(i) if-then, a, if-then, b, point, there exists, c, point, l(ab) = l(ac) = l(bc)

(ii) if-then, A, and, B, a, b, circle, radius, center, there exists, intersection point, c, l(ab) = l(ac) = l(bc)

Finally we analyze the remaining elements of sentences (i) and (ii), and we find out that:

(3mA) The concepts of circle, center, radius and intersection point occur in sentence (ii), which is the root of the proof-tree, and are all related to the concept of point, that occurs in sentence (i), which is the undischarged leaf of the proof-tree; they are connected via the definition (used in the proof-tree) of circle as the set of all points in a plane equidistant from another, called the center and where the segment from the center to any of them is called the radius. More precisely, each of the concepts circle, center, radius and intersection point contain that of point by definition.

(3mC) the conclusion contains the elements and, A, B that are new and not related to any remaining element of the assumption.

Since sentence (ii), which is the theorem we want to prove, either contains elements which already occur in sentence (i) (i.e., the undischarged assumption) or contains new elements or elements that by definition contain others occurring in sentence (i), we can establish that the conclusion of our proof-tree is conceptually more complex than the undischarged assumption and hence that the proof of the Circle Theorem is actually explanatory.

Not only does our approach vindicate and systematize Bolzano's intuitions, but also it allows us to dig deeper into them and study in detail the structure of the explanation that he identified. For example, it allows us to clearly say what the ground of this explanation is: it amounts to the fact that, given two points, there always exists a third that forms with them an equilateral triangle. This is the reason why it is the case that, given two circles such that the line between them is a radius for both, these circles always intersect in a point that forms with their centers an equilateral triangle. This analysis confirms Bolzano's conjecture:

So for example the proof of the first proposition of Euclid's Elements (on the possibility of an equilateral triangle), according to the opinion of all mathematicians is direct. However, does it show the ground of the truth to be established? Is an equilateral triangle possible only on account of the intersection of these circles, or is it not, on the contrary, rather that the circles intersect because there is an equilateral triangle? (Bolzano, 2004, §13) We close this section by briefly showing that the steps that have led us to argue for the explanatory power of the proof of the Circle Theorem, can also be used to argue that the proof of the Point Theorem is not explanatory.

We start by formalizing the proof of the Point theorem (see Section 3) with the help of the proof-tree structure. In particular, we adopt the same formal language employed for the formalization of the Circle theorem and we denote with ψ the following formula:

∃c P oint(c) ∧ c ∈ A ∧ c ∈ B ∧ l(ab) = l(ac) = l(bc).
We thus obtain the following proof-tree:

P oint(b) Circ(B, b, ab) (c -p) * P oint(a) Circ(A, a, ab) (c -p) * Circ(A, a, ab) → (Circ(B, b, ab) → ψ) Circ(B, b, ab) → ψ → E ∃c P oint(c) ∧ c ∈ A ∧ c ∈ B ∧ l(ab) = l(ac) = l(bc) → E ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc) (c -p+) * P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc) → I P oint(a) → (P oint(b) → ∃c P oint(c) ∧ l(ab) = l(ac) = l(bc)) → I
We briefly discuss the structure of the proof-tree, also with respect to the informal proof that the proof-tree is supposed to formalize. The informal proof begins by considering the two points a and b mentioned in the statement of the theorem. In the proof-tree, this corresponds to the two uppermost leaves from which we conclude that we can construct two circles, one with center in a and radius ab, the other with center in b and radius ab. From this and the assumption saying that if A is a circle having center in a and radius ab, and B is a circle having center in b and radius ab, then these circles always intersect in a point c such that l(ab) = l(bc) = l(ca); by a double application of the rule that eliminates the implication,28 we obtain that there exists an intersecting point c such that l(ab) = l(ac) = l(bc). From this, we can infer that we have a point c such that l(ab) = l(ac) = l(bc). Then, by a double application of the rule that introduces the implication, we obtain the desired conclusion.

The proof-tree formalizing the proof of the Point Theorem is analogous to the proof-tree formalizing the proof of Circle Theorem: they both have the same structure, they both display undischarged assumptions which convey properties linked to those of the theorems they prove, and they both use the same generalization, namely the definition of circle as set of points. However, the undischarged assumption and the conclusion of the proof-tree for the Circle Theorem correspond to the conclusion and undischarged assumption of the proof-tree for the Point Theorem, respectively. As our method has shown that in the first case there is an increase of conceptual complexity from top to bottom of the proof-tree, by an analogous analysis, it is easy to observe a decrease of conceptual complexity from top to bottom of the proof-tree for the Point Theorem. It seems reasonable to conclude29 that the proof of the Point Theorem is not explanatory. Thanks to our method, we can justify our claim: a property of the circles cannot explain a property of the point because, at least according to the definition used in the proof, the former are more complex than the latter.

Pythagoras' Theorem

We use this section to treat Pythagoras' Theorem by means of our method. In the literature on mathematical explanation, there is a proof that is based on the similarity of triangles that is often considered as a legitimate explanation of Pythagoras' Theorem: this was first noticed by the mathematician [START_REF] Bouligand | Premières leçons sur la théorie générale des groupes[END_REF], and the further discussed by [START_REF] Steiner | Mathematical explanation[END_REF] and [START_REF] Mancosu | Mathematical explanation: Problems and prospects[END_REF]. We will show that there is a way to formalize this proof by means of a proof-tree where the undischarged assumptions are conceptually less complex than their conclusion, i.e., we will show that according to our method this is indeed a proof that can be regarded as an explanation.

Pythagoras' Theorem. For any right triangle ABC with the right angle on A, the square BC 2 on the hypotenuse BC equals the sum of the squares AB 2 and AC 2 on the other sides AB and AC of the triangle.

Explanatory proof. Consider any right triangle ABC with the right angle on A and let AH be its height with respect to the hypotenuse BC, as shown in Figure 3. First, we notice that the triangle AHC contained in ABC is similar to ABC itself since they both have a right angle and they both share the angle on C. 30 The similarity between the triangles ABC and AHC implies the following equality of ratios:

AC BC = CH AC
which can in its turn be expressed in the following way: AC 2 = CH • BC. Symmetrically, the triangle ABH contained in ABC is similar to ABC itself since they both have a right angle and they both share the angle on B. The similarity between the triangles ABC and ABH implies the equality of ratios As we have done before, let us dwell on this proof and let us identifying its main components. On the one hand, it contains a conclusion -the sentence "if ABC is a right triangle, then AC 2 + AB 2 = BC 2 " -but also some premises, namely the sentences concerning the fact that if two triangles are similar, then they have a certain equality of ratios. Finally, the proof appeals to a general property, namely the fact that right triangles can be seen as composed by two similar triangles.

Let us now move to the formal level. In order to simplify our task, let us use the following denotation: RT r(x ∼ y/ /z) stands for x is a right triangle, divided into triangles y and z by the height, while Sim(x, y) stands for x and y are similar triangles. We can then formalize the previous proof by the following proof-tree: The first step of the informal proof, by which we infer that the triangle ABC is similar to the triangle AHC, is formally represented by the uppermost inference step in the proof-tree π0, in which we conclude Sim(ABC, AHC) from the hypothesis that ABC is a right triangle, divided in the triangles AHC and AHB by the height. In order to make this inference, we use, as a rule, a general property of right triangles, which says that any such triangle, seen as divided into two triangles by the height, is similar to both of them. 31 The following inference step in the proof-tree π0 allows us to derive, by modus ponens, the conclusion AC 2 = CH • BC from the previously obtained conclusion Sim(ABC, AHC) together with the implication Sim(ABC, AHC) → AC 2 = CH • BC. The symmetric argument for the pair of triangles ABC and AHB, which yields the equality AB 2 = BH • BC, is similarly formalized by the proof-tree π1. The formal proof continues by combining the two obtained equalities AC 2 = CH • BC and AB 2 = BH • BC into the equality AC 2 + AB 2 = CH • BC + BH • BC by the introduction of the symbol +. Then, we rewrite AC 2 + AB 2 = (CH + BH)(BC) as AC 2 + AB 2 = BC 2 . The last inference step of the proof corresponds to the discharge of the assumption by means of the rule that introduces the implication.

the set of all right-angled triangles divided into two triangles by the height is a subset of similar triangles. Hence the concept right-angled triangle divided into two triangles by the height is more complex than the concept similar triangles because more specific at the extensional level: we pass from similar triangles to similar triangles such that, united, they form another (right) triangle that is similar to both.32 (3mC) the conclusion contains the element + which is new and not related to any remaining element of the assumption.

Since the conclusion of the proof-tree formalizing the proof of Pythagoras' Theorem either contains elements which already occur in the undischarged assumptions of the proof-tree, or a new element, or elements that are more complex that those occurring in the assumptions either by definition or via the objects they denote, we can establish that the conclusion is conceptually more complex than the undischarged assumptions and hence that the proof of Pythagoras' Theorem is actually explanatory.

Our method confirms what has been previously noted by [START_REF] Steiner | Mathematical explanation[END_REF] and [START_REF] Mancosu | Mathematical explanation: Problems and prospects[END_REF]; moreover it adds new elements to their analysis. It is indeed able to specify -via the logical formalization of the explanatory proof -the structure of the explanation, the role that generalizations play in the explanation, and, last but not least, the grounds and relative conclusion of the explanation, which amount to the (undischarged) assumptions and the root of the proof-tree, respectively. Our analysis of Pythagoras' explanatory proof shows us with rigor how the explanation works: the fact that in right-angled triangles the square of the hypothenuse is equal to the sum of the square of each side is grounded by certain ratios amongst similar triangles, via the fact that any right-angled triangle is similar to both triangles in which it can be divided by the height.

Our analysis of Pythagoras' Theorem yields a structure that is similar to that which emerges for the explanatory proof of the Quadrangle Theorem. In this theorem, a property of quadrangles is grounded by a property of triangles via a theorem that connects quadrangles and triangles, namely via the objects that these concepts denote. Similarly, in Pythagoras' Theorem, a property of right-angled triangles divided into two by their height is explained by a property of similar triangles via a theorem that connects similar triangles with right-angled triangles divided into two by their height via the objects that these concepts denote.

Conclusions

When it comes to scientific explanations, and thus also mathematical explanations, one can distinguish two different perspectives, namely the ontic or the epistemic perspective. Whereas for the latter perspective, explanations are mainly activities which generate understanding, the ontic perspective will look for some systematic pattern of objective dependence relations which explanations track or can be identified with (e.g. see [START_REF] Kim | Explanatory knowledge and metaphysical dependence[END_REF], [START_REF] Inglis | Functional explanation in mathematics[END_REF]).

In this paper, we have concentrated on the ontic perspective on explanations, by introducing a novel approach for mathematical explanations that is based on two ingredients: the move from informal proofs to proof-trees and the increase of conceptual complexity from the undischarged assumptions to the conclusion of such proof-trees. In other words, in this paper we have proposed a novel approach which, although it stems from mathematical practice, insofar as it is tested with examples of proofs that mathematicians find explanatory, does not necessarily aim at capturing the way in which mathematicians make statements about the explanatoriness of proofs. Rather, the main goal of the approach is to capture what the several different proofs that mathematicians find explanatory have in common, namely their shared and underlying features. In this respect, we believe that our approach brings clear advantages: it identifies the structure of explanatory proofs, it isolates their grounds and conclusion, and finally it accounts explicitly for their asymmetry. Moreover, it adopts and relies on a standpoint that brings mathematical explanations closer to scientific explanations. Because of these many virtues, we think that it might represent the basis for a new and interesting way of looking at mathematical explanations.

Figure 1 :

 1 Figure 1: A quadrangle divided into two triangles

Figure 2 :

 2 Figure 2: Equidistant points A, B and C

Figure 3 :

 3 Figure 3: A right triangle with height AH

Some exceptions are[START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF],[START_REF] Mancosu | Bolzano and Cournot on mathematical explanation[END_REF],Pincock (2015a),[START_REF] Poggiolesi | Conceptual (and hence mathematical) explanations, conceptual grounding and proof[END_REF].

In this paper, we use as synonymous the words "ground" and "reason." However, we do not take grounding to be a metaphysical relation as it is commonly assumed to be in the contemporary literature, e.g. see[START_REF] Fine | Guide to ground[END_REF]. In this paper we rather think of the notion of conceptual ground, which has been receiving an increasing attention recently, e.g.,[START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF],Poggiolesi and Genco (2023), Smithson (2020).

In this respect our approach is similar to the one of[START_REF] Wilhelm | Comparing mathematical explanations[END_REF]. However, two important differences prevent us from a stricter comparison. First, while, as we will show in the next section, we use the resources of natural deduction calculi, which allow a fine-grained analysis of the structure of proofs, Willhelm uses the resources of Hilbert systems. Moreover, he only puts forwards an approach for comparing explanatoriness of different proofs.

E.g. see[START_REF] Avigad | Mathematical method and proof[END_REF][START_REF] De Block | Mathematical rigor and proof[END_REF].

E.g. see[START_REF] Jansson | Explanatory asymmetries: Laws of nature rehabilitated[END_REF]Jansson ( , 2017a)).

See Ciabattoni et al. (2008),[START_REF] Marin | Synthetic inference rules for geometric theories[END_REF].

For any reference to the logical rules concerning introducing or eliminating logical connectives, see for example[START_REF] Troelstra | Basic Proof Theory[END_REF].

There is an extensive logical literature concerning the form of explanatory derivations in logic and the crucial role of undischarged assumptions in these derivations, see for example[START_REF] Genco | Formal explanations as logical derivations[END_REF],[START_REF] Poggiolesi | On constructing a logic for the notion of complete and immediate formal grounding[END_REF][START_REF] Poggiolesi | Grounding rules for relevant implication[END_REF]. Note that this literature also deals with truths that might be quite complicated, for which it is possible to construct derivations that display immediate and mediate reasons or grounds (on the distinction between immediate and mediate grounds see again[START_REF] Genco | Formal explanations as logical derivations[END_REF],[START_REF] Poggiolesi | On constructing a logic for the notion of complete and immediate formal grounding[END_REF][START_REF] Poggiolesi | Grounding rules for relevant implication[END_REF]).

See for example Lange (2022) on the counterfactual account.

E.g. see[START_REF] Harari | Methexis and geometrical reasoning in Proclus commentary on Euclides Elements[END_REF].

E.g. see[START_REF] Martijn | Proclus on the order of philosophy of nature[END_REF].

E.g. see[START_REF] Belaval | Leibniz, critique de Descartes[END_REF].

E.g. see[START_REF] Betti | Explanation in metaphysics and Bolzano's theory of ground and consequence[END_REF],[START_REF] Sebestik | Logique et mathematique chez Bernard Bolzano[END_REF].

E.g. see[START_REF] Detlefsen | Fregean hierarchies and mathematical explanation[END_REF].

An excellent paper introducing in a clear way this tradition and its main ideas is[START_REF] Detlefsen | Fregean hierarchies and mathematical explanation[END_REF].

E.g. see[START_REF] Poggiolesi | On the importance of being analytic. The paradigmatic case of the logic of proofs[END_REF],[START_REF] Troelstra | Basic Proof Theory[END_REF].

See for instance[START_REF] Margolis | Concepts[END_REF].

Note that in case of negated sentences the situation is slightly more complicated; see[START_REF] Poggiolesi | On defining the notion of complete and immediate formal grounding[END_REF].

E.g., see[START_REF] Avigad | Mathematical method and proof[END_REF],[START_REF] Lange | Because without cause[END_REF].

Although neither Proclus nor Kant framed their discussion on concepts in terms of the distinction between intensional and extensional level, we can nowadays assert that they both were thinking of concepts in an intensional perspective.

The idea of considering explanatory relations in the context of a theory is not new, e.g. see[START_REF] Hempel | The function of general laws in history[END_REF],[START_REF] Jansson | Explanatory asymmetries, ground, and ontological dependence[END_REF].

We thank an anonymous referee for raising up this point.

E.g. see[START_REF] Troelstra | Basic Proof Theory[END_REF].

Although we have not tested all possible formalizations of the Point theorem, our conclusion sounds reasonable.

Since by fixing two angles of a triangle, we also fix the third, the equality of the two right angles of the two triangles and of their angle on C implies that the angle on B of ABC and the angle on A of AHC are equal, which, by the definition of similarity, implies that the two triangles are similar.

In other words, any triangle whatsoever can be divided into two triangles by the height, but only right triangles are such that the original one is similar to both.

In line with we have said above, we can also look at the link between similar triangles-right angled triangle divided into triangles by the height in terms of generality: the former concept is indeed more general than the latter.

Acknowledgments

We would like to thank F. A. Genco and W. H. Holliday for their many, bright and rigorous comments over earlier versions of the paper. A special thank goes to B. Hill to whom we owe the insight of looking at complexity from an extensional point of view. Plus we are in debt with him for the several discussions over the notion of mathematical explanation. We finally would like to thank the Editor R. S. D. Thomas for his feedback and precision through the whole editorial process.

Now we have a proof-tree that formalizes the informal proof and systematizes its keyelements: the undischarged assumptions amount to the premises of the mathematical proof, the root to the conclusion, and the general property occurring in the informal proof as a theorem has been used as a rule in the proof-tree. The proof-tree share the same structure displayed before, namely:

However, in order to conclude that such proof-tree formalizes an explanatory informal proof, we have to show that its undischarged assumptions, namely the sentences:

(i) if AHC and ABC are similar triangles, then AC 2 = CH • BC, (ii) if AHB and ABC are similar triangles, then AB 2 = BH • BC, are conceptually simpler than its root, namely the sentence:

(iii) if ABC is a right triangle divided by its height into two triangles AHC and AHB , then

In order to accomplish this task, we use our method. So first we divide these sentences in their basic elements, namely: (3mB) Sentence (iii) contains the concept right-angled triangle divided into two triangles by the height, while sentences (i) and (ii) contain the concept similar triangles.

There is no explicit definition in the proof-tree that links these two concepts. Hence there seems to be no reason to think that the former is related to and more complex than the latter. On the other hand, there is a property of right-angled triangles, telling us that any such triangle is similar to both triangles obtained by dividing it by the height, which is involved in the proof and it implies that


T Manos

Ch Skokos

T Bountis

Application of the Generalized Alignment Index (GALI) method to the dynamics of multi-dimensional symplectic maps

Keywords: Symplectic maps, Chaotic motion, Regular motion, GALI method

We study the phase space dynamics of multi-dimensional symplectic maps, using the method of the Generalized Alignment Index (GALI). In particular, we investigate the behavior of the GALI for a system of N = 3 coupled standard maps and show that it provides an efficient criterion for rapidly distinguishing between regular and chaotic motion.

Introduction

The distinction between regular and chaotic motion in conservative dynamical systems is fundamental in many areas of applied sciences. This distinction is particularly difficult in systems with many degrees of freedom, basically because it is not feasible to visualize their phase space. Thus, we need fast and accurate tools to obtain information about the chaotic vs. regular nature of the orbits of such systems and characterize efficiently large domains in their phase space as ordered, chaotic, or "sticky" (which lie between order and chaos).

In this paper we focus our attention on the method of the Generalized ALignment Index (GALI), which was recently introduced and applied successfully for the distinction between regular and chaotic motion in Hamiltonian systems. 1 The GALI method is a generalization of the Smaller Alignment Index (SALI) technique of chaos detection. [2][3][4] We present some preliminary results of the application of GALIs on the dynamical study of symplectic maps, considering in particular the case of a 6-dimensional (6D) system of three coupled standard maps. 5 It is important to note that maps of this type have been extensively studied in connection with the problem of the stability of hadron beams in high energy accelerators, see 6 and references therein.

Our numerical results reported here verify the theoretically predicted behavior of GALIs obtained in 1 for Hamiltonian systems. In addition we study in more detail the behavior of chaotic orbits which visit different regions of chaoticity in the phase space of our system.

Definition and behavior of GALI

Let us first briefly recall the definition of GALI and its behavior for regular and chaotic motion, adjusting the results obtained in 1 to symplectic maps. Considering a 2N -dimensional map, we follow the evolution of an orbit (using the equations of the map) together with k initially linearly independent deviation vectors of this orbit -→ ν 1 , -→ ν 2 , ..., -→ ν k with 2 ≤ k ≤ 2N (using the equations of the tangent map). The Generalized ALignment Index of order k is defined as the norm of the wedge or exterior product of the k unit deviation vectors:

GALI k (n) = ν1 (n) ∧ ν2 (n) ∧ ... ∧ νk (n) (1)
and corresponds to the volume of the generalized parallelepiped, whose edges are these k vectors. We note that the hat (ˆ) over a vector denotes that it is of unit magnitude and that n is the discrete time.

In the case of a chaotic orbit all deviation vectors tend to become linearly dependent, aligning in the direction of the eigenvector which corresponds to the maximal Lyapunov exponent and GALI k tends to zero exponentially following the law:

1 GALI k (n) ∝ e -[(σ1-σ2)+(σ1-σ3)+...+(σ1-σ k )]n , (2)
where σ 1 , . . . , σ k are approximations of the first k largest Lyapunov exponents. In the case of regular motion on the other hand, all deviation vectors tend to fall on the N -dimensional tangent space of the torus on which the motion lies. Thus, if we start with k ≤ N general deviation vectors they will remain linearly independent on the N -dimensional tangent space of the torus, since there is no particular reason for them to become aligned. As a consequence GALI k remains practically constant for k ≤ N . On the other hand, GALI k tends to zero for k > N , since some deviation vectors will eventually become linearly dependent, following a power law which depends on the dimensionality of the torus on which the motion lies and on the number m (m ≤ N and m ≤ k) of deviation vectors initially tangent to this torus. So, the behavior of GALI k for regular orbits is given by 1,7

GALI k (n) ∝    constant if 2 ≤ k ≤ N 1 n 2(k-N )-m if N < k ≤ 2N and 0 ≤ m < k -N 1 n k-N if N < k ≤ 2N and m ≥ k -N .
(3)

Dynamical study of a 6D standard map

As a model for our study we consider the 6D map:

x ′ 1 = x 1 + x ′ 2 x ′ 2 = x 2 + K 2π sin(2πx 1 ) -β 2π {sin[2π(x 5 -x 1 )] + sin[2π(x 3 -x 1 )]} x ′ 3 = x 3 + x ′ 4 x ′ 4 = x 4 + K 2π sin(2πx 3 ) -β 2π {sin[2π(x 1 -x 3 )] + sin[2π(x 5 -x 3 )]} x ′ 5 = x 5 + x ′ 6 x ′ 6 = x 6 + K 2π sin(2πx 5 ) -β 2π {sin[2π(x 1 -x 5 )] + sin[2π(x 3 -x 5 )]} (4)
which consists of three coupled standard maps 5 and is a typical nonlinear system, in which regions of chaotic and quasi-periodic dynamics are found to coexist. Note that each coordinate is given modulo 1 and that in our study we fix the parameters of the map (4) to K = 3 and β = 0.1.

In order to verify numerically the validity of equations ( 2) and (3), we shall consider two typical orbits of map ( 4), a chaotic one with initial condition x 1 = x 3 = x 5 = 0.8, x 2 = 0.05, x 4 = 0.21, x 6 = 0.01 (orbit C1) and a regular one with initial condition x 1 = x 3 = x 5 = 0.55, x 2 = 0.05, x 4 = 0.01, x 6 = 0 (orbit R1). In figure 1 we see the evolution of GALI k , k = 2, . . . , 6, for these two orbits.

It is well-known that in the case of symplectic maps the Lyapunov exponents are ordered in pairs of opposite signs. [START_REF] Lieberman | Regular and Chaotic Dynamics[END_REF] Thus, for a chaotic orbit of the 6D map (4) we have

σ 1 = -σ 6 , σ 2 = -σ 5 , σ 3 = -σ 4 with σ 1 ≥ σ 2 ≥ σ 3 ≥ 0. So for the evolution of GALI k , equation (2) gives GALI 2 (n) ∝ e -(σ1-σ2)n , GALI 3 (n) ∝ e -(2σ1-σ2-σ3)n , GALI 4 (n) ∝ e -(3σ1-σ2)n , GALI 5 (n) ∝ e -4σ1n , GALI 6 (n) ∝ e -6σ1n .
(5) The positive Lyapunov exponents of the chaotic orbit C1 were found to be σ 1 ≈ 0.70, σ 2 ≈ 0.57, σ 3 ≈ 0.32. From the results of figure 1a) we see that the functions of equation ( 5) for σ 1 = 0.70, σ 2 = 0.57, σ 3 = 0.32 approximate quite accurately the computed values of GALIs.

For the regular orbit R1 we first considered the general case where no initial deviation vector is tangent to the torus where the orbit lies. Thus,

-(σ 1 -σ 2 )n , e -(2σ 1 -σ 2 -σ 3 )n , e -(3σ 1 -σ 2 )
n , e -4σ 1 n , e -6σ 1 n for σ 1 = 0.70, σ 2 = 0.57, σ 3 = 0.32 in a) and proportional to n -2 , n -4 , n -6 in b).

for the behavior of GALI k , k = 2, . . . , 6, equation (3) yields for m = 0

GALI 2 (n) ∝ constant, GALI 3 (n) ∝ constant, GALI 4 (n) ∝ 1 n 2 , GALI 5 (n) ∝ 1 n 4 , GALI 6 (n) ∝ 1 n 6 . (6)
From the results of figure 1b) we see that the approximations appearing in (6) describe very well the evolution of GALIs.

In order to verify the validity of equation ( 3) for 1 ≤ m ≤ 3, in the case of regular motion, we evolve orbit R1 and three random initial deviation vectors for a large number of iterations (in our case for 5 × 10 7 iterations), in order for the three deviation vectors to fall on the tangent space of the torus. Considering the current coordinates of the orbit as initial conditions and using m = 1 or m = 2 or m = 3 of these vectors (that lie on the tangent space of the torus) as initial deviation vectors we start the computation of GALIs' evolution. We note that the rest 6m initial deviation vectors needed for our computation are randomly generated so that they do not lie on the tangent space of the torus. The results of these calculations are presented in figure 2, where the evolution of GALI k , k = 2, . . . , 6, for different values of m is plotted. Figure 2 clearly illustrates that equation (3) describes accurately the behavior of GALIs for regular motion also in the case where some of the initial deviation vectors are chosen in the tangent space of the torus. Let us now consider the case of a chaotic orbit which visits different regions of chaoticity in the phase space of the map. The orbit with initial conditions x 1 = x 3 = x 5 = 0.55, x 2 = 0.05, x 4 = 0.21, x 6 = 0.0 (orbit C2) exhibits this behavior as can be seen from the projections of its first 1000 successive consequents on different 2-dimensional planes plotted in figure 3. The projections look erratic, indicating that the orbit is chaotic. However, we also observe in all three projections that the C2 stays 'trapped' for many iterations in two oval-shaped regions and eventually escapes entering the big chaotic sea around these regions. This behavior is also de-picted in the evolution of the Lyapunov exponents of the orbit (see figure 4a). The three positive Lyapunov exponents are seen to fluctuate around σ 1 ≈ 0.033, σ 2 ≈ 0.02, σ 3 ≈ 0.005 for about 1000 iterations exhibiting 'jumps' to higher values when the orbit enters the big chaotic sea, stabilizing around σ 1 ≈ 0.793, σ 2 ≈ 0.624, σ 3 ≈ 0.365. Let us now study how the GALIs are influenced by the fact that orbit C2 visits two different regions of chaoticity characterized by different values of Lyapunov exponents. Since C2 is a chaotic orbit, its GALIs should tend exponentially to zero following the laws of equation (5). Thus, starting the computation of the GALI k , k = 2, . . . , 6, from an initial point of C2 located in the first chaotic sea, we see that the slopes of the exponential decay of GALIs are well described by equation ( 5) using for σ 1 , σ 2 , σ 3 the approximate values of the Lyapunov exponents of the small chaotic region (figure 4b). On the other hand, using as initial condition for this chaotic orbit its coordinates after 10 6 iterations, when the orbit has escaped in the second chaotic region, the evolution of GALIs is again well approximated by equation ( 5) but this time for σ 1 = 0.793, σ 2 = 0.624, σ 3 = 0.365, which are the approximations of the Lyapunov exponents of the big chaotic sea (figure 4c). Thus, we see that in this case also the σ i , i = 1, . . . , k which appear in equation ( 5) are good approximations of the first k Lyapunov exponents of the large chaotic region in which the orbit eventually wanders after about 10 3 iterations.

2 3 4 5 6 -3,0 -2,5 -2,0 -1,5 -1,0 -0,5 0,0 Log( i ) Log(n) a

Conclusions

In this paper we verified the theoretically predicted behavior of the Generalized Alignment Index (GALI) by considering some particular regular and chaotic orbits of a 2N -dimensional symplectic map with N = 3. In particular, we showed numerically that all GALI k , 2 ≤ k ≤ 2N , tend to zero exponentially for chaotic orbits, while for regular orbits they remain different from zero for 2 ≤ k ≤ N and tend to zero, following particular power laws, for N < k ≤ 2N . Thus, by using GALI k with sufficiently large k, one can infer quickly the nature of the dynamics much faster than it is possible by using other methods.

Also, the study of chaotic orbits which visit different regions of chaoticity in the phase space of the system, provides further evidence that the exponents of the exponential decay of GALIs are related to the local values of Lyapunov exponents. Thus, we have shown that the different behaviors of the GALIs for regular and chaotic orbits can be used for the fast and accurate identification of regions of chaoticity and regularity in the phase space of symplectic maps. We plan to investigate this further in a future publication concerning maps with N >> 3, which describe arrays of conservative nonlinear oscillators.

Fig. 1 .

 1 Fig. 1. The evolution of GALI k , k = 2, . . . , 6, with respect to the number of iteration n for a) the chaotic orbit C1 and b) the regular orbit R1. The plotted lines correspond to functions proportional to e-(σ 1 -σ 2 )n , e -(2σ 1 -σ 2 -σ 3 )n , e -(3σ 1 -σ 2 )n , e -4σ 1 n , e -6σ 1 n for σ 1 = 0.70, σ 2 = 0.57, σ 3 = 0.32 in a) and proportional to n -2 , n -4 , n -6 in b).

Fig. 2 .

 2 Fig. 2. Evolution of GALI k , k = 2, . . . , 6, for the regular orbit R1 on a log-log scale, for different values of the number m of deviation vectors initially tangent on the torus on which the motion occurs: a) m = 1, b) m = 2, c) m = 3. In every panel lines corresponding to particular power laws are also plotted.

Fig. 3 .

 3 Fig. 3. Projections on the planes a) (x 1 , x 2 ), b) (x 3 , x 4 ) and c) (x 5 , x 6 ) of the first 1000 successive points of the chaotic orbit C2.

Fig. 4 .

 4 Fig.4. a) The evolution of the three positive Lyapunov exponents of the chaotic orbit C2. The evolution of GALI k , k = 2, . . . , 6, with respect to the number of iteration n for the same orbit when we use as initial condition of the orbit its coordinates at b) n = 0 and at c) n = 10 6 iterations. The plotted lines in b) and c) correspond to functions proportional to e -(σ 1 -σ 2 )n , e -(2σ 1 -σ 2 -σ 3 )n , e -(3σ 1 -σ 2 )n , e -4σ 1 n , e -6σ 1 n for σ 1 = 0.033, σ 2 = 0.02, σ 3 = 0.005 in b) and σ 1 = 0.793, σ 2 = 0.624, σ 3 = 0.365 in c).

  was partially supported by the "Karatheodory" graduate student fellowship No B395 of the University of Patras, the program "Pythagoras II" and the Marie Curie fellowship No HPMT-CT-2001-00338. Ch. Skokos was supported by the Marie Curie Intra-European Fellowship No MEIF-CT-2006-025678. The first author (T. M.) would also like to express his gratitude to the Institut de Mécanique Céleste et de Calcul des Ephémérides (IMCCE) of the Observatoire de Paris for its excellent hospitality during his visit in June 2006, when part of this work was completed.