aboutlogic #04 | Graham Priest – Working with Contradictions & Paraconsistent Logics

00:00:00: I actually think that debates about the foundations of mathematics are rather confused.

00:00:04: I think the days where we thought we could get a buy with a sort of universal foundation for mathematics is just a feature of the history of mathematics, which has now disappeared.

00:00:15: There's just a whole variety of mathematics, plural, and to reduce the whole of mathematics to any kind of a mathematics is just a hopeless enterprise.

00:00:30: Today's joining us from New York.

00:00:33: Graham Priest, a philosopher who also studied mathematics and is well known for many things.

00:00:41: Particularly, we will talk about contradictory logics or logics where we can work with a contradiction without being able to prove everything.

00:00:50: We'll talk about non-standard things, non-standard arithmetic, non-standard set theory and how all this is philosophically motivated.

00:01:02: Hello, everybody.

00:01:02: Welcome to our next episode of the Logic Podcast about logic.

00:01:07: And I'm very happy that Graham joined us from New York,

00:01:11: who's

00:01:11: quite well known for a couple of things from Buddhist philosophy to dialytism to work on the foundations of math.

00:01:21: Thank you once again for joining.

00:01:24: Well, thank you for inviting me.

00:01:26: I think there's one main theme a lot of philosophers think when they hear about you and that's dilatism.

00:01:32: Would you be so kind to say a few words about this branch of philosophy or this philosophy?

00:01:40: So in Western philosophy, there's been high orthodoxy, philosophy in the last thousand years, that contradictions can't be true.

00:01:51: And dilatism is the view that some are true.

00:01:56: Now, there have been a few people in the history of Western philosophy.

00:02:00: Eastern philosophy is another subject.

00:02:01: We can talk about that if you like, but let's just talk about Western philosophy for the moment.

00:02:06: There have been a few exceptions to the orthodoxy in the history of Western philosophy.

00:02:11: The most obvious example is Hegel.

00:02:13: That's a contentious statement, but we can talk about that if you will.

00:02:17: But generally speaking, the thought that some contradictions are true and the movement that that is so, is a relatively modern phenomenon and it comes from a slightly surprising direction which is formal logic itself.

00:02:34: So in the last fifty or sixty years we've seen the development of branches of logic called paraconsistent logic, which roughly speaking mean the systems of logic where you can have a contradiction without or hell breaking loose, which is of course a necessary condition for considering the possibility that some contradictions might be true.

00:02:55: And Dilithism is exactly the view that some contradictions are true.

00:02:59: And so this has been a debate that's going on in metaphysics, foundations of logic, formal logic now for forty or fifty years.

00:03:11: And the word Dilithia is a neologism, which I coined with my now sadly deceased colleague, Richard Sylvan, that Dilithia is just a true contradiction.

00:03:22: And so Dilithism is viewed that some contradictions are

00:03:29: true.

00:03:29: Could you say a few words?

00:03:31: What do you need to tweak on classical logic in order to omit the explosion principle that everything follows from one contradiction?

00:03:39: Are there different strengths or how to do that?

00:03:45: Look, there are many different power consistent logics and they work on very different principles.

00:03:53: Modern non-classical logic uses many different techniques.

00:03:56: And virtually any technique that you can use to construct a non-classical logic can be used to construct a para-consistent logic.

00:04:05: The important thing is that explosion has to go.

00:04:11: Explosion is the view that a contradiction implies everything.

00:04:18: If that goes... So is this

00:04:20: exfazal quad limit?

00:04:22: I mean... So is this X-Files look for a little bit or is it something else?

00:04:26: Or not P and not P?

00:04:30: Okay, X-Files look for a little bit could mean a few different things.

00:04:39: Well look, explicitly it's from P and not P, Q follows.

00:04:45: So for any P and Q, from P and not P, Q follows.

00:04:50: So it's a version of X-Files though.

00:04:54: But the explosion is connected with other principles.

00:04:59: The most obvious is the disjunctive syllism.

00:05:04: If P and not POQ, then Q. So there are para-consistent logics which retain the just disjunctive syllism, but in most para-consistent logics, that goes as well.

00:05:19: Can you maybe explain a little?

00:05:21: I mean, I'm not a... I'm not a classical logician.

00:05:27: I'm an intuitionist.

00:05:32: So for me, the question for what's truth is maybe slightly misleading or is not one which I find particularly enlightening.

00:05:46: But I guess for you, truth is quite important, right?

