Formal Verification and Mathematical Understanding (& others) (contd.)

0:00 But if you note, when Hilbert produced this non-constructive group of the sparsicides concerning algebraic invariant, a response by some mathematicians was, this is not mathematics, this is theology, so a rejection of that style. And then you get the development of intuitionistic or constructive mathematics as a counter-proposal, as we need a different style here. Always looking at those things is that here the structuralist style gets defined negatively, really negatively, where you don't restrict yourself to the finite and you don't restrict yourself to constructive proofs. But that in itself doesn't tell us yet what we gain using the structuralist style. Following this idea that a style forms a kind of unity, another thing Hacking and Davidson proposed is look at the determining concepts and their opposites and how they combine to form a style. So what would be the determining concepts here for this Dedekindian style? Here is what I, by looking at this recent work on Dedekind and what I found. So in David Kim's approach to mathematics, we get the free exploration of conceptual possibilities as opposed to restriction to study just quantities or things directly connected with old established applications or to what's intuible, so broadening out of mathematics beyond that. You get the emphasis on general proofs related directly to fundamental concepts versus what, now this is from the point of view of Dakin, versus blind calculation, the brute force of formulas, extrinsic aspects. You get the use of a general notion of function and set as tools versus a restriction tool, some more formal things, effectively computable things and finite things. You get an attention to entire structures and their mappings, as opposed to looking at mere numerical or formal attributes of particular things connected to particular representations.

2:30 You get the determination of the most general class of structures for which a result holds, versus a study of particular structures and things closely tied to notation. And you get the characterization of mathematical structures in terms of functions and relations, this is not connecting it with Casillo, versus follow or intuitive constructions. Now, I think all I've said here is... To give you a bit of a sense by using some words in which the style has been described of what I mean by structuralists, to give this real content, one has to actually look at the mathematics, in this case, what is to do. I think it's somewhat useful to think in terms of these overall features of the structural style, but then one has to go to the actual mathematics and give it real content. So one has to go and study how data can develop ideal theory in terms of set theoretic constructions, this focus on fundamental characteristics, study of algebraic integers and other structures in general. Similarly, in his work on Galois theory, Dedekind gives the first model presentation of Galois theory in the sense of presenting it as the theory of field extensions and their automorphisms, as opposed to some other ways of doing it. Back now to the natural and real numbers, he gives a characterization of the natural and real numbers in terms of methods and relations and set theory constructions. So I'm not able to do that here for time reasons, but by looking at those things, one can give real content to this earlier very general abstract notions. I can't give that to you, but happily I can refer you to Jeremy's paper for the first study of ideal theory. I think it's a really very illuminating paper in that respect. He really goes, Jeremy really goes through De Ligt's theory of ideals with that in mind.

5:00 I recommend that. As far as I know, no one has done the second one yet. I think that would be equally interesting to look at how David can develop GAWA theory and how it differs from other presentations of it. I think there's a little bit in Edward's book. Okay. Okay. And the last one is connected with my own paper, so I think by looking at those things one can see the connection between the methodological issues and the metaphysical, so that the methodological structuralism and the metaphysical structuralism come together here. The notion to use here, but there is a bit of work has been done on it in Hattling and so on, Davidson, that I find and I want to explore this verbal to make that connection. So people studying the mathematics talk about this style and there's this philosophical notion of style of reasoning and thinking about this. One can bring those together. Another thing is to the notion of explanation. In many cases, that notion plays a role in mathematics. I want to do the same thing here in this connection. Let me just very briefly say the direction in which I would go here in this particular case. Clearly, when we are talking about explanation here, we can't mean causal explanation in the narrow sense of causal. But there is a broader notion of causal explanation, causal explanation in the sense of answering a wide question with because, something is the case because, the questions of a certain kind have certain solutions because this and this. So it's that kind of notion of explanation here, so causal in this broad sense. The theories or models of scientific explanation in the literature, in terms of scientific science literature, some are applicable to mathematics and explicitly presented that way in Kitchell.

