Evening talks

0:00 Prove that you can't? That you can't. By means and... How do you prove that you can't? Well, of course. You do have, in your language, your syntax, you do have means for constructing more maps, namely just composing. That is taken as a... I suppose, as a way of terms, there's this nerd stand named on terms, which is somewhere between symbols and actual math. So the terms are closed under certain operations. So to put it entirely in that language, what I'm saying, that in order to accurately mirror the lattice of subtopologies... You need, in your language of presentation, you need a rule of term formation, primitive terms corresponding to these compositions. Is that what you're saying? No, no, the compositions are right there. You need a term formation principle which says, if I have proved that, well, why there exists a need to... Or even leaving aside the particular idea of inverting a certain map, if I can prove that a certain formula describes a graph of a map. Then I'm allowed to introduce a new term, i.e. a primitive term, which corresponds to that, with an axiom that says it corresponds to that. But now the big problem is that this violates Tarski's principle, and I think his principle was a perfectly very good principle, which is what? It's one that the computer scientists should all know about, namely the fact that whatever you mean by language, theorem, blah, blah, there are all kinds of different schemes, well-formed formulas should be a recursive set, although inevitably theorems will be an RE set, but unless the formation of formulas is something that you can understand, a priori, you see. You can't even understand exactly what the set of theorems is going to be. But why doesn't, I mean, in that context, why doesn't there's colonization of the language? I mean, because you can just stick these constants in.

2:30 You can't just stick things all over the place. That would be very inaccurate from the point of view of the semantics. You'd be introducing a whole bunch of structure that you didn't mean to be there. Well, there would be a lot of meaningless crap there. Yeah, so if you do that in group theory, it's no longer group theory. The thing that you get would have it... You just have to think seriously about the fact that every notion should have a category of models. So the category of models of that skull-mized thing might be interesting in a protecticological point of view, but it's so far away from the mathematical content that it may obscure it. Well, I mean, there's something odd, I mean, I'm not quite sure I can put my finger up, but there's something, I mean, what we're talking about is just conservative extension, definitional extensions of language, basically. And they're conservative, and they're harmless in that respect. Tarski defined, in essence, the category of theories. Where theories are always understood in the sense of presentations of signature or undefined terms. In that way, an interpretation of one theory into another one is another theory that you get by considering the disjoint union of the primitives, of the signatures. And then, in that new language... So you're putting down all the axioms you had before, but the two theories separately, plus a new axiom that says it's for all axioms, that it is a map. One of these symbols corresponds to the other one. So you see, from a categorical point of view, that's the co-graph of the map that you want. It's the quotient of the sum. You take the sum of the two theories, and you take the quotient. But again, once you have that theory, you're going to have... Sorry, that category, you're going to have composition of these morphisms by stacking three theories together, and some morphisms are going to turn out to be monomorphisms or strong monomorphisms or strong epimorphisms, et cetera, et cetera, et cetera. So, we're back to the question, in that category, suppose we look at the strong monomorphisms with the fixed domain, you see. Now, we were contemplating variable signatures all over the place.

5:00 Well, we have to still contemplate them at that level. Again, that's the point. You might think that just by, you know, just by adding axioms, you, the co-graphs would be describing all the, all the sub-theories in this sense, in this sense of sub-theory. But they're not all accounted for by sub-languages, by sub-theories in the same language. And you see, as you say, well, you could wholesale. Okay, so the way that logic is very often presented in the course that I had and many books, already one is basically taking a skew because it always starts off by saying, well, we have a countable number of predicate symbols of all possible varieties, and we fix that. So, in other words, this is the Phragian world. There's one system, and everything's going to be a subsystem of that in some way. We can have axioms, but they will, of course, apply only to some of these symbols, but these symbols are there in the background. So we could always, if we want to invert something, we could always say, well, that was the 17th symbol. That really meant to be the inverse of the 16th one, right? But you're not allowed to do that if you're going to take the category of models seriously. Because you don't know the interpretation of all those extra symbols. The models are determined independently of any particular interpretation. The models are just determined by the signature, what the models would be. But there is no variable signature. All the signatures are the same. That's what I mean. For each signature, there's a category of models. That's the more realistic. But again, I'm saying that isn't right either. So if you have all these free signatures floating around for later use, then they will have incompatible interpretations. So that's no good. And on the other hand, as it turns out, it turns out, contrary to expectation, that the category of the fixed signature doesn't account for all the sub-objects that you'd want even for that fixed signature. And you're saying that the Plotarski principle, the Plotarski-Hood technique, would be possibly useful? That's right. I remember we had a debate on that in an email a few years ago.

7:30 It was hard to get these people to realize what Tarski's principle is. But why couldn't you? And other people were saying it's not, and finally Peter Johnstone came down and said, well, it's not really important. It's very important. It is important for certain purposes. Anyway, that is the, as far as I know, the only solution to this is, in fact, to just neglect that and take as a principle a term formation. That if I can prove something, then I can introduce the term. So that idea, you know, as sort of idealistically imagined, certainly would succeed in presenting all the things that I want to present, except it wouldn't quite be a real theory in a ludologically usable sense, in all sorts of ways. But it is getting later formed. The free group on the natural numbers is a subgroup of the... Oh yes, okay, you can code arbitrary letters by strings of two letters, and then you find that this is a monomorphic interpretation of groups. Because the letters are not surprising, you can send it to the three groups generated by them. Well, I don't think that's surprising either. I mean, it seems to be that once you've got the idea of the code, then yeah. I wasn't thinking about it in the right context. If you'd said, I can get by with two primitive symbols, then I can tell you something good. But that's essentially... Right. Yeah. Now that's a good example. And I understand that. I still don't see an example of some tools that you're not able to call.

10:00 For example, in the example you were mentioning, you have a more basic... You could add a symbol for each inverse, ask that it is an inverse, and the presentation results with an extra symbol, but you could also ask for the original symbol to be blown or undead without adding an extra symbol, to be still, as if you did the correct opos, then that wouldn't be an example of a sub-topos which is expressible. I think that's right. So we need a pure example. I approve it. It's quite careful, so it should be true. I can't necessarily approve it, because intuitively... I can't explain that, but... Before that... Sorry? Perhaps there is an obvious property of genetic morphisms that if you extend the... If you extend the presentation on all the weird things, has the genetic morphism had a... all denotes a property of death? Yeah. Is it clear? I don't know. In this case, Lydia would be saying that we can really get nasty with the presentation but get all the totals. In the presentation, maybe, why don't we get what you're expecting? I think you can actually add a geometric sequence. Well, at least my proof shows that you can.

12:30 But apparently, the semantica is not so observable. Do you have it written down? I have written down the data since... That I could access it? Well, I will explain it now. The fact is... Listen, can I just... I've got to get going. I've got to make a phone call to the States, which is five o'clock. And what's happening this afternoon? Because I've got... I've got to write a letter to the bloody Medicaid people, and I've got to do it now. What's happening in South Carolina? They'll be coming back here. They'll come back here. Usually it ends up in about 2.30. 2.30? Well, I may be done by then. And I may not. I've got to find some papers. Poor old Julian. His father didn't bother to. And I've got to provide the information. I've got to provide it in Egypt.