00:05:51: No, it isn't.

00:05:52: I mean, the view is that some contradictions are true.

00:05:55: What I mean by truth, anything, you can choose, right?

00:05:58: And it can be an intuitionist notion of truth.

00:06:00: It can be a notion of truth where truth is identical with warranted assertibility.

00:06:06: It can be a correspondence theory of truth.

00:06:08: It can be a deflationist theory of truth.

00:06:10: It can be a coherency of truth.

00:06:12: I don't mind.

00:06:12: I mean, I think the view is interesting, arguable.

00:06:19: exciting, whatever you think the notion of truth is.

00:06:25: So I would say for me, more important is the notion of evidence.

00:06:30: How does this fit into your framework?

00:06:32: I mean, yeah, okay, so tools is maybe just a word, a proposition of rules if I have evidence for it.

00:06:41: And users say, okay, you could use this as tools or in a more generalized sense, tools values, right?

00:06:52: Unless you think that truth is identical as verification, which is a view, but not one that I hold, then there's a distinction between what is true and what's known to be true, at least rationally believed to be true.

00:07:05: And that's the question of evidence.

00:07:08: So as David Tume says, the wise person apportions their beliefs according to the evidence.

00:07:15: If I say that some things are true and you ask me, well, give me some examples, and why should I believe those are true, then we turn to the evidence for such claims.

00:07:24: And that, of course, is going to depend on what those claims are.

00:07:33: Yes, so I would actually identify whether I have propositional hopes, whether I have evidence for it, and I guess that's the difference.

00:07:44: Yeah, especially when we think about mathematics, I mean reasoning in mathematics.

00:07:51: So to me, mathematics is something I construct in my head.

00:07:55: So the notion of truth, which applies to the real world, is maybe a bit more problematic, if you, or is certainly more problematic, if we apply them to constructions, we perform our head.

00:08:16: Well, Okay, I understand what the notion of truth is in intuitionist mathematics.

00:08:27: You'd have so many more about what you understand truth to be outside mathematics.

00:08:37: So maybe I should ask you that before we continue.

00:08:45: What was the question again?

00:08:46: What was the tool's outside of mathematics?

00:08:49: It means realist notion.

00:08:56: Not everyone needs the truth, that's like mathematics is realist.

00:09:09: In quantum physics, this is also doubted, I guess.

00:09:14: So, okay, I think I would adopt this, the terrace of, as you say, different perspective.

00:09:26: of reasoning and realism or is an idealized or a caricature of reasoning which I'm just using it to contrast it with reasoning in mathematics because I mean reasoning about the real world refers to objects which which we think we completely understand, which are outside, which are not, which are observable.

00:09:58: Okay, I understand.

00:10:00: But look, that's that's a bit of a, of a of a caricature, right?

00:10:06: Okay, but look, we reason in a certain way when we do interest mathematics, we reason in a certain way when we do classical mathematics, we reason in a certain way when we do para-consistent mathematics.

00:10:18: I don't think that's terribly contentious.

00:10:24: So I guess maybe this is another key phrase for questioning you about pluralism and logic and maybe pluralism and pure mathematics and maybe even pure pluralism and applied mathematics.

00:10:38: So how far would you push this idea that there are simply different things they stand next to each other?

00:10:45: There's not one true logic or Not one true mathematics or not one true applied math.

00:10:52: What are you?

00:10:53: Oh,

00:10:53: I think it's absolutely crucial to distinguish between pure mathematics and applied mathematics.

00:10:58: Pure mathematics is the study of structures abstract structures And we know there are abstract structures which are governed by classical logic, abstract structures which are governed by intuitionistic logic, abstract structures which are governed by para-consistent mathematics, and you don't have to be a dilatheist or an intuitionist to find these important and interesting structures.

00:11:19: So, am I a pluralist about pure mathematics?

00:11:22: Absolutely.

00:11:23: When you apply a piece of mathematics in physics or linguistics or biology, you have to choose the right bit of mathematics to apply.

00:11:33: which is the right bit of mathematics to apply will depend, well, at least in the first instance, whether it gives the right empirical results.

00:11:42: And that's always going to be an issue.

00:11:45: So, I mean, there is an issue when you apply mathematics about as to which is the right bit of pure mathematics, or at least, which is the best bit of pure mathematics.

00:11:57: That doesn't arise when you're just doing pure mathematics.