7:30 I think also Hempel's original account, that there are some interesting connections, and van Fraassen's pragmatic account, too, I think there are some interesting connections. This has been explored a bit in the literature already. For example, just to mention a few things, in Jeremy's paper on Dedekind's ideal theory, when I read it, I immediately read his description of what's valuable, what we gain in Dedekind's ideal theory. Things like this come up, subsumption under general law. These aspects come up. In connection with Kitchell, things like uniformity, unification, and the probability of arguments come up, again, very directly in journalism, nice analysis of David King. So all I'm doing is pointing out those connections to these accounts of explanation. I'm particularly interested in this idea of a conceptual approach to mathematics as opposed to a computational or something like that, and these emphasis on characteristic properties or internal definitions, to me, parts of the analysis of the mathematical work are quite in the direction of Steiner, Steiner's model. And, in particular, the following power of science proposals from the school of mathematical exploration is that an explanatory proof makes reference to a characteristic property of the entity or structure mentioned in the theorem must be evident, that is, that if we substituently approve a different object of the same domain of theorem collapses, more we should be able to see, as we vary the object, how the theorem changes in response. It may be that Steiner's notion of mathematical explanation is more local as Paolo put it, so looking at a particular proof and so on.

10:00 I want to take him, I want to interpret him or reinterpret him in a global way. So I want to take this idea of appealing to a characteristic property and so on, And so my hunch of what I want to explore is I think one can take this idea of Steiner's, probably put it, I can't go into the details of it, but I think one can easily put this, globalize it, put it in the context of Van Frasen's view on explanation, and then apply it to that particular case. The nature of the structures by which reasoning is built, and I actually would now like to read more of James' work, I would say it's actually different from Greenland. So I think there's, one thing I'm interested in here is people talk about constructive mathematics versus classical mathematics. This umbrella term classical mathematics. I think what we are seeing now is that within classical mathematics there are different sub-styles. So there's the big, what I call structuralist style. I think the Riemann style is different. There are connections. Connections are the characteristics. So I think that's the direction in which we are moving. I'm trying to understand these different styles, and I don't, my idea here is that one can, given this notion of explanation, maybe one can argue that what we get in the deconstructualist style of reasoning as developed further by Noetherian novels later on, is a certain novel kind of mathematical explanation, or to bring it back to Jeremy's account of understanding certain mathematical facts. I should emphasize, it's not the only one, so you get, there are other kinds of explanations, computational ones, so this is not meant to exclude other styles, but it seems potentially illuminated to bring this out, this gain we get from structural styles.

12:30 Not at all, I really don't like everything, but I just wanted to make a comment, I think about... This actually, just in the very last thing you said about using the term style to refer to what Dedekind is, I think when you just talk about it as a style, it seems to mask that, well, in a sense, Dedekind's style really is supposed to, I mean, he's a guest, he really is a guest, the algorithmic style, the development of ideal theory. I mean, his remarks against what, you know, against Coomer's, why Coomer's approach wasn't the right one, I mean. I would put it more as he's in favor of developing his approach and I think, I mean my If you look at the opposition here, Kronecker on the other side was much more restrictive. Dedekind, there are lots of remarks in Dedekind's work where he says, okay, develop that approach too, that would be useful too. And I'm going to develop this one, which seems particularly insightful. I think it was more just to say that if you just refer to it in style, it does seem to lose some of the philosophical force behind what he actually thought it was. The right way to go about things, which you see come out when he criticizes Kummer's approach to ideal divisors. Can you say a little more about what he thinks? I may not. Well, there's two things. He points to the fact that actually Kummer makes certain mistakes that arise out of his formulation. But then he says, but in addition... There's a kind of, I can't remember the exact words, but we might put it as a kind of a conceptual shortfall, which comes out when you generalize to higher, I can't remember the dimensions, higher something, more complex, a wider range of structures, right? The Kummer theory breaks down in ways that the Dedekind theory doesn't. So I think, you know, there really is this edge to what Dedekind is saying in these remarks. When you were presenting hacking, different styles of reasoning often have different truths following from them. I don't know the history of ideal theory at all, so I don't know if there are good examples there, but is there going to be a common place in the way you're understanding it?

15:00 Different styles are actually going to lead to conflicting theories? So from how I understand Heffernan-Davidson, that's a central theme for emotional style, that it leads to these new possibilities, and I'm not sure if it has to be conflicting, but it can, not necessarily. Right. Now in this case, using infinite sets of those techniques, and structures, studying structures more generally, those seem to be real statements. There are new mathematical statements about those kind of things. And there is a conflict with the constructivist or the mathematical kind of approach. So it seems exactly to apply here. So I found that there was one reason why I thought, oh, this is a good fit here. We've come to the close of the discussion. Let's thank our speaker.