Formal Verification and Mathematical Understanding (& others)

0:00 Speakers, the first one up is Jeremy Aviga from Carnegie Mellon University with a talk on mathematical understanding and formal verification. Thanks very much. So I'll put this up early so you can just read it for yourself. Hopefully the relevance of this quote will be kind of apparent later. You're supposed to notice the intense concentration of self in the middle of such a heartless semester. My god, you can tell it. So this talk is, in large part, an extended advertisement for a paper that's already on my web page called Understanding Proof, and that paper in turn is an advertisement for some contemporary work in formal verification, which I take to have relevance to the epistemology of mathematics in ways that I try to spell out there. So what I'll do in the bit of time I have here is I'll say some things about mathematical and so I'm going to go from the general to the specific very quickly. I'll say a few things about mathematical understanding in general and understanding of proofs. Then I'll tell you something about formal verification and then a specific project in formal verification namely finding ways of verifying proofs with real inequalities. So the philosophy of mathematics has traditionally been concerned with issues of justification, which is to say identifying the proper warrants for mathematical knowledge, saying what makes a proof correct, saying what justifies the choice of axioms, you know, describing the sense in which proofs give you knowledge that's worth having. That don't fall neatly under that category. So there are, for example, there are evaluatory judgments made about mathematical development that are not easily cast as judgments as to the correctness of the proof or the truth of the statement. Let me just give you a couple of examples.

2:30 So, during his lifetime, Gauss published six proofs of the law of quadratic reciprocity, two more were found in his unpublished papers, and since then, about 200 proofs have been published. And the question is why? I mean, if you take the role of a proof to be warranting the resulting theorem, well, after the 15th or 20th published proof, you're pretty damn sure that the theorem is true. The answer to the question is what are you getting beyond that? For another example, it's common to say that Riemann's introduction of the complex zeta function to number theory, and more generally developments in complex analysis towards the end of the 19th century, made it possible for Hadamard and de la Vallée-Poussin to prove the prime number theorem in 1897. So that proving the prime number theorem really took the efforts of the mathematical community almost a century. And the question is, what is the sense of the word possible? What does it mean to say that, you know, these developments made it possible for them to prove the time numbers? It's fairly easy to make the case that it's not an issue of logic. In other words, it's not the case that they couldn't prove the theorem using the language and the inferences that were available to them before that. So something else is going on. The word understanding is used as sort of a cash flow phrase to capture things like this. So one commonly says that, well, you know, the extra, you know, 199 proofs after the first augment or contribute to our understanding. The introduction of the zeta function provided a certain understanding. But all too often the philosophical discussion ends there. It's commonly felt that when you start talking about understanding, you're talking about something mysterious and occult. You know, understanding has this essence that's just ineffable. And I think that's unfortunate because in ordinary usage, I mean, I'll argue that there's really nothing mysterious at all about understanding. And I think there's a lot more that can be said. So to illustrate, suppose we're talking about my friend Paolo, who's a smart guy, and I tell you that Paolo understands group theory, and you ask me to explain what I mean. So how am I likely to respond? What type of response do you expect to get from me?

5:00 Well, I might say, well, I mean, so Paolo, you know, he knows what a group is, he can tell you what a group is, he can give you some examples of groups, he can tell you, you know, he can recognize the additive group structure of the integers and then describe all the subgroups, he knows Lagrange's theorem, he can use Lagrange's theorem and show that the order of any element in a finite group divides the order of the group, he knows what a normal subgroup is, if you show him a normal subgroup, he can form the quotient group and work with that. He can list all the finite groups of order less than 12 up to isomorphism, can solve all the problems in his textbook, and so on. What's salient about this example is that the way I'm explaining, the way I'm filling out what I mean when I say that Paolo understands is by just giving a list of abilities. I'm just describing the abilities that I take to be encompassed by that description. Now we can talk about, you know, understanding, you know, lots of things. We talk about understanding theorems and proofs and problems and solutions, understanding methods, understanding theorems, understanding definitions, so it's a very, you know, the word is used in lots of ways, but when you think about the ways that it's used, invariably, when we talk about understanding, we seem to be talking about the ability to do things. It may be the ability to solve problems or to at least... Choose an appropriate strategy for solving a problem, maybe the ability to solve a proof, or to recognize a certain definition as being fruitful, or to apply a concept in the right way. And what I'm going to argue here is that this sort of informal way of explaining understanding is, when pushed and made more formal, it's still quite useful. And so let me try to be careful here. So, as I pointed out, we usually explain our informal descriptions of understanding by giving lists of abilities or characterizing the abilities that we take to be associated with that type of understanding. Now, informal language is sloppy, so it would be silly to look for, you know, sharp notions where there aren't. So, I mean, for example, it would be silly to expect a precise definition of what it means to understand group theory. Because, again, you know, the way we use that phrase will depend very much on the context, and even the specific context is kind of open-ended and indeterminate and vague. But in restricted contexts, we often make descriptions of understanding or related notions, we often use related notions, to make claims that we would like to discuss and debate and analyze and defend.

7:30 And in situations like that, we're forced to try to spell out what we mean by all of our descriptions. So for example, I don't know if I'm supporting if I say that a certain way of educational, a certain way of teaching something promotes understanding, or if I point to a mathematical development that I claim is important because it promotes a certain type of understanding, and so on. And so what I'm pointing out here is that it's still useful to analyze the notion of understanding in terms of the possession of abilities that you can get to encompass. Now you might worry that this sounds a lot like behaviorism. What I'm doing is I'm sort of identifying understandings with sort of the behaviors that somebody understands is capable of exhibiting. Or the disposition to behave in certain ways. But no, no, it ain't so. So keep in mind that in examples like the one I gave when we talk about understanding, I mean, sometimes the abilities we put forth are described in observational terms. You know, Paolo's ability to state the definition of a group or to respond to a question appropriately. But very often the abilities are described in more abstract terms. The ability to recall a definition, to use a lemma, to recognize a subgroup, to form a quotient group. These are things that are put in more abstract terms, but nonetheless we think of these abilities as being able to explain the abilities to produce observable behavior. So talk of abilities can still have an explanatory causal structure. So this is really little more than just a vague proposal that this way of framing issues is useful. And not only is it useful, but it opens up new opportunities for discussion and study. Suppose you're a philosopher of mathematics or a mathematical logician and you're interested in mathematical proof. Well, in traditional terms, there are really just two types of analyses you can give it, two things you can do. You can show that a statement is provable in some form of axiomatic theory, or you can show that it isn't. Two tricks, obviously. But if you sort of expand your horizon to think about two more general notions of understanding, you can think about what does it mean to understand a proof and what types of understanding do we get from proofs?

10:00 And again, just in informal usage, you know, when you say that somebody understands a proof, well, it can involve a very, very vague and heterogeneous list of things, but, you know, understanding a proof, so if you claim to understand a proof, so in particular, you should be able to respond to challenges as to your correctness. So, for example, you claim to understand a proof, and I say, well, good, I don't understand it, you know, please explain it to me, I don't understand this inference, why does this follow from that? You should be able to respond appropriately. Or understanding the proof could involve being able to give a sketch, a high-level overview or a sketch of the proof. Or to cast the proof in different terms, either eliminate or add abstract terminology. Sometimes understanding the proof we take could involve being able to indicate the main ideas. If you understand the proof, well, tell me what the central key idea is. Sometimes understanding involves the ability to motivate a proof. A sequence of steps, and you might want to say, well, why is this the natural thing to do? Sometimes it's the ability to give examples of the various phenomena described in the proof. Sometimes it's the ability to indicate where in the proof the hypotheses are, what goes wrong if you omit, and so on. Or to recognize the proof as being a generalization of something else. So say that, well, this is just like the proof of, you know, unique baptizations, you know, just in this more general sense. And the idea is, a priori, depending on what you want to do, any of these things might be things that is profitable to try to cash out and spell out and analyze more carefully. Okay, so that's pretty much it for the overview. So, for the rest of the talk, I want to really focus on this first aspect of understanding a proof. So, again, it's only a small aspect, but understanding a proof involves, in particular, being able to spell out an a proof. Now, if you think of a proof as, you know, the formal axiomatic model, it doesn't make much sense. I mean, a formal axiomatic proof, I mean, each step is, you know, there are small steps, and each step you should be able to check. There's a small list of axioms and rules. But ordinary mathematical proofs are not like that. They proceed at a much higher level, and so if you think of proofs in those terms, then this type of understanding is sort of interesting. How is it, you know, you need to be able to fill in the details. And this is the type of understanding that is relevant to the field of formal verification, and we'll say a little bit about that.