00:12:01: So you were saying that different kinds of mathematics, maybe classical structures or intuitionistic structures, are appropriate for different applications, right?

00:12:15: And I wonder whether there is not, while there is maybe not the perfect logic or a perfect system, whether some systems are maybe in a way better or... better suited than the others?

00:12:34: Well, that they are is undeniable.

00:12:37: I mean, just consider geometries.

00:12:40: I mean, there are many geometries, right?

00:12:43: And until relatively recently, it was assumed that one was the correct geometry for what you might call the canonical application of geometry, namely the charting the spatial or spatial temporal structure space.

00:12:55: But now we think it isn't.

00:12:57: So we've changed.

00:13:00: what we think the best mathematical structure is for that application.

00:13:04: Right.

00:13:06: But this is not really going through the foundations of mathematics in a way.

00:13:11: This is a particular way.

00:13:14: I mean, for us, as you say, to model something in the real world geometry, and it turns out that Euclidean geometry is not the right one for the relativity.

00:13:29: and so on, right?

00:13:31: But does this really affect the sort of foundations of reasoning?

00:13:35: Okay, if you want to talk about the foundations of mathematics, you're not talking about applications anymore, you're talking about pure mathematics, right?

00:13:42: Yes, yes, that's true.

00:13:43: And I actually think that debates about the foundations of mathematics are rather confused.

00:13:51: I think the days where we thought we could get a buy with a sort of universal foundation of mathematics is just a feature of the history of mathematics, which has now disappeared.

00:14:02: I think one should recognize that there's just a whole variety of mathematics, plural, and to reduce the whole of mathematics to any kind of mathematics is just a hopeless enterprise.

00:14:18: Could you maybe help us to think about mathematical structures where para-consistent logic is the counterpart, so to speak, in the foundation?

00:14:27: We had some constructive math in this podcast already when Thorsten talked about his research.

00:14:33: We assume classical maths.

00:14:35: So to speak, how would a structure look like where paraconsistent logics comes into play?

00:14:43: Well, there are many well-known inconsistent mathematics, set theories, topologies, arithmetic, and so on.

00:14:53: So for example, based on certain paraconsistent logics, you can have axiomatic theories of arithmetic, which are complete.

00:15:04: They're inconsistent.

00:15:06: But what Goelzer actually tells you, and I'm going to challenge this result, is that any arithmetic of a suitable expressive power is either inconsistent or incomplete.

00:15:20: Now, if you're using classical logic and it's inconsistent, then it's silly because everything is holes, right?

00:15:26: But if you use a paraconsistent logic, that's not true.

00:15:28: And we know that there are axiomatic mathematics, systems of mathematics, which are complete in the sense that everything true in the standard model is provable.

00:15:38: So for any p, p or not p is true.

00:15:41: But of course, they're inconsistent.

00:15:44: And these structures are well known.

00:15:47: There's various open problems concerning them, but the systems themselves are relatively well understood.

00:15:56: I mean, Gürtel's theorem also holds in intergenistic mathematics.

00:16:00: It's not dependent on classical reasoning.

00:16:04: Sure.

00:16:05: In fact, it invokes very little mathematical reasoning.

00:16:13: You certainly don't need classical mathematics or the full strength of intuitionist mathematics.

00:16:18: You're absolutely right.

00:16:24: Let me try to push this debate like within pure mathematics.

00:16:28: Is then there a debate to be made about theory choice there?

00:16:32: saying this particular research program yields to structures that we can handle quite well or is more fruitful?

00:16:40: No, I don't think there is a question of theory choice as far as pure mathematics goes.

00:16:47: You don't have to choose whether you want to be Euclidean geometry or Riemannian geometry.

00:16:53: They're both Yorkshire's.

00:16:53: You can do both, right?

00:16:56: Theory choice arises when you apply a piece of pure mathematics for a particular application, then there is a question of which one gives you the best results.

00:17:07: And if you want to say that when you're applying the mathematics, it gives you a theory of what it is you're applying the mathematics to, then you have a question of theory choice.

00:17:20: Yeah, I'm a little puzzled whether there isn't like a question of fitting to the way we think, or I mean, maybe this is an artifact of how I was raised, so to speak, and if I

00:17:34: would have been

00:17:35: raised.

00:17:36: The way we think is a matter for cognitive psychologists.

00:17:41: And what we know from cognitive psychology is that most people don't reason very well.

00:17:49: What logicians do is study norms of reasoning, not people how people actually reason.