12:30 The 19th century, it's been understood. Mathematics can be formalized in axiomatic theories, at least in principle. For most of the century, the phrase in principle was the operative one. So if you've ever tried to write down a formal deductive proof and you've ever done mathematics, you know that being able to link the two is very difficult. Unwrap all definitions and spell everything axiomatically. It's a tremendous amount of work and really infeasible practice. It's only been in the last few decades that that's been changing in the sense that now you can use their computational proof assistants that have been designed that allow you to construct formal axiomatic derivations in practice. You have a proof in mind that you want to verify and you try to give the computer enough detail to actually construct a formal axiomatic proof. So your input to the proof assistant, so something called a proof script, you can think of it in a couple of ways. One way to think of it is just sort of a high level description of the formal axiomatic proof. Another way to think of it is a sequence of instructions that enable the computer to actually construct the derivation. People who do formal verification sometimes refer to proof scripts as being code. It's a program that constructs the formal derivations. If you want to do this, you don't want to spell out every low-level inference. You want to work at a higher level and have the computer... In which case, the key task is to find ways of having the computer verify these types of instances. And there, the problems you're up against, there are really three types of problems. It really all comes down to combinatorial explosion. So, I've indicated here, so first of all, look, if you're trying to prove that E follows from A or B, C and D, well, the canonical way to do it is show that, you know, E follows from A and the others, and B follows from B, you know, so that's just a case split, if A is the conclusion and if B... But look, if you have a lot of disjunctions, each time you have a case split, you're doubling the work, you know, the number of things that you have to do, and so that can multiply quickly.

15:00 Another problem is that if you're either trying to prove an existential conclusion or use a universal hypothesis, again, using a universal hypothesis will allow you to use any instances, and it's not always clear, so there's no bound on the number of instances you'll need to use, let alone what they are. And finally, verifying an inference, so the inferences are rarely purely first-order logical entailments. Rather, they can use facts from a general background library. Your background library may be huge, and so there's the issue of, well, how do you know what background theorems you'll need to verify the entrance? And the problem is compounded by the fact that all of these can come together, so you might have to deal with all of these at once. So, for example, if you're thinking about the real numbers, you know, it's a general fact that for every x and y, either x is less than y or x is equal to y or x is greater than y. And, you know, you may need to use that in a group. But to just, you know, instantiate terms randomly and split out all the possibilities will just get you nowhere. And so this is, you know, this is where I like the Moby Dick. That's what we found. I mean, there's this vast immensity of possibilities. Which, you know, could be a little bit frightening, but somehow, you know, we managed to go on. And we managed to go on because we stick close to our ship. So let me just give you one example of this. Ramsey's theorem tells us that for every k... By the way, some mathematical details go by quickly. Don't worry about it. So Ramsey's theorem tells you that for every k there's an n large enough, so it's that no matter how you color the edges between n vertices, color each edge red. The theorem says that for every k there's an n large enough, so it's that you're guaranteed to have a homogeneous subset of size k.

17:30 There is a subset of vertices of size k, such that all the edges between those vertices are red. Now once you have the theorem, it's natural to ask, given k, how large does n have to be to guarantee the existence. So a lower bound will say that if n is big enough, there's a counter-example. Here's an early counter-example. Here's an early lower bound due to Erdős. So the theorem is that if k, so if all k greater than or equal to 2, if n is less than 2k over 2, 2 to the k over 2. Then there's a counterexample. There's a coloring of the complete graph on n vertices with no homogeneous subset. The case is that k equals 2 and 3 you can check. Erdős' proof uses the probabilistic method. He was basically the pioneer of the problem. The idea is you imagine picking a graph or coloring a graph at random, and then you show that with non-zero probability, that graph will have the property that you want. So in this case you learn there has to be at least one calculation. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the k. The probability that they're all blue is 1 over 2 to the k. The probability that they're all red is 1 over 2 to the So now let's just bound this quantity. So n choose k, well it's just a factor of, you know, k things, each one at most n, and on the bottom you've got, well, k minus 1 things that are at least 2. Okay, so n choose k is less than or equal to n to the k over 2k minus 1. And so the probability you're trying to bound is, n choose k is less than or equal to, now you use the fact that you're assuming that n is less than 2 to the k over 2.

20:00 So I'm sorry to do this to you. So n choose k is at least less than or equal to i and m2. So you also use the fact that k is greater than or equal to 4, so the thing is less than or equal to 0, so m to 1. Then you put it all together. So the probability that there's no homogeneous subset is strictly less than 1. So with non-zero probability, there is a homogeneous. So in particular, when n is bounded, as in the statement of the theorem, there is a homogeneous, there is a coloring with no. What I want you to think about, I said, look, this went by quickly and maybe you understood it. What I want to point out is that understanding this particular thing involves being able to, if I ask you to, you know, go through what I just did more carefully and spell out, you know, justify all these inferences here, you should be able to do that. And again, speaking informally, understanding elementary mathematics involves being able to verify inequalities of And the point is, if you're doing formal verification, you need to model that type of understanding. You need to say something about what it means to understand inequalities of that sort, and explain how to do it. Oh boy, I'm running out of time. So, let me, let me, so Tarski's theorem gives you a partial answer, so you know that the first order theory of the wheels is decidable. Let me just say quickly that that doesn't tell the whole story, because the procedure for wheel-closed wheels is slow, and arguably it's just misguided to the type of thing... But WIRS is very limited, so it doesn't extend at all to very straightforward inferences of monotone functions and exponentiation of logarithms.

22:30 So all the calculations that involve exponentiation there are not covered. So how do you go about verifying these things? So one observation is that often you just work backwards. That's idea number one, you work backwards. So for example, to prove that ST is positive, You can just show that s and t are both positive. Or you can show that 1 over t is less than 1 over s. So you can always try to work backwards. But the problem is that this is called backchaining, and the problem is that backchaining is nondeterministic. So, for example, you can also prove that s times t is positive by showing that s and t are both negative. So you have the dreaded case, or the non-determinism is even more dramatic. So if you want to show that a sum of things is less than a sum of some other things, well, you can pair things up in different ways. I mean, for example, you can show that s plus u is less than v and t is less than r. Or even more dramatically, you can show that s plus t plus u is less than r plus v. You know, by showing that s plus u is less than r plus 3 and t is less than r minus 3. And look, this is maybe what your hypotheses are, what they give you. Okay, so if you just work backwards, there's just too many possibilities. So that alone won't do it. Another strategy is to work from your hypotheses. You know, you have all this information. Now you just derive, oh, I just went through this. But, you know, you just sort of work forward and you keep deriving new facts, like sort of elementary steps. And so you get to the point. But of course, you know, you can't just work, you know, you can't just derive things at random. You somehow have to need some plan as to where you're going. The third idea, the third idea is that sometimes we're able to do complicated things by being able to do certain things and being able to combine those simpler abilities. So the first order theory of linear equalities and inequalities is easy to handle. There are deterministic procedures that tell you what to do. And the multiplicative theory, well, modulo case splits.

25:00 So you need to know the sign. Modulo splitting on the sign. Multiplicative theory is also easy to handle. And let me also tell you that in computer science, there are methods known as Nelson-Oppen methods that tell you how to combine decision procedures. So the theorem is that if you have a decision procedure for the universal fragment of a theory T2, and the languages of T1 and T2 are disjoint, except for the equality symbol, then you can combine the decision procedures and get a decision procedure. So if you know what to do in each case, you know what to do. Now, in the case that we're dealing with, the overlap is more substantial, so Nelson methods, open methods don't, but nonetheless, this is, I think, a very powerful idea that somehow combining globally can give you. So, in the context of real arithmetic, Harvey Friedman and I made a study of, so we defined a theory, you know, T of Q, that basically is the union of the additive and multiplicative coefficients from the nationals. Well, I mean, so we're logicians, so we prove theorems, right? So we said that a theory has good normal forms, so you can put terms in a canonical normal form in such a way that it's easy to test whether two terms are proven to be equal. The full theory is undecidable, but the universal threshold, so think about quantifier-free validity. That theory is decidable. And the results, they're beautiful logical results, if I do say so myself. I mean, they're nice theorems, they're beautiful proofs. But they're not at all practical. Our decision procedure goes by a tortuous reduction to the theory of real close fields. So you have a procedure that does less than real close fields in Russia. In the same paper, we also propose a heuristic method. And it is roughly, you put the terms in normal form, and you just go back and forth using the additive and multiplicative procedures to derive new inequalities, so you work forwards, but you work forwards guided by, so the theory tells you that all that's relevant are inequalities between subterms of the terms you have available. So you work forward, but derive anything that may potentially be relevant.