00:17:56: It's an idealized form of reasoning, not common.

00:18:05: But your paraconsistent logic, are they not applicable more to some kind of epistemic reasoning?

00:18:12: Are you not trying to model how people in a very reason?

00:18:16: You just said you aren't.

00:18:18: No,

00:18:21: I leave that

00:18:23: to cover the psychologists.

00:18:27: So you wrote a book about non-classical logics and this is sort of less stuff like intuitionism and some other.

00:18:37: other logics, which I would call epistemic.

00:18:42: And what I wonder is, don't you think there is a difference between intuitionism and these, what I would call epistemic logics?

00:18:51: Or is this just, I mean, it's all subsumed under non-classical, right?

00:18:59: I'm not quite sure you mean by epistemic logics.

00:19:03: There are epistemic logics standardly so-called, and those are branches of modal logic.

00:19:08: But look, a non-classical logic is any logic which is different from Frege Russell logic.

00:19:17: And as you know, you know, the twentieth century has seen the development of many, many, many non-classical logics.

00:19:24: that the book you're referring to that I wrote is a textbook.

00:19:27: And it just goes through the gamut of many by no means all non-classical logics explaining what they are.

00:19:35: The distinction is non-classical, right?

00:19:41: So you're, in some sense, interested in the notion of tools, whereas when I, coming from intuitionistic logic, as I said already before, interested in the notion of evidence, and because, for me, I mean, reasoning, I guess it's pure mathematics, is some kind of storytelling, and hence I find this.

00:20:03: So if classical use is Boolean, we're completely misleading.

00:20:12: But to me, the mathematics I think in or I work in is interstitial reasoning.

00:20:23: The idea of evidence is central.

00:20:26: I think you said earlier that notion of evidence is not something which interests you.

00:20:30: particularly or this identification is not something.

00:20:33: No, I

00:20:33: didn't

00:20:34: say that.

00:20:36: I said, I mean, if you want to know which contradictions are true, of course, you have to engage with the evidence.

00:20:43: But look, I'm not a philosophical intuitionist.

00:20:49: I know that you are.

00:20:50: Okay.

00:20:51: Despite that, I know what systems of intuitionistic mathematics are like, you know, I've written.

00:20:57: many papers like Trailster and Dumbit and so on.

00:21:01: And I can investigate those when I put my mathematical hat on.

00:21:06: And I know what moves the legitimate and what are not.

00:21:09: Okay.

00:21:11: And there's perfectly good mathematics.

00:21:13: I recognize an interesting mathematical structure when I see one.

00:21:16: So even though I'm not a philosophical intuitionist, I understand intuitionist mathematics, and I'm happy to engage in that.

00:21:24: know, bit of pure mathematics when the occasional rises.

00:21:29: But I put it to you that you understand what classical mathematics is.

00:21:35: So you know how to do classical real number theory.

00:21:38: Oh, sure.

00:21:40: I bet you were trained as a classical mathematician.

00:21:43: And you know how to prove things in classical real number theory.

00:21:47: All right.

00:21:48: So and you know that it's kind of interesting mathematics, interesting mathematical structures, right?

00:21:54: So just like I'm not an intuitionist, but I can engage in intuitionist mathematics.

00:21:59: You're not a classical logician, but you can engage in classical mathematics.

00:22:03: So I don't, I don't, that's not where the dispute lies.

00:22:08: No, but okay, may I add a bit to this?

00:22:12: Yes, I mean, first of all, I'm not, I wasn't educated as a mathematician.

00:22:15: I was actually educated as a computer scientist, and hence lots of my intuition is based on what you can do with a computer in a day.

00:22:28: So to some degree, I would say I avoided this brainwashing which happens in mass departments, I would say.

00:22:38: And to me, I can formally do classical moves, or I may sometimes also do classical reasoning myself, but I feel it's a bit like A bit like cheating.

00:22:56: Something is left out.

00:23:00: The reasoning doesn't seem to be a bit of an imprecise reasoning.

00:23:11: And the proofs don't explain very well why I would accept some resilience.

00:23:21: Well, I mean that that's your view.

00:23:24: I mean we seem to have a lot of mathematics that not the same but Of course it you can do.

00:23:31: constructive proofs Shouldn't be identified with intuitionism.

00:23:35: Okay, but clearly constructive proofs give you more information than classical proofs.

00:23:41: and so why not?

00:23:43: oh because Why aren't?

00:23:46: well because intuition is a form of constructivism, but as you know, there are other forms Right?

00:23:51: Okay.

00:23:52: You mean like something like Markov's principle of Russian constructivism?

00:23:57: Well, there's a branch of mathematics called constructive mathematics, which uses, which reasons?

00:24:06: simply you only use constructive mathematical proofs.

00:24:13: Okay.

00:24:14: But intuitionism goes a long way beyond that because If you simply do constructive mathematics, it's a fragment of classical mathematics.

00:24:24: It's those things which you can establish with classical proofs.

00:24:27: But in intuitionist mathematics, you can actually prove things which are not true in classical mathematics.

00:24:33: For example, that every real value function is continuous.

00:24:37: So intuitionism pushes things way beyond the bounds of simple classical, simply constructive reasoning.

00:24:45: Yes, true.

00:24:46: In the sense of dammit, okay, I'm more a follower of... Martin Lowe and we usually tend to be broadly consistent with classical reasoning.

00:24:54: So I couldn't do these additional statements.

00:25:01: But I mean, I don't know about your mathematical education, but I bet you learn to integrate and differentiate.

00:25:13: So you know how to operate integrals and differentials.

00:25:17: And I'm sure you use those all the time in your work, right?

00:25:20: So I'm sure you know the theory of classical reels.

00:25:26: Yeah, I mean, okay, I'm not doing much work on the real numbers.

00:25:34: Yeah, I'm interested in it.

00:25:40: And especially, I mean, so my main area, we're working on something like type theory and There's this new idea of homotopy type theory, which is, I would say, an alternative to set theory, in a way.

00:25:59: To me, while I'm non-classical in the sense of, I would say, modern type theory, intuitionism, I find the idea of consistency quite important and useful.

00:26:15: when I have a logical system.

00:26:16: What

00:26:16: it is in the area you work in.

00:26:18: Because

00:26:20: in your branch of mathematics that interest you, if you get a contradiction, you're in real trouble, right?

00:26:26: But this is not the case in all pure mathematical structures.

00:26:31: But by the way, I mean, so sometimes, especially when we do formal proofs, they can get quite complicated.

00:26:39: And so then temporarily you accept your work in inconsistent theory because it makes life easier.

00:26:48: So one example is like the predicate of hierarchy.

00:26:52: of of types.

00:26:54: I mean there's types different levels.

00:26:57: if you quantify all types you always raise the level.

00:27:00: also if you quantify all propositions you raise your level and keeping tracks of these levels can be quite technically complicated.

00:27:10: so sometimes I just say okay let Let there be a type of all types and I work on this inconsistent theory.

00:27:18: And I wonder if I can get some help here from you.

00:27:24: I mean, to me, it's more like a meta.

00:27:27: It's like, okay, something I know I'm cheating.

00:27:30: Yeah.

00:27:32: And I rather avoid this, but for practical reasons, I'm quite happy to cheat for a while.

00:27:39: Yeah.

00:27:42: I mean, that's interesting.

00:27:43: I mean, mathematicians usually do not reason formally.

00:27:50: Okay, if you open a page of any mathematics journal, you will not see any formal proofs.

00:27:55: Sure.

00:27:58: We reason sort of heuristically, and we think that in the end, it could probably be formalized.

00:28:04: But often that's just a sort of an assumption, and it can be a well grounded assumption.

00:28:10: But when you make the sort of assumption that you've been talking about, you probably make the assumption that it's not really essential, it's just convenient and it could be dispensed with when you do things, you know, in a kosher fashion.

00:28:30: I mean, people do naive set theory all the time, which we know to be inconsistent, but it's usually there's an assumption that when we do this, it can be legitimized in similar Frankel set theory or something like that.

00:28:43: I mean, sometimes it's literally a ritual, right?

00:28:46: You just say it at some point, oh, I chose my right extension of ZFC, but not a minute was spent whether you are even using ZFC, so to speak, maybe it's just PA.

00:29:00: But I think that's true.

00:29:02: That's interesting.

00:29:03: I mean, on the other hand, one more mathematicians who are interested in doing formal proofs, I mean, we have just given buzzard.

00:29:12: on this.

00:29:12: And there are famous, I mean, examples where mathematicians publish poofs, which then they had to recognize themselves were flawed, right?

00:29:27: And to sort of avoid this situation.

00:29:35: I think increasing number of mathematicians or some mathematicians start using proof assistance and computer-based tools.