27:30 And this, I'm morally convinced, is really the right way to go, but we don't have theorems to that. The question is, how do you make that case? The obvious way to make the case is to, look, just compile a library of sample problems and, you know, you implement the procedure and we can solve all these problems and so and so many milliseconds. And we are hoping that, you know, computer scientists will take up the challenge and do this. I think it would be, we want more than that. So the problem that they see is really a conceptual problem. So compare the situation, so with decision procedures, you have, the point is you have a deterministic decision procedure, but a priori that doesn't guarantee that it's going to be a decision procedure that's great in principle but runs just too slowly and is much less useful than a decision procedure, well a procedure that may be, but you know, just all the things you care about in practice. And when you talk about heuristic methods, you're designed not to be complete, but you're designed to work well on a type of infinite number of factors, and the idea is we need, I mean, I put that in quotes, but we need a better conceptual language, I maintain, to be able to understand common textbook, and we need a better way of saying it, conceptual common, trying to characterize the types of delts with. It's very fruitful to characterize the types of abilities that... But, you know, it's not the only one. I mean, any place where, again, where notions of understanding come up, you know, clarifying notions, you know, I maintain that reflecting on the types of auditory judgments are not only, you know, but they can also lead to genuinely mathematical... If you have seen that a certain way of doing mathematics or something about mathematics is good or positive, if you can somehow articulate what it is...

30:00 This is exactly the shift that we're close to and whether or not it connects to this idea of a boatload of heuristics and whether or not in this boatload of heuristics the inferences divide naturally into kinds. That's my question. The hypothesis, the feeling, the thing that I'm morally certain of is that there is something to say here that mathematics is structured in such a way to make understanding possible. In other words, definitions hang together, there are methods, there's some story to be told about how the elements of mathematics work, but I don't know how to tell that story. I don't know exactly what you mean by natural, the sense of natural kinds. So my feeling is you want to look, let me also say that I think what you want to do is look at mathematical facts and work from the example. Yeah, so I do think that things, I think they should come out in our own argument of natural kinds.

32:30 Of course you made this connection explicit, so maybe it wasn't part of your goal, but at the beginning you were talking about the fact that you're proving the same thing over and over again. Can you connect to that? Oh yes, so I did. There's another paper on my web page called Mathematical Method of Proof where I explore that issue. But there's the thing I think you want to tell is that when you value different proofs, very often it's you value proofs for showing you how to do things. So I think the same type of abilities are. The proofs show you things, and these are things that give you the ability to do other things. And I try to give out lots of examples in that paper. I mean, here I'm fixated on the word ability, here I'm fixated on the word method, which is closely related. You talk about methods of doing things... I've shifted from talk of method to talk of ability because, you know, talk of ability sort of lets you be a little bit agnostic about the procedure by which the ability is observed. So what's important is that that you can do, thus and such. It may not be, you may not care what the algorithm is or whether there is an algorithm. You want to calculate what the abilities are. But on the other hand, as I mentioned, you want the ability to tell some kind of causal story. Some abilities can account for other abilities and stuff, and that seems to lead to a sort of compositional that you really compose and perceive. So I don't quite know how it should be done, but they did roughly that, that the proofs give you a certain type of procedural, methodological, or ability knowledge that you want to carry, that the philosophical has to do that. You know, the title, I guess, was on the program, Finding the Right Definition in Mathematics with Consequences for Ontology.

35:00 I'm so eager to share. Okay, I would say it was called Something on the Order of Finding the Right Definition in Mathematics with Consequences for Ontology. I tried to keep things under control when I unsuccessfully tried to keep things under control. Leave that aside. But I want to talk about some things having to do with finding the right definition in mathematics. And in particular just to put a bunch of issues on the table to introduce you to some simple examples. And wave my hands in the direction of more complicated examples to try to get you to realize that there are a cluster of issues here that should be paid attention to. Now, I'll start with a background observation, and I'm happy to say it's a commonplace. In a proposal, I said that I wanted to explore this, and Thelma Cahill, an anonymous referee, said, ah, everybody knows this. So it's good that everybody knows this. So we can start with that. The mathematical arguments are assessed for more than just strict enough codency. We prefer to explain or yield understandings of the issues that Jeremy touched on as well, or discussed as well. The idea of proof explaining or yielding understanding is one of this idea that one of several different equally logically cogent proofs could be the right proof interacts in delicate ways with lots of other things, lots of other ways in which you might say we can get it right. Where this isn't just reduced to having a deductively cogent argument. In particular, finding the proper definition of a term or an expression or finding the proper domain of definition. Something like that.

37:30 Okay, now for orientation, I want to just point to a kind of thing that you'll find mathematicians do. Okay, help illuminate what this involves and what philosophical ramifications it might have. Okay, so here are a couple things. And this is John Harris, an algebraic geometer. And in a retrospective survey of algebraic geometry in the 20th century, he says, the thesis presented here is that the progress of algebraic geometry is reflected as much in its definitions As in its theorems. In fact, this long survey of 20th century algebraic geometry really bore that out. The major epochs were all marked by introducing, successfully introducing specific concepts which then allowed you to restructure from a group of ways. Now here's another remark from, this is now an elementary textbook, Spiver. In an advanced textbook, Spivak's Calculus of Manifolds, Spivak says that Stokes' theorem shares three important attributes with many fully evolved major theorems. First, he says it's trivial. Second, it's trivial because the terms appearing in it have been properly defined, and he says it has significant consequences. You should know that by trivial he means proof that involves only two applications of Houdini's theorem. Now, there are really two different ideas here. I'm going to treat them, run them together, but it's worth noting, of course, they are the same. One is the stipulative introduction of a new concept, and the other is refining the definition of an established one. It's not going to matter to me to treat them as a piece. Now notice here that you're getting a good fully evolved Fermi-Stokes theorem involved in getting the definitions right, supposed to have as a consequence the results for controllers, supposed to be measured in significant consequences, and obviously many different things will contribute to making a consequence significant. Connections, explanations, proof of instance. Okay, now I want to give one example just to... There are lots more complicated examples I can give, but this one is nice and simple and familiar.

40:00 This is finding a proper definition of prime number in algebraic number theory. To some extent, these things are going to be context sensitive. In analytic number theory, different considerations will be relevant. You might say that what it is to be a prime number is truly what you can say by definition, right? It's analytic, truly we all know that to be prime is to, a number n is prime if it's even re-divided by only one n. Now, in the natural numbers and some other extended settings, not all of them, this is equivalent to another less familiar definition. Actually, you know, familiar to the practitioners, but not to the... A number a is prime if whenever a divides a product bc, and you write that down, a slash bc, then a divides b or a divides c. Now, in extended context, right, and this is one of them, z and pi by, these aren't equivalent. Now, in general, the word prime in algebraic number theory is reserved for the second definition, right, or things. And the word irreducible is used for number sets first. So why is this? Well actually the point was already appreciated in the early mid-19th century by Eisenstein, who pointed out that the property that did most of the heavy lifting... Most of the interesting properties of prime numbers turned out to be the second one, right, and there's actually a nice article in Mathematica Nalen in 1993 where, I mean, they're considered all the different possible meanings. You could attach to the word prime, as exemplified in the prime decomposition theorem for the natural numbers, and she indicates, gives a set of reasons for preferring the definition, which is, you know, now the new definition, the A divides B, C, then A divides B, or A divides C definition, as it does most of the heavy leavening, right, most of the interesting ones, right, but prime numbers turn out to depend on the second. Now, just to put it in a kind of charged way, I'd say that really the familiar definition isn't the right one, even though it's what everyone who isn't a specialist would cite if they're asked for a definition of prime number.

42:30 One of the things a mathematician is supposed to do is to find the right definition, figure out which definitions are the good ones, and in the case of front-number theory, this is the right one. So you have kind of an epistemological issue. We want to just be clear on what kind of an advance in knowledge we make when we discover the right definition. The classic discussion of by Putnam in the analytic and the synthetic, where he points out that you might take kinetic energy in pre-relativistic physics to be, by definition, one-half mv squared, right? And then when relativity comes along, you sort of have a choice. It really is true by definition that kinetic energy is one-half mv squared, in which case... You replace kinetic energy with another definition, or you might say, well, no, it wasn't true by definition exactly, it was a very well regimented but false empirical fact, and so we have to change our account of the fact. To think of it in either of these two extreme ways is to miss the important point, which is there is some kind of advance of knowledge that we're making by figuring out what the right definition should be. And just saying, well, we had one definition and we replaced it with another, or, well, we were just wrong about the facts, either one kind of overlooks this kind of intermediate status. There are a number of ways that the discovery has, and I want to emphasize that we find this sort of thing happening in mathematics, too. Now, more generally, I think, although this is to use a very ambiguous and many-slendered word, you'll find people talking about natural functions, natural formulations of things.