00:29:47: That's true.

00:29:47: That's something which is changing.

00:29:51: That's right.

00:29:52: Well, in fact, I was up at Rensselaer Institute of Technology last week talking to people who work on computational proof.

00:30:00: And I was told, I believe these things that I'm told, that it's now been established by sort of systematic studies that something like proofs that appear in mathematics journals are actually wrong.

00:30:15: And it's been discovered.

00:30:16: Often

00:30:17: they can be fixed.

00:30:18: Yeah.

00:30:19: Well, hopefully, yeah.

00:30:23: I mean, yeah.

00:30:26: It might depend on the area a little bit.

00:30:27: In graph theory, people would agree and say, oh, most it's like very local errors.

00:30:34: There is some indices wrong, but the proof idea goes through.

00:30:38: But of course, even that.

00:30:40: might fail and the theorem still might be true.

00:30:43: Oh, of course, that's true.

00:30:45: It doesn't mean the proof is right.

00:30:46: It means it's repairable.

00:30:48: Sure.

00:30:50: Well, sometimes it can be quite hard.

00:30:52: So I think, so Vladimir Wojcicki, he got interested in former proofs as well, because I think he published a proof which he later discovered was wrong.

00:31:02: And I think... So often what you need to do is you need to add some assumptions or you need to be more precise what you're actually assuming.

00:31:09: So actually the theorem in its most general form still fails, but can be salvaged.

00:31:17: But if you're dealing with formal proofs, there's a question of what the formal system of logic is you're using.

00:31:24: that you need to formalize.

00:31:26: So, for example, if you formalize an intuition next proof, you're going to be involved in a different system of formal proof than if you're formalizing a classical proof.

00:31:36: Yes.

00:31:37: So, I mean, we use this idea that this explanation propositions as types, I mean, I understand the proposition.

00:31:49: by having an element of the type of evidence for it.

00:31:56: And there's a very natural way to assign to positions the type of evidence.

00:32:00: So that's maybe in a very interesting, because if you go like, you talk about naive set theory.

00:32:08: So Kantor identify the notion of a set with the notion of a predicate in some sense.

00:32:17: And then it turned out that not every predicate corresponds to a set, so you have to restrict.

00:32:27: This is ZF, or ZFC, where you have to restrict the collections which you can form.

00:32:35: In type series.

00:32:35: the other way around you start with collections and then propositions are emergent in a way.

00:32:44: Could I use that to ask or maybe if you want to comment on that?

00:32:47: No, no,

00:32:49: let's go.

00:32:51: Do you think it's possible to give like a very rough idea how paraconsistent axiomatic set theories look like?

00:32:58: Where is there the tweak, so to speak, from the knife conceptions?

00:33:02: or do you think it's too... technical together, idea that's

00:33:08: feasible.

00:33:08: No, let me, I think one can say a few simple things which will probably do what you want.

00:33:15: So in a moment ago when I've talked about Knife Set Thee, I was just talking about reasoning informally, okay, but Knife Set Thee has a kind of technical sense nowadays which is different and it just follows.

00:33:27: It takes us back to this assumption that any condition defines a set.

00:33:34: All right.

00:33:36: And we know that that leads to contradiction.

00:33:43: And the sort of in Zumilo-Frankl set theory, what you do is drop that assumption.

00:33:48: You don't assume that every condition defines a set.

00:33:51: Okay.

00:33:52: But a naive set theory in the contemporary technical sense is a sense where you retain the assumption that every condition defines a collection.

00:34:01: So you've got a set of all sets, a set of all sets that are not members themselves, et cetera, et cetera.

00:34:06: And of course, you're likely to get contradiction when you do that.

00:34:12: So if you do that, you cannot use an explosive logic like intuitionistic logic or classical logic.

00:34:18: You have to use a paraconsistent logic.

00:34:21: Which paraconsistent logic gives you a nice, smooth mathematical system?

00:34:26: That's still a matter that's being debated.

00:34:30: What is known is that certainly if for a number of paraconsistent logics, if you use the cave naive principle that every condition defines as set, the theory you get is non-trivial.

00:34:44: You cannot prove everything and that's provable, okay.

00:34:51: Of course, if you But some paraconsistent logics will give you triviality, independent of their inconsistency, because there's a paradox of self-reference called Curry's paradox.

00:35:05: And if you have certain principles about the conditional, then you're going to get triviality.

00:35:10: So we know that some paraconsistent logics will blow up even if you're using the naive, set-ready principle, some will not.

00:35:19: And then there's another very interesting question of if you want to recapture sort of standard results of sex theory about transphonic cardinals and orders and so on.

00:35:31: Are there para-consistent logics which are strong enough to do that without blowing up in your face?

00:35:35: And that was an open question for a long time.

00:35:38: But that question was answered affirmatively by Zach Weber maybe fifteen years ago now.

00:35:46: So there's a lot of research still going on in this area.

00:35:50: But the bottom line of your question is, yes, you can have a set theory which uses the naive assumption that every condition determines a set question.

00:36:02: What is the best underlying paraconsistent logic to give you a smooth theory of the infinite in these situations?

00:36:10: And we know quite a lot about that, but there are still a number of open questions.

00:36:18: May I ask, I mean, you talk about set theory, if you now come from type theory, so we have the same kind of paradox, right?

00:36:26: If you have a type of all types, you get an inconsistent type theory.

00:36:35: I mean, are these ideas of power consistency applicable in this context?

00:36:42: Look, I don't know, because I never studied them very carefully.

00:36:47: Clearly, if you are seriously operating with an inconsistent system, and it's not just this kind of to make life easy for yourself, you can't be using an intuitionist logic.

00:37:00: Could you do this with a para-consistent logic?

00:37:04: In principle, yes, in practice, I don't know the result.

00:37:09: So that is no para-consistent type theory, are you saying?

00:37:15: As far as I know, there isn't an a well-articulated, paraconsistent type theory.

00:37:21: Any more than there's a well-articulated, paraconsistent category theory where something similar happens.

00:37:28: because you can have a category of all categories.

00:37:31: And category theorists tend to reason about the category of all categories.

00:37:35: But I think when they do so, they do so in an informal way.

00:37:42: Informal in the sense of pre-formalized.

00:37:46: whether or not you can sort of nail down the formalization in category theory with the category or categories or type theory with the type of all types, that I don't know.

00:37:57: You've had to ask someone who's more familiar with the area than I am.

00:38:01: Sure, sure.

00:38:03: By the way, we have got in type theory another issue with category of all categories.

00:38:10: It is not to do with size.

00:38:14: When are two things equal?

00:38:15: When are two types equal?

00:38:16: That's quite a difficult notion.

00:38:19: So there is a category of, of all, yeah, the category of all categories is actually a higher category.

00:38:27: It's not an ordinary category.

00:38:29: So it's a bit of a different, it's a bit of a different emphasis.

00:38:32: It's, it's, I mean, when you talk about naive sets theory, the issue seems to be size, right?

00:38:39: This hierarchy of sets.

00:38:42: Well,

00:38:43: it is into a Milo-Frankl set theory.

00:38:45: In a nice set theory, size makes no difference because every condition, whatever defines a set, so size becomes irrelevant, but of course it's highly relevant to the Milo-Frankl set theory.

00:38:57: Yeah,

00:39:00: I mean, or size is... the issue which causes these paradoxes, I would say, I mean, or ignoring size, because once you say, if I quantify all sets, I get something which is a bigger set, a class or something, then the issue disappears.

00:39:19: So that's what I mean, these paradoxes, which you have to do with size.

00:39:27: That's one solution to the paradox of set theory, to say that very large set, very large totalities are not sets.

00:39:36: And that's the sort of solution that's implemented in Zameela Frankel's set theory.

00:39:40: But there are other set theories which work on different principles.

00:39:47: In type series, it's a similar solution, which is called universe, the universe of all types, or for small types, it's a larger type.

00:39:55: It's very similar.

00:39:57: I'm just pointing out that there is another issue which is totality.

00:40:01: It's like the category of all categories.

00:40:04: It's not a category.

00:40:05: And this is not just... So size is actually quite easy to address in a way by introducing this hierarchy.

00:40:11: But there is another issue is that the complexity of objects is increasing.

00:40:19: It may not have anything or may not be related to this... power consistent.

00:40:26: Right.

00:40:27: Right.

00:40:29: But may I ask one to start one last block because our potential next guest or hopefully our next guest might also say something about Hegel.

00:40:40: And that's why I wanted to invite you.

00:40:43: So you mentioned at the very beginning Hegel, you also mentioned Eastern philosophy, which would be also a very nice path to go, but for the connection to the next guest.

00:40:55: What's Hegel doing and all this?