45:00 There are a number of different ways of evaluating definitions and other things, overlapped significantly with analogous questions concerning properties in the physical world. If we want to start with just simple intuition of cases, let's say you wanted to... The intuition pump case like distinguishing green and grue, where somehow green is natural and grue isn't, and that can form sort of a bedrock way of distinguishing, a bedrock example of distinguishing natural from artificial. We do the same sort of thing in mathematics, right? You might say, well, if it's divisible by 17, it could be distinguished from the property is pi or a random surface of genus 7 or the stone check and factification of the integers on the same sort of grounds, right? So one is intuitively natural, the other one not. The other one artificial. It's all together. For orientation, I went back and looked at this classic discussion by David Lewis in his writings on universals, talking about the work that's done by the idea of a natural property. And I say, well, one of the things that the work does is it's supposed to underwrite the intuitive natural, non-natural distinction in clear cases. It's supposed to form a basis for judgments of similarity and simplicity, and it's supposed to support assignments of context. For example, in perfect impact cases, it's supposed to underwrite a distinction of intrinsic and non-intrinsic properties. So, single and intended interpretations of cases of underdetermination, I guess that should be, supports the distinction between laws of nature and assumptions and realizations, and it's relevant to descriptions of causation. Now, apart from the causation, which is kind of the wild card for discussions of mathematical properties as opposed to physical ones, most of the entries on this list aren't importantly different in the case of physical properties than mathematical ones.

47:30 An account of natural properties won't help at all unless mathematical functions are included in what's counted as natural. Although it's hard to imagine how an account of natural properties could help in a discussion of laws of nature, unless at least some mathematical properties, functions, and relations are included, since the criteria and practice for law-like nursing simplicity of laws often pertain to their mathematical form. Now, can this relation be formulated as a partial differential equation? Is it first or second order? Is it linear? Now, I'll just gesture in the direction of a more complicated example that I don't want to, that I wouldn't be able to entail on, but I just sort of want you to know that it exists. Find examples of mathematicians identifying certain properties as natural and find corresponding examples of people with There's a lot of specifically applied mathematics in mind, making distinctions between natural and non-natural formulations, and you can find cases, and one really quite striking one is the approach of Riemann to complex function theory, parallel to this approach of Helmholtz to theory of potential and electric charge, in arriving for the same reasons. The same principles for identifying certain formulations as natural ones and certain as not. So I just want to indicate that the sorts of things that we have to understand in mathematics don't occur just in pure mathematics, but also... So let's say we want to get clearer on what's going on when identifying the right definitions, something that mathematicians will do, and maybe also understand how that might relate to the idea of finding certain definitions and categories as being the natural ones in mathematics.

50:00 All right, what's called, you know, the practice of trying to find a mathematical definition. It interacts with a range of other objectives. So, to understand what's going on when we try to... There we have to understand what's going on when we try to explain something in mathematics, and when we try to understand what's going on when we're trying to explain something in mathematics, we have to get clearer on what it is to find the proper domain of definition. What I want to do is give you a couple of simple examples to indicate how all these things can interact. So here's just for a quick orienting question. What do we gain by using the complex numbers? Now there's a popular kind of answer concerning ideal elements generally, and it's sometimes taken, I'm not sure how accurate they do, to appear in Hilbert's On the Infinite, which is that complex numbers are useful because they can abbreviate deductions. There's a sort of computational age element that they're kind of eliminable. But they don't have any cognitive significance beyond that. And now I guess to borrow an example from Mark Colvin, sometimes the gains from complex numbers don't get preserved if the complex numbers are eliminated. I forgot what Colvin points out. That by formulating theories over the complex numbers you can unify apparently diverse phenomena. A nice simple example that he points to is the unification of trigonometric and exponential functions, functions which over the real seem to have little to do with one another, but admit of these sort of unifying definitions over the complex numbers, and you have the usual real-volume sine, cosine, and exponential functions as special cases. This example carries over to more direct physical applications for solutions of differential equations.

52:30 Here what we do is we introduce complex numbers. That gives us a unified mathematical theory, but the cognitive advantages aren't restricted just to some abstract platonic realm because it carries over to a unified physical theory as well. Theory is too grand for family of answers to certain questions, right? So, I mean, as Colvin is aware, right, this gives a connection to philosophical accounts of explanation, as is the case for Friedman, but there's, at this point, there's a question mark that we have to erase. If the unification is a good one, it has to be that we aren't just cobbling together a couple of theories. You have to be unifying things in the right way. For example, it can't be that you're just gerrymandering together some predicates that will give you a formal unification of different theories. But rather it has to be done in a way that really provides illumination. So what can we mean when we say really provides illumination? One thing you might point to, and here you now bring something else in, because this interacts with something else, you might say that it should be the case that we can use this to provide explanations of things. So, let's see if that, and here's an example of where you can point to this unification as one which allows you to explain. And this is again a simple example, well known, you can find it in lots of elementary textbooks, sort of a stock example of explanations using complex numbers. Explaining the radius of convergence for real-value theories. And here are a few simple functions. We have g of x is 1 plus x squared.

55:00 H of X is 1 divided by 1 plus X squared and K of X is 1 over 1 minus X squared. Now, from the point of view of just simple calculus in the real life, the first two of A to G and H have much more of an affinity than the second and third. The first two are never zero and they're never undefined. They're infinitely differentiable everywhere. But when we extend things to series, sort of complications appear, our judgments of which things have affinities to which change, and we just recall that with some regressibility conditions are not distributed, we can extend a function to a power series, generally f of x is sum of j is 1 to the infinity of a j of constant x to the exponent of j, and this equality is going to hold within some bounds. So we can expand the functions we looked at, g of x, 1 plus x squared is its own expansion, 1 divided by 1 plus x squared expands into this is the series, and 1 over 1 minus x squared expands into this. Now actually, you don't have to do anything as fancy as Taylor's theorem, you can just plug in, do a substitution into a familiar series of divides. It doesn't really matter for our purposes how it is that we write the series. Okay, the functions of h and k both have the same radius of convergence, which is 1. And they converge for x between 1 and minus 1 and then diverge otherwise. So you say, well, look, if you're asking yourself, why does this series diverge? Well, you should expect that you'd run into problems at 1 and minus 1 because 1 minus x squared is going to be undefined there. But why are you going to go haywire here? What's the problem there? It seems that in restricting yourself to real numbers, there seems to be no rationale for expecting that you're going to run into problems with one or the other.

57:30 Okay, when we go to the complex point, it becomes absolutely clear. 1 over 1 plus x squared is well-behaved for real numbers. It has complex similarities, singularities. We can even draw a picture that kind of reinforces this and say what does this look like in the complex plane where here the argument, the real and imaginary parts of the argument are on these two axes and the absolute value of the value of the function is on the third axis. So here in fact you have poles at precisely these places. And that's where the singularities are going to occur, and more generally you get a result that there is a radius of convergence, which is the distance in the complex plane from the center of the series to the nearest singularity in the complex plane. There is also a connection to definition, again I could give lots of examples, I'll just give one. To find the proper definition of elliptic function, or what was taken to be the proper definition of elliptic function, you have to take the definition not of what was originally introduced, It was originally introduced by inverting a class of integrals, but rather you sort of accepted the correct definition, which identifies its characteristic properties, and thus have meromorphic doubly periodic functions, in particular the function has two periods. This definition is only going to make sense. This definition is only going to work if you're over the complex plane, because one of the periods is always going to be imaginary. Here we kind of cycle around. We start out with this idea of what's involved in giving a proper definition. Here it turns out that in some cases, to give a proper definition, you also have to have a proper domain of definition.

1:00:00 What makes that domain of definition proper? Well, it's going to allow you to explain certain things. It's going to give you unified theories of certain things. A case that Jeremy introduced at the beginning, which, although it avoids the issue of talking about causation, I'll talk a little bit about, I'll just touch on projectability, because what's striking about the theorem that Jeremy mentioned at the outset, quadratic reciprocity, is that not only did Gauss give six proofs of it, But it had been conjectured, and this is something Goetz himself referred to, by induction, even before it was proved. And actually, if you look at the reading, this is sort of preserved in Euler's textbook. The reasonings correspond to exactly what you would find if you wanted to give an elementary presentation in your elementary class of how you might reason with grue and green. Euler calculates a bunch of cases, makes a conjecture, doesn't work. Calculates more cases. Re-conceptualizes, makes a different prediction based on new sort of ways of carving things up, doesn't work, tries again, it works. And it works in part because he hits on the right category, the mathematical equivalent of Grue versus Green. Now, I'll just close with a sort of point to the thing that Euler... This is not exactly what Euler used in simplifying the history considerably to get the story right. One way of defining something which allows you to give an extremely straightforward, clean statement of the theorem that Euler ended up sort of conjecturing by induction.