00:40:58: Was he interested in formal logic or how to get him into

00:41:03: it?

00:41:03: Not in the modern sense, because there was no formal logic in the modern sense when he was around.

00:41:08: He was actually quite knowledgeable of the mathematics of his day.

00:41:12: And so in the logic, you find the discussion of various topics in the philosophy of mathematics of his day.

00:41:19: particularly infinity and infinitesimals and the calculus.

00:41:25: I mean, you find those things discussed.

00:41:28: But I mean, obviously it wasn't a philosophy of mathematics in any interesting sense.

00:41:31: Well, I mean, Hegel scholars might disagree, but that's my view.

00:41:35: All right.

00:41:37: But Hegel is certainly a dilithist.

00:41:40: He clearly endorses contradictions.

00:41:44: So for example, in the logic, when he's discussing motion.

00:41:49: He's concerned with what motion is and he says, look, what is it to be a motion?

00:41:57: Now, you might think that to be a motion is to be here at one point of time and here as another.

00:42:05: And he said, that's wrong.

00:42:08: That can be true even though the thing is stationary here at one time and here at another time.

00:42:16: He says, to be in motion is to be both here and not here, but at one and the same time.

00:42:23: That's unquote in German, of course.

00:42:26: So he says that motion realises contradictions.

00:42:31: An object in motion is both where it is and already somewhere else, maybe because it's gone a little bit further already, or maybe not quite got there yet.

00:42:41: So that Hegel is a dilithiist, I think is ungain sayable.

00:42:46: Another example in his discussion of the liar paradox in his lecture on the history of philosophy, when he talks about eubulities, he says the liar paradox is both true and false.

00:42:58: And if you only have one of these, then you only got half the story.

00:43:01: So that he's a dilithiist, I think is ungain sayable.

00:43:05: Now the much more interesting question is what role does contradiction play in his systematic philosophy.

00:43:14: And if you're talking about that, you're talking about the dialectic.

00:43:18: And it's clear the contradiction is integral to the dialectic.

00:43:22: Now, how?

00:43:23: that's another question, and that's a much more contentious question.

00:43:27: And let's, we will compare it to how Hegel can also be used in the foundation of mathematics next time.

00:43:35: Excellent.

00:43:35: Have you got talking on Hegel?

00:43:38: I mean, it's not confirmed yet, so we hope to get us Schreiber there.

00:43:44: And you also had some ideas how, I think his approach somehow comes from Hegel's idea of nothingness and how to start up things from zero.

00:43:55: And he has also formalized this in some model logic, but I'm no expert in it.

00:44:00: I will need to read the N-Lab, and that's always time consuming for

00:44:05: me.

00:44:07: Yeah, no, I mean, there are a number of people who have tried to formalize Hegel.

00:44:12: And I think this produces some very interesting ideas.

00:44:19: How good they are, I think is highly contentious.

00:44:23: I mean, it's also a hard topic, so to speak, because the audiences are so different, right?

00:44:28: Because I wouldn't think about a formal logician and a Hegel scholar at the same time.

00:44:33: Maybe I should, but I think the Friege scholar would be closer to logic.

00:44:38: Normally.

00:44:39: That's true.

00:44:40: Look, by far the best formal logician who is engaged in Hegel that I know is a German logician called Uwe Petersen, who used the techniques of substraturologic to articulate Hegel's ideas.

00:44:58: And Uwe is still working, I believe he's in Hamburg.

00:45:03: So if you want to talk about

00:45:07: formal

00:45:08: logic.

00:45:10: If you're interested in a good formal logician who knows his Hegel, then Uwe will be a terrific person.

00:45:17: Yeah, thanks for the pointers.

00:45:20: Okay, so if Thorsten, if you don't have a very pressing question.

00:45:25: Nope, I don't like

00:45:26: that.

00:45:26: And Graham, if you don't think that there's anything you need to say to qualify, I mean, we haven't talked about.

00:45:32: No, we've opened up many, many interesting issues.

00:45:34: And of course, there's a lot more to be said about all of them.

00:45:37: But time, especially for a parkhouse is very finite.

00:45:41: So, okay.

00:45:43: Yeah, then thank you very much for your time for these lovely insights and different ideas.

00:45:48: And I think pragmatically, you turned us a little more pluralistic simply for.

00:45:54: teasing so many interesting topics.

00:45:57: Okay, then have a great day and see you soon.

00:46:00: Okay.

00:46:01: Bye bye.