1:02:30 What's known in the trade as the Le Genre Symbol. For n and p and not prime, n mod p is defined as this. It's 1 if a certain thing happens, minus 1 if something else happens, and 0 if yet a third thing happens. And what that does is by using that definition, you take a relatively complicated theorem and you can give it a single line statement. If we're thinking, that sort of poses a kind of puzzle, and the puzzle turns out to be a complicated answer. Should we regard that as a sort of desirable unification or not? You have a complicated statement and you make it simple. But then it looks as if, just on its face, as if you've made it simple. By cobbling together something which is even uglier than Grue, and the answer is, well, you know, if I have 15 sort of disjunctive clauses, I can come up with a single statement, right? But the actual answer is it's very complicated, right? And you can, after about 150 years of mathematical investigation, you can say, in fact, this really is an exceedingly central property. All of the natural numbers, although you would sort of define it rather differently, is something that you can later discover. So just to close, I'll sort of truncate things here with this sort of kind of closing. To the extent that we're going to make distinctions between properties being natural or artificial and mathematics. As in the case in the empirical world, if we see there as being a connection between patterns of inductive reasoning and finding the right categories, as in the textbook discussions of Grue and Green, the same issues are going to arise in mathematics.

1:05:00 Make a first approximation of distinguishing between a natural and artificial by focusing on the fact that something is disjunctive, that's going to work because things can fail because things can be superficially disjunctive, so to say, deeply not, and it can require a lot of investigation to turn that out. I just want to repeat what I set out to do. I wanted to point to a family of phenomena and mathematics and indicate how they interact and bring out that if we're going to understand one issue in the cluster, we're probably going to have to understand a lot of them, and I hope to convince you of that. Well, to begin, I think I agree with everything you said, but it's highly reminiscent of old debates about the nature of definition, whether definitions in math are stipulative or real. You're on the real side, and I think that's the correct side. Well, I mean, I do think that there are some definitions that are stipulative. There's a way in which what I'm trying to do is, in the longer paper which this takes some bits from, revisit the old debates between the questions of whether or not mathematical definitions are stipulative or can be real. And you can sort of trace out this sort of history where real definition keeps taking it on the chin. There's a classic text of the history of logic by Henriquez, who is an historian of logic of great health and great gender. His view is that what we should have learned after all of the times since Aristotle is that all definitions are null. That all definitions are stipulated. The idea of real definitions is completely empty. ...completely dormant in the 20th century except with one exception of this thin but kind of interesting book by Robinson, who revisits the idea of real definition and he said, look, here's one reason why it's turned out, the idea of real definition has turned out to be untenable.

1:07:30 There are just too many different things being called real definitions, right, and they list some long list of things that you could be calling a definition when you say it's a real definition. I think what we should do there is go back to Robinson's list and it seems to me that several of those things are things that definitions really can do. And rather than sort of try to stick to the old idea of what a real definition must be, we ought to just sort of rethink how much of the old picture can be saved. Well, I think the right way, the right thing to say about them is to just say, look at the history of math. It's just like the history of physics. Look at the changing definition of electron from 1890, you know, pre-quantum mechanics into quantum electrodynamics into the standard model. It keeps changing. And there it's clear they're not stipulating what an electron is, they're trying to actually tell us what an electron is. It's a classic example of a real definition. Now I want to follow up very quickly, a very quick question. There are ontological consequences of this. Let me just say, I think it's not a knock-down argument, but it's strong support for a kind of Platonism in math because it's so analogous to the physics example. We think there's a real world out there. We're all realists about physics and they keep changing the definition of electron, trying to get it right, and we keep changing definitions of function. Trying to get it right, shouldn't we think that there's just a photonic world and we're conjecturing about it? It's fallible. Math is highly fallible. Well, I want to suspend judgment on that, but if anybody asks, we all agree with you. I guess I want to ask my question now in a way that it relates to Jim's point. You used the word natural definition or the natural definition. Different, I suppose. The right definition. The proper definition. Now, if it's the proper, Or the right, then it sounds like you're looking for the right real one of all time, and I thought maybe you didn't mean that.

1:10:00 Well, that was a concession to usage. I mean, you'll find mathematicians saying, this is the proper definition, right? And then if you sort of say, well, what do you mean, V, unique, absolutely, and all, well, no, no, no. In the context of algebraic number theory or the qualified thing. So I certainly don't want to say that... It's always going to be the case that one definition is the uniquely best. I think it's enough for my purposes and seems to be enough to support the conclusions I think you ought to draw, if you can make distinctions of better and worse. Well, but is this at a time? Or is it best overall? So one question that occurs to me, right, is did Robinson get the right definition of infinitesimal? Was there just that one to be gotten and it was, you know, gotten much, hundreds of years, a couple hundred years after Newton? Or not, right? Or is it just that there might be a good or natural definition at the time? Particularly if, right, you're incorporating this notion of unification into what makes something good or natural, yeah? Because presumably that… One way of construing that is that it's relative to your knowledge, yeah. I want to be clear with that. I'm not making anything of... One of the things I'm trying to bring out here is how complicated the network of interactions are. So I certainly don't want to say anything so straightforward as it's natural if it supports a unification. No, of course, of course. Lots of times, right? Here is what it, you know, when you want to say this is a particularly natural definition, it's because when you unravel it among the things that you... In the case of infinitesimal, I'd have to consider the... I mean, it would depend specifically on the case. But at the very least, I'd be very surprised if it didn't turn out that Robinson's was at least, whether it's the uniquely best, it might... It would nonetheless be much better than several other candidates, right? And it's enough that you can say, look, here are these two definitions. They're equivalent. One of them is much better than the others, right? Or one of them is better than these others we've looked at.

1:12:30 Then you say, well, are there other definitions that could be equally good, or are there other definitions that might be equally good in other contexts? I say that may be. I don't see that what I'm saying is hostage to there being a uniquely best. I didn't think so either, but I wanted to be clear about this. But if you were taking the real definition in the way that I think Jim meant, then maybe it would be incompatible. Yeah, I would say that there was a meaning to find some kind of analog and traditional philosophy in the program, but it may have to be solved. Paolo Mancuso. Let me say something in general about this topic, because many of you might not be familiar with such a topic as explanations in mathematics, but there are two contexts in which explanations in mathematics occur. One of them is how you can give mathematical explanations of scientific facts. So sometimes geometry or arithmetic or number theory enters as an essential component of the explanation of a certain scientific phenomenon. And getting clear on that kind of usage basically opens up the whole issue of how mathematics applies to the world. And so recent work by Batterman and by... Margaret Morrison here is very useful exactly because it points out how sometimes you can get that the math removes you from the world and so detaches you from explanation and at the same time there are cases in which the math seems to give the structural explanations as in the Batman cases that you'd like to have and so this is a really detailed topic and problematic topic. Also there are consequences for ontology here.

1:15:00 In particular, I'm thinking of the work Alan Baker did and Colifat is doing on whether you can revive certain forms of the indispensability argument by using, in fact, explanations of scientific phenomena in which the mathematics is essential to the explanation, and there is an article by Alan in the British Journal of Social Science from 2005. So that's for the... This is sort of one line of the problem. The other one is mathematical explanations within mathematics, i.e. the idea that in mathematics, like in any other rational enterprise or science, we do explain things, and if so, what kind of... What do the explanations look like? Well, here again, we have two different sorts of important applications of philosophy. One of them is, if you're sort of tired of an epistemology of mathematics which has been completely hijacked by ontology, i.e. the idea that the only question you need to ask, and nothing you shouldn't, but it shouldn't be the only question, is how we... As empirical beings and sentient beings of the type we are can have access to abstract objects, if you're sort of targeting epistemology hijacked in that way as the only question to ask, well then you should reflect on the fact that, as Jeremy and Jamie were saying, there are other epistemological problems in mathematics that you can raise and that are completely unlike this one. So there is an issue of epistemology, and finally there is an issue of application to philosophy of science. Most theories of scientific explanation either rely on causality or rely on laws of nature as the central component. Well, then those theories cannot serve as theories of mathematical explanation, because causality and laws of nature do not seem to enter into mathematical explanation. Okay, so now for mathematical explanations within pure mathematics, that's all I want to talk about here today, there are basically two theories on offer out there.

1:17:30 And one of them is due to Steiner, to Mark Steiner. And it's a theory I like to, following Freeman, to call a local theory of explanation. In Steiner's account, what counts as an explanation? Whether a derivation, in fact, counts as an explanation. For Steiner, it's basically a syntactic feature of the derivation. Certain derivations have very specific properties, and those make them explanatory, and the other ones are not. So this is really as far from contextual as you can get. It doesn't depend on the context whether something counts as explanatory. It's a local phenomenon that can be judged, in fact, without even a reference to a more global concern. Now, by contrast, the theory defined by Kircher on unification These are global theories of explanation. A single derivation doesn't count as explanatory per se. It counts as explanatory only if embedded in the best explanatory store, as Kircher calls it. That's why it's global. The single derivation becomes explanatory because it belongs to this particular global context. Now, of course, in Keacher's case, the usual objections that I was raising about theories of explanation coming from the scientific explanation camp do not apply because, in fact, Keacher sees as one of the advantages of this theory of unification that it applies to mathematics and it accounts for certain problems that are typical of... The theories of explanation like explanatory asymmetry also in mathematics. So what I'd like to do, of course, I don't have that much time, but I'll try to at least give you a sense of this longer paper, is say something about Kitcher's theory of explanation, which I'm sure most of you are familiar with, and then I'm going to talk about a case from real algebraic geometry, trying to, in fact, assess Kitcher's model from the point of view of this case. And the spirit is palpative. It's not just that... We're using this counterexample to say, you see, it was all wrong, but it's actually to, what's interesting about the counterexample is that it's a counterexample in which uniformity...

1:20:00 And so, in a way, you feel like that's the kind of situation that Keacher's model should be able to account for, but in fact, it seems to fail on that. And so, the theory is positive in the sense that we'd like to see what can be done with this model, in fact, in terms of improving it. So here just for a couple of quotes. First one is that the fact that the unification approach provides an account of explanation as much as we assume it is in mathematics and science is crazy. And then he says, you know, obviously all I've done is to sketch an account of mathematical explanation, sorry, of explanation, and then at the end there is a second quote that says what needs to be done is to look closely at the argument patterns favored by scientists and attempt to understand it. Now, what's the basic intuition here? Well, first of all, in 1981, Kircher points out two things about what we should expect from a theory of explanation. The first one is that a theory of explanation should account for how science advances our understanding of the world. And secondly, it should help us in evaluating arbitrating disputes in science. The basic intuition is one that Kicher found in Friedman, in particular the article on Explanation of Scientific Understanding where Friedman put forward the idea that understanding of the world is achieved by science by reducing the number of facts that we take as rules. Kicher disagrees with the specific details of Friedman's proposal, but thinks that the general intuition is correct, and so he modifies Friedman's proposal by emphasizing that what lies behind It's the reduction of the number of argument patterns used in providing explanations while being as comprehensive as possible in the number of phenomena explained. So that's the key here, is the notion of argument pattern, which will become the key element for the explanatory source that Kinshaw wants to define.

1:22:30 In an account given by Kircher, an argument is considered as a derivation. In other words, if we take an argument to simply be a pair of premises and conclusions, that doesn't tell you much about how you go from the premises to the conclusions. Whereas in the systematization account, the one that Kicher is proposing, actually the steps involved in going from premises to conclusion are spelled out and in that sense what we get is a derivation. An ideal explanation then does not simply list the premises but shows how the premises yield the conclusion. Let me just say a couple of things about the details of the model, at least to get the terminology straight here. So what's the idea here? We're trying to systematize a bold decay of sentences that either we hold or that we believe in, and we like to systematize those by, in fact, providing derivations that systematically explain, as it were, this bold decay of sentences. Well, then, a general systematization of K is just any set of arguments which derive sentences in K from other sentences in K, so these are just taken to be derivations in ordinary sense. Well, what's the explanatory store over E ? Well, it's the best systematization, of course, we need to say in what sense, we can talk about best systematization here. Now, what does the explanatory store look like? Basically, let me give you the intuitions, probably. If you've got that, that's enough, and the rest takes care of itself. It's the idea that when we engage in science, be it Newtonian Mechanics or Darwinian Biology or Mathematics or whatever, you have, as it were, a bag of argument patterns.

1:25:00 And those argument patterns you believe in or you take to the explanatory argument patterns and basically you reuse these argument patterns in all kinds of instances. And those are the kind of argument patterns that you appeal to for explanations. Now, there might be different levels of explanatory unification of the volume of knowledge, and that will be measured by, in fact, some parameters on how the argument patterns behave. You know, for instance, do they account for all the truths? Or how many there are, how many argument patterns there are. Obviously, apparently, the fewer the better, and so on. So, it starts with the notion of a schematic sentence. That's a sentence in which you might replace some or all of the non-logical expressions by dumbing letters. Then you have filling instructions that tell you how to replace constants for the dummy letters. They tell you that in place of a variable for a function you can put a continuous function or something of that sort. A schematic argument then becomes just a sequence of schematic sentences. But the extreme case is the logical case. Where every non-logical constant has been removed, and in fact you can plug in anything that belongs to the right syntactical category, but of course in the sciences we make a lot more restrictions on what can be replaced for the particular nanny letters. Finally, a classification for a schematic argument is a set of sentences which tells you exactly what role each sentence in a schematic argument is playing, i.e. whether it's a premise, which sentences are inferred from which, according to what. So it gives you a full classification of the argument itself. And finally, then, a general argument S and S is a triple consisting of a schematic argument S. A set of sets of theory instructions and a classification sheet for it. Okay, now let me just give you a quick example to convince you that this kind of stuff can be applied to mathematics. If you know the teacher work, you'll know that he uses schematic argument for Newtonian mechanics that seem to be everywhere, according to him in Newtonian mechanics, and other schematic argument for biology.

1:27:30 But here is an example from mathematics. Suppose, you know, a typical problem with calculus. Well, here is the solution using derivatives. In the first step, you compute the derivative of the function of the curve, then you plug in 1 for x, you get a certain value, and then by looking at 0.16, you have a systematic way to write the equation of the tangent at the curve. Well, suppose you want to turn the tangent to a differentiable curve at x at point x0, y0. Well, we can replace, not systematically, right, for the curve f of x and g of x now being the derivative, then we compute g of x at x0 and get a certain constant, and then we write the tangent line. So the fitting instruction of the schematic argument would be Replaced by the description of a function under consideration. Replaced by the derivative. Replaced by the value of geotag that takes zero. Classification, 1 and 2 are premises. 3 falls from 1 and 2 by count of zero. Notice that it's bicalculus, which means we're not saying exactly what logical patterns are used, in fact, in that particular inference. This example was tailored to mirror exactly the one that Kircher has for Newtonian mechanics. Okay, now, I will not get into the details of exactly how the best explanatory source to be determined, but let me give you the intuition. Basically, the best explanatory store, or the explanatory store over K, the best systematization of K, is obtained by looking at three types of parameters. One of them is looking at all the possible systematizations. Choose the one that maximizes the following factors. Fewer number of patterns, the better. Second, there is an extra conditional stringency of patterns. I cannot get into that because it would take too long. Finally, the best systematization is the one that will account for as many as possible of the truths you want to account for.

1:30:00 So, maximize if you can account for all the truths. That's going to be the best. So the best systematization is directly proportional to the fewer number of patterns and inversely proportional to the quantity, as it were, of consequences that you can get out of it. And as I say, you know, we can make this a bit more precise, but I don't want to get into that because that would take too long, and if you've seen it, you know what it looks like. If you haven't, you wouldn't learn it just by looking at it transparently, so either way, I think... Now, there's only one thing I want to mention about a modification we have to make in order to really test this Kichererian model against the mathematics case. The way in which teachers assess the issue is very limitative for when you try to apply it to systematic cases in the history of math or to mathematical practice. The reason is this. If you look at the way the systematizations work, they have to start from sentences in K and infer things in K. But normally what happens in the history of science, and mathematics in particular, is that great advances in unification, or sorry, in explanation, are obtained by enlarging your language so that, in fact, Previous phenomena that were, in fact, unexplained, so to speak, now fall into context by appealing to a larger language, so that we do modify its definitions, and by doing this we actually have even some textual evidence that Kicher would be very sympathetic to doing that, that he realized the need for doing that, by allowing, in the best systematizations, that although the sentences inferred are in K, The premises from which you can infer them come from a superset of K and a superset of the language of K. So we might appeal, let me give you an example. You won't explain in math what's the advantage of studying the solution of equations by radicals that Lagrange gives us in comparison to Viet. Well, it's a whole new conceptualization. What advantage do we have in looking at a certain way of looking at the solubility of equations in Abel and in Galois?

1:32:30 It's the new whole structural or generalization that allows us to use the Weider language to explain facts that were already known but now in the Weider context they seem to receive the explanation. The general setup from future. Now let me get a bit to the algebraic geometry part, to the real algebraic geometry. The test case comes from a book by Brownfield written in 1979 called Partially All the Rings in Semi-Algebra Geometry. And the first quote is key because I hope it will serve as a representative sample of the fact that explanation does come up in mathematics and people have strong feelings about it. So in this book, we absolutely and unequivocally refuse to give proofs of the second type. I'll explain what that second type is. Every result is proved uniformly for a real closed ground field. Our philosophical objection to transcendental proofs is that they might be able to prove a result, but they do not explain it, except for a special case of real numbers. Now, of course, I have done a lot of work previously on studying even the history of this notion of mathematical explanation, starting from the Greeks. There is a lot of evidence, well into the 20th century, on the opposition between proving and explaining. It's found in the posterior analytics by a response in a very clear way. But it's interesting that here we have someone immersed in contemporary mathematical practice saying, I'm not going to be using a certain type of proof because although it does prove the result, it won't explain it. So let me tell you something about the context of this. In real algebraic geometry, you're basically starting with two real closed fields. That's a field which at least in unique ordering, such that every positive element has a square root and every polynomial of degree has a root. I'll write the axioms there. I won't say anything about them in particular. But the thing about this system is that it's... Decidable and complete. So we have a decision procedure for this system such that, due to Tarski and Seidenberg, such that if you pick any phi in the language of this theory, you can run the algorithm and basically have an answer as to whether in fact phi follows from the axioms and is true, or the negation of phi follows from the axioms and is true in that case too.

1:35:00 As a consequence of the completeness of the system, you have a property, which in model theory is called a transfer property, which serves as a form of... Look, if you want to prove something about all real closed fields, here is how you might go about it. Show that in R, that, you know, the paradigmatic example of a real closed field is a sentence by holes. Then, you can lift it and conclude, because of the transfer theorem, that is true in all real closed fields. Where is the catch? The catch is that when you're showing that in R, phi holds, you might be making, you might be appealing to facts that are specific to R, to the real numbers, and that do not hold for the other real closed fields. That's the kind of proof that, in fact, are rejected by Bramfield, because he says, What you're appealing to is the peculiarity of the series of real numbers. For instance, you might be appealing to completeness of the real numbers, which doesn't hold for the other real close fields. To give you then the large sketch, what Brampton rejects are a type of proof that might appeal to the decision procedure, right. You might be thinking, look, one way to prove this result is clock phi into the algorithm. If you get one at the end, you know that phi is a theorem. That's one way to go about proving results for the theorem. It's of course completely, as it were, uninformative and Basically, you won't get explanations of results of what phi is true just by running the algorithm, but that's one way you could go. Second type of proof is the one that I just mentioned, using a transfer theorem. The third type of proof, which is the one preferred by Brownfield, and is the one that he calls explanatory, is one that uses the uniformity. In other words, it appeals only to proofs that uniformly apply to all real field. I had an example to make this a bit more concrete, but I won't go through it because the time is short. I will simply flash the statement.

1:37:30 It was the result, actually there are some definitions about semi-algebraic sets, but the result was the simple one, the one you're familiar from the chemistries. A polynomial S of X1, Xn assumes a maximum value of an inbounded clause semi-algebraic set S in Rn. We give three proofs. One using the decision procedure, one using the transfer theorem, and one using the uniform method preferred by Granville to see what the difference really is in a specific case. Now, let me say, let me get to the punchline here and say why we think that this is a real challenge to what the teacher is doing. Well, the thing is that we'd like a model like the teacher one to be able to make the right predictions about cases of mathematical practice, where in fact people claim that sometimes the proofs are more explanatory than others. But because the whole system is really centered on this notion of paucity of patterns, the fewer the better, what turns out to be the case here is that the first type of proofs, the ones that rely on the decision procedure, are the best ones because, in fact, we can... Okay, so here's the setup. We're trying to account for all the elementary truths. In the first case, we can apply a single argument pattern that says, so f now stands for the functional algorithm, think of it as a lambda term, which is the algorithm. So if f of a sentence phi equals 1, then infer phi. That's a single argument pattern that is going to account for all the truth of real close fields. By contrast, when you go to proofs of type II and III, the kind of argument pattern that you need to prove the theorems about polynomials like this one is useless when applied, say, to proving the Brauer fixed-point theorem. You're not going to be using the same pattern. It doesn't even make sense to think of using the same pattern. It's going to be a different type of derivation so that in cases two and three, they're already ending up with infinitely many patterns. So we claim then that what this shows is that the notion of unification that Kircher has makes the wrong predictions about cases in mathematical practice because it favors accounts which might unify but are completely unexplanatory and doesn't make, in fact, the right distinctions.

1:40:00 In fact, even when you leave on the side the case of proof one and you focus on two and three, There is not really a clear-cut answer that teacher model can give as to whether we have a preference for proof types 2 or proof types 3 for the simple reason that everything becomes very complicated by the existence of the infinitely many patterns. And once you have the infinitely many patterns, the little schema for computing which one is the best to restore doesn't seem to apply in any... I'll stop there. Thank you very much. I'm wondering whether Kitschel's model has some resources to answer your challenge. Let me just bring it up and see what you think. Let me say what I have in mind. When evaluating different planetary stalls, there are three criteria in Kitschel. You focused on the first and the third, the fuel patterns, more consequences. You mentioned the second one, the stringency, and then didn't go into that. The stringency one, as I understand it, has to do with when we should count arguments as similar, and there are two dimensions, same logical form and same non-logical vocabulary. It's actually what we inject in the... So on the surface it looks like the one that uses the decision procedure is... Very good in the first respect, one logical pattern, but maybe not so good in the second respect. So I'm not sure the Kitscher model would predict, if you factor that in, I'm not sure it would predict. Well, let me put it this way. This is an important point, and we are addressing it in the paper at length. But the short answer is that I don't see how Kitscher can really appeal to it to get out of trouble. For the simple reason that even in his description of how stringency works, he admits that he has no real clear idea about how to define the notion of stringency and it sort of takes it as implicitly defined by the final equation, so to speak, about what counts as the best unification.

1:42:30 So we're actually giving Kicher a lot of leeway in terms of addressing that question. Showing why it can't be a reply. One thing that also occurred to me though was that if you take this notion of stringency seriously, it will turn out that in logic, where there are normal logical constants and so no stringency to be talked about, there are no explanations. That I find also rather surprising. And of course if logicism is right, then there are no explanations in mathematics, but that's a big if to be charged. At least the way you presented it, it seems like your case supports the Steiner proposal to a certain extent, because what this writer seems to be saying is that we want to give the proofs in terms of real closed fields, not in terms of some particular real closed fields. So there's some notion that the proof should live with the intrinsic features of the... What is the generalization of the entities that we're talking about, rather than some sort of more accidental instantiation, do you think that's... That's correct, but it only goes toward meeting one of the criteria of Steiner. There is the issue of generalizability in Steiner that brings a lot of problems. In other words, that explanatory proofs are all those ones that also could be generalized, and it's not at all clear, you know, in what sense you can generalize some type of proof of this sort. I'm not excluding that, for instance, Steiner's model on my account for some of these cases, or some cases of mathematical explanations, I mean, we addressed Steiner at length in that paper with Asner last year. Here, you know, I would say that it's the generalization issue that brings trouble. In other words, the final proof is not what gets judged as explanatory, you have to see that that final proof also gives rise to A generalization that goes beyond it and I just can't, I see where that would go. I'm afraid we don't have time for any more discussion.

1:45:00 So our last speaker is Derek Repp from the University of California Riverside. Getting him started on reasoning and mathematics. I feel like my talk maybe shouldn't have been the first one here because it puts into context the number of things that went on in the earlier talk. There will be a lot of connections, but I will be painting with a pretty broad brush, and on the other hand, then maybe getting my talk at the end, you already have some of the details to be plugged in. Philosophy of mathematics there has been a broadening recently beyond foundational, narrowly logical, and also metaphysical investigations, but I think a broadening in a number of ways, but one broadening I'm particularly interested in and that this symposium is about is taught what some people call a new epistemology for mathematics or taught a broader investigation of methodological issues. And because of that broadening, there used to be a lot of context between philosophy of mathematics and philosophy of science. I think here we potentially have again some very interesting connections between the two fields. That's why I proposed a symposium here. I thought at a philosophy of science conference this would fit in. We will highlight here, although I'm interested in, have to do with the notions of style of reasoning and explanation, so there's a lot of connection to what you just heard. But I will be looking at, I'm doing research on historical figure, Richard Dedekind, so it will be in connection with him. It will be pretty programmatic. I will basically report on some recent research, some will make you aware of it, which I thought might be worth doing. We try to make some connections within that research and with these notions of style of reasoning and explanation.

1:47:30 I think there's an issue I'm interested in is how exactly to frame discussions about new epistemology or new methodology. Jeremy was already talking about it in connection with emotional understanding. So what's a good way of framing it? That's what I'm interested in. So it's somewhat meta-philosophical, also, what I will be doing. Okay, so very briefly on static end. So, Dedekind is quite well known among philosophers of mathematics and science for a couple of things, most famously maybe his introduction of Dedekind cuts to introduce the real lumbo, the rigorous definition of the real lumbo. It's often seen as part of the arithmetization of analysis. This is in his paper Continuity and Irrational Lumbos. Then there's his logistic treatment of the natural number, the natural meaning of numbers, including a formulation of the Dedeck and Kerner axioms, a proof of categoricity, analysis of induction, then also... He contributed some early contributions to set theory, so the paper, The Nature and Meaning of Numbers, has a definition of infinity, being Dedekind infinite, and in his correspondence with Cantor, he made some trouble. So I think these parts are fairly well known and have been taken to be central in the philosophy of mathematics, philosophy of science. A little less so are the following. So this concerns now some other parts of Dedekind's work. Among mathematicians, or in the history of mathematics, he's maybe most well-known, besides for his theory of ideals, the study of algebraic number fields, which he presented in several supplements to his edition of Eureka's lectures on number theory. He also made some other contributions to algebra. For example, he gave a model in the first presentation of Galois theory and some other things, and then he applied this to the study of Riemann surfaces. So these are some things that until recently were not studied very much by philosophers of mathematics, but now there's interest in it, so that's what I will be talking about.

1:50:00 So the point will be, what's the philosophical interest of those things. Here it's pretty established, the philosophical interest of people in that area. What about here with those things? Now just, this is my report here on some recent work. So a couple of papers have come out recently. In a paper I published, I present, maybe this is more in connection with his definition of the natural and the real numbers, I present him as a precursor of, as I argue, an attractive alternative to structural disputes about mathematical objects, so this goes back to metaphysical issues in the paper listed. They present him as an important influence on and precursor of Hilbert and Bernays abstract formal axiomatics. Now Morse, getting closer to what I want to talk about today. So what I'm interested in, what's motivating me is I want to put this first part, what I've claimed about his metaphysical views, in the context of these methodological issues. I think that there are important connections and that's what I'm trying to figure out. So in that connection, there's a somewhat older paper by Harold Stein from 1988 in which he, that's guiding my investigations, in which he sees Dirichlet, Riemann, and Dedekind as central figures in what he called the second birth of mathematics in the 19th century. More recently, there are several papers by Jamie focusing on Riemann and his influence on Dedekind and Frege in particular as part, similarly, of a methodological revolution, as Jamie calls it, in the 19th century. Then there's a paper that just came out by Jeremy. On the methodological significance of Dedekind's study of algebraic number theory, his theory of ideals, and there are some earlier studies of that too that are quite interesting to read and evoke. I will be looking at Jeremie's echoing topic as a resource.

1:52:30 And then there's also some relatively recent work more on the significance of this, or generally his work on set theory and algebra. So, quite a bit of interest in the methodological side of dedicating now. A little bit more about that. So, in my paper, I attribute a particular structuralist view about the nature of mathematical objects to him, so I have a particular reading of that in my defense. Moving to the more methodological issues, in Stein's paper, he presents Dirichlet and then also Riemann and Dedekind, also the former group that's closely connected, as the proponents of a novel conceptual approach to mathematics, or they see mathematics as the free exploration of conceptual possibilities. What I'm particularly interested in is this idea of conceptual, a conceptual approach. I think it's a very suggestive proposal, but what does that mean, what does that amount to really? In Jamie's papers on Riemann, he mentions things like the following, that Riemann's study of mathematical functions in terms of their essential characteristics, related to some of the things we were talking about, or other things like the presentation-independent characterization of mathematical objects, or the emphasis on global definitions. As part of the methodological innovations in Riemann. In Jeremy's paper, he talks about Lelikin's use of set theory constructions and non-constructive reasons, but then also the study of algebraic notions and structures in terms of fundamental characteristics, again, so there's a direct connection. I think that's the connection I'm interested in, this appeal to fundamental characteristics, essential characteristics, and a conceptual approach. And proofs based on the latter, not on external forms of representation, so it connects to all the papers we've already seen. Now for me there's also, so this is what I would do, actually what I'm presenting is more, here's a project I want to pursue. For me in the background is also

1:55:00 Something else that I hope will allow me to connect these methodological issues with the more metaphysical issues. Ernst Cassirer in his book Substance and Function from 1911 actually takes Dedekind as a very central figure. He has this account of the development of modern mathematical science and he sees Dedekind as a central figure. This is the title of the book. Away from the old Aristotelian notion of substance, a mathematical notion of function, a movement taught the determination of mathematical objects in terms of their functional and relational aspects, and then mathematics as the general study of relational structures. So there's this big view in Cassiro that this is what happened, and I think these recent studies fit into that. Now, how is this connected to the notion of style of reasoning? When I thought about this recent work on Dedekind, the methodological side, I wondered what are some good, some fruitful terms in which to frame these things. And it occurred to me that the notion of style of reasoning that I had seen in philosophy of science. The publications, I noticed that some people are already using that. So, Edward, in his study of the Genesis of Ideal Theory, where he compels Dedekind and Kronecker and argues in favor of Kronecker, says he admits Dedekind's legacy consisted not only of important theorems, samples, and concepts, but of a whole style of mathematics that has been an inspiration to each successive generation. Similarly, when you then look at, for example, Jeremy's article and Jamie's paper, too, on Riemann, they use the notion of style, too. So there's a style of reasoning in Riemann, different from the style of reasoning in Biostrasse. There's a style of reasoning in Dedekind, different from the one in Kronecker. But what's the notion of style here? That's the meta-philosophical issue I'm interested in.

1:57:30 I think it's pretty clear that we need to put, I mean, style is used in a lot of different ways. It's pretty clear we should put aside the use of the notion of style in the sense of a personal style, like the style of a writer. That's not what this is about. Also, I mean, sometimes there's a... A very helpful paper that's not published yet by Paolo, in which he, listed at the bottom, in which he looks at the use of the notion of style to talk about the development of mathematics. And I think as he documents... Some writers who talk about style in mathematics do. They talk about national style, for example, German versus French style, and maybe also personal style. I want to put those aside. Similarly, one can use style in a merely aesthetic sense or in a merely pedagogical significance. I think the notion of style we need here has to be more to it than that. I think, I mean, Edwards doesn't say much, but sometimes I get the sense a little bit that he credits Dedekind with this new style, but then he tends to think of it as just this pedagogical aesthetic thing. He was so good at presenting things clearly and so on. Now, I think what we really want here is something like a notion of a cognitive style or methodological style or a style of reasoning. And what I want to claim is that in Dedekind you get, in that sense, the emergence of a structuralist style of mathematics. There's no conformity in how to talk about these issues, so people talk about this in Jeremy's paper, he talks about sets of philosophical principles or mathematical values. Some other people have used the term image, an image of mathematics for this. I would use the notion of style of reasoning here, and I think Ian Hacking, in his work, is pretty close to what's useful here, the kind of style we are talking about.

2:00:00 Hacking's notion is based on the work of the historian of science, Cromby, so he picks it up from there. So, Hacking says things like this, every style of reasoning introduces a great many novelties, including new types of objects, evidence, Sentences, new ways of being a candidate for truth or falsity, laws, or at any rate modalities, possibilities. One should also notice on occasion new types of classification and new types of explanation. So part of what I'm proposing is I think one can look at that recent work on these methodological issues through that lens and look at a number of these things. I'll come back to the explanation in particular. Now, what's useful about the notion of style? Oh, there's another paper by Arnold Davidson in which he also looks at this, he's following, following Hacking, in which he looks at the notion of style involved here. Now, Hacking, following, Davidson, Hacking, following Hacking says the following styles of reasoning give systematic, systematicity and structural, systematicity, structure and identity to our thought. There's sort of a package here, a gestalt or something like that. That notion of style captures. So what is that? To see what that is, one thing one can do, so what I'm now wondering is, so what can one do here? How can one use the notion of style? Well, one thing one can do is look at contrast. So if there's the structuralist style in Dedekind, what's, as opposed to what? If this is sort of one gestalt, what's the alternative? You can find Kronikov with his alternative development of ideal theory. So by studying the two, the Dedekindian style stands out more. So in Kronikov, unlike in Dedekind, you get the rejection of infinite sets, the infinity set of the use of set theory.