You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
James E Hanson (Jun 17 2024 at 13:38):@Benedikt Peterseim I never fully responded to your more philosophical question about structuralism.
I don't think I'm a mathematical Platonist, so I'm not sure I think there are a 'the' natural numbers. In particular I don't think that the von Neumann naturals are literally the natural numbers. Moreover, if I adopt the philosophical stance that mathematics is actually 'about real-world computation' (which, to me, seems relatively common among constructive type theorists), then I don't really see how to maintain the idea that there should be a unique natural numbers object. Real-world computation is fundamentally untyped and at a base level one always needs to choose an encoding of something like the natural numbers. One can clearly implement computational systems that attempt to get around this, such as cubical type theory, but this is clearly a high-level conceptual framework being imposed on real-world computation, as evidenced by the high computational complexity of things like Cubical Agda.
That said, I also don't think it's all that incoherent for a Platonist to literally identify the von Neumann ordinals with the ordinals the way set theorists often do. The von Neumann ordinals have exact structural parity with the ordinals; they don't have any extraneous coding structure the way things like coding the integers as pairs of natural do. As a corollary of this, I also don't think it's incoherent to literally identify the finite ordinals with the finite von Neumann ordinals. Obviously the finite ordinals are a natural numbers object, but depending on how one defines 'finite ordinal,' this is a very slightly non-trivial fact. There's clearly different intensionality between the definitions of the finite ordinal numbers and the finite cardinal numbers.
In any case, I also don't think book HoTT entirely succeeds at the structuralist philosophy. As far as I can tell, book HoTT doesn't have universe subtyping. This means that it suffers from the same 'hall of mirrors' effect that Russell originally identified as an unsatisfactory aspect of Principia Mathematica. Each type-theoretic universe has its own copy of the natural numbers, the Dedekind real numbers, etc. and are obviously 'morally' isomorphic as objects, but in the context of book HoTT saying that these two objects are 'equal' isn't even a meaningful statement.
James E Hanson (Jun 17 2024 at 13:50):Graham Manuell said:
I guess the distinction is that no one would be under the impression that synthetic geometry is good for all purposes, but that if someone advocates for something as a foundation for mathematics you believe that listeners will think it is capable of handling all the metamathematical issues you discuss above but this isn't (yet?) true. Is this an accurate description of your position or is there more to it?
Yes, I think this is a relatively accurate description of my position, although I also think there is a case to be made that certain kinds of metamathematics are always going to be easier to do with 'dumber' untyped systems like set theories.
James E Hanson (Jun 17 2024 at 14:06):@Graham Manuell But also, type theory still has its own kinds of junk theorems, so I can't really accept the implication that junk theorems 'do not exist' is type theory. There aren't as many of them, but there's things like needing to define division on the natural numbers so that (because type theory is bad at handling partial functions). Also, while set theory has more 'advanced' junk theorems like ' is a topology,' people often cite relatively simple ones like ' makes sense' (assuming we're coding reals as lower Dedekind cuts), but this kind of 'coding garbage' occurs in type theories in practice all the time too. If we coded (classical) reals as pairs where is a lower cut of type Nat -> Bool and is a proof that is a cut, then is a theorem, even though this is just as much junk as .
For an example of this in practice, I was trying to formalize some model theory in Coq, so I was looking at the library Autosubst. In this library, they literally identify their variable symbols with natural numbers:
(** A type synonym for natural numbers used as de Bruijn indices *)
Definition var := nat.
This means that it's meaningful to take the factorial of a variable or ask whether a variable is a prime in the context of this library, for instance. Is this actually a problem? No of course not. Moreover, I'm sure that the developers of Autosubst chose to do this to avoid needing to obnoxiously cast naturals to variables all the time. But I feel like this speaks to a broader point which is that a certain amount of junk behavior in a system is sometimes not really a problem and trying to eradicate it entirely isn't even necessarily practical.
James E Hanson (Jun 17 2024 at 15:12):@Mike Shulman
In some cases, simply by rephrasing some definitions, a theorem can be made constructive and its proof more elegant.
This is neither here nor there, but given my current experience with constructive math, I find this sentence hilarious. The phrase 'In some cases' and the word 'simply' are doing an incredible amount of work here. As a bit of probably unwanted advice, I'd say that if you really want to convince mainstream mathematicians that they should be interested in HoTT, you should probably deemphasize constructivity. I've met people who like higher category theory but who aren't interested in HoTT because they're under the impression that it's necessarily constructive. And while the HoTT book itself emphasizes that constructivity isn't obligatory, I've also met HoTT people online who insist on statements like 'univalence is incompatible with LEM,' which while true under some readings (specifically interpreting 'LEM' as type-level LEM) is also really misleading (since type-level LEM already implies global choice without univalence, and this is really not what most people mean by 'LEM').
and in (iv) the difference is that the HIIT construction does not require first constructing the Dedekind reals, and in particular also works predicatively.
The problem I still have with this is that the Cauchy real construction in the book isn't really using the full power of higher inductive types. It's just a quotient inductive type. Quotient inductive types are compatible with set theory, and moreover it seems reasonable to me that something like CZF + "quotient inductive types exist" would be predicative.
Similarly, a friend of mine pointed out to me that CZF with the regular extension axiom can probably also construct the HoTT Cauchy reals. I think some people might not consider REA predicative, but CZF + REA is still a really weak theory as far as these things go.
Rathjen and Lubarsky's paper on the regular extension axiom came out in 2003, about ten years before the HoTT book. Did any of the authors of the HoTT book talk to any constructive/predicative set theorists (like Rathjen or Lubarsky) about whether this construction could be done in previously studied constructive set theories (since you said this section is about constructivity, not about predicativity)? Or did the person that wrote this just assume that it couldn't be done the same way someone seemingly just assumed that there's no such thing as a predicative set theory with a proof-theoretic consistency proof?
it says that set-theoretic axioms can be chosen arbitrarily.
No they can't. They still need to be consistent. This is a less restrictive requirement than having computational content, but it's still a meaningful restriction.
Obviously one can write down some axioms that seem to be semantically sensible and hope they're relatively consistent to some standard theory without actually knowing so, but is this really that much more fundamentally arbitrary than writing down something like the univalence axiom and hoping that it can be given a computational interpretation at some later time?
This is why I still feel pretty comfortable saying that the book's statement here is wrong and obnoxiously phrased.
And the computational behavior of type theory (sans axioms) is necessary for practical implementations of it,
Doesn't this depend to some extent on what you mean by 'practical implementation'? Lean with Mathlib and Isabelle/HOL both fail to be constructive and yet are fairly practical proof assistants built on type theory.
in contrast to implementations of set theory where I would expect it suffices to have a "computational" interpretation of the underlying first-order logic.
I don't think this is an accurate description at all of what computational content in constructive set theories means. You need to know that the axioms are in some sense computationally realizable. This depends on the semantics of the axioms in a strong way and doesn't just come from some computational interpretation of intuitionistic first-order logic.
Mike Shulman (Jun 17 2024 at 17:06):James E Hanson said:
And while the HoTT book itself emphasizes that constructivity isn't obligatory, I've also met HoTT people online who insist on statements like 'univalence is incompatible with LEM,'
I've been fighting against that for at least a decade now, starting with the book. If you have any suggestions about how to more effectively stop people from saying that, I'd love to hear them.
The problem I still have with this is that the Cauchy real construction in the book isn't really using the full power of higher inductive types. It's just a quotient inductive type.
It's not supposed to be an application of higher-homotopy inductive types. In fact it's just the opposite, an illustration that the idea of higher inductive types is useful even at set-level. And yes, you can construct equivalent objects in many set theories, but that doesn't mean the idea of higher inductive types isn't useful, just as the idea of ordinary inductive types is useful even though you can construct them in set theories.
Obviously one can write down some axioms that seem to be semantically sensible and hope they're relatively consistent to some standard theory without actually knowing so, but is this really that much more fundamentally arbitrary than writing down something like the univalence axiom and hoping that it can be given a computational interpretation at some later time?
Yes, I think it is. The difference is not in the state of "we hope/expect X but are not sure about it yet" but in the difference between the notion of consistency and the notion of computability.
And the computational behavior of type theory (sans axioms) is necessary for practical implementations of it,
Doesn't this depend to some extent on what you mean by 'practical implementation'? Lean with Mathlib and Isabelle/HOL both fail to be constructive and yet are fairly practical proof assistants built on type theory.
Yes, that's why I said "sans axioms". My understanding is that these proof assistants are built on a type-theoretic core that is constructive and hence implementable, with classical properties added on top as axioms.
in contrast to implementations of set theory where I would expect it suffices to have a "computational" interpretation of the underlying first-order logic.
I don't think this is an accurate description at all of what computational content in constructive set theories means.
It wasn't intended to be. It was intended as a description of the amount of computation needed in to be able to implement a set theory (even a classical one).
James E Hanson (Jun 17 2024 at 17:53):Mike Shulman said:
I've been fighting against that for at least a decade now, starting with the book. If you have any suggestions about how to more effectively stop people from saying that, I'd love to hear them.
I think that one thing that is a confounding factor here is that people still talk about 'propositions-as-types' often when trying to introduce the idea of type theory even though strictly speaking type theories with Prop aren't using propositions-as-types. I don't know if this is really a way of addressing the issue though, because propositions-as-types is a good way to introduce the mindset with which type theory approaches logic (i.e., tighter intermingling of 'logic' and 'stuff').
It's not supposed to be an application of higher-homotopy inductive types. In fact it's just the opposite, an illustration that the idea of higher inductive types is useful even at set-level. And yes, you can construct equivalent objects in many set theories, but that doesn't mean the idea of higher inductive types isn't useful, just as the idea of ordinary inductive types is useful even though you can construct them in set theories.
My point is that the list reads like a list of (in the context of constructive math) HoTT can do this, set theory can't. (ii) for instance is saying that a certain fact about categories can't be implemented constructively in set theory. And look at (iv):
In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved. But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles; see Chapter 11.
How is this not saying 'set theory needs non-constructive principles to do the Cauchy reals well, but HoTT doesn't'? Note the word 'requires.'
Yes, I think it is. The difference is not in the state of "we hope/expect X but are not sure about it yet" but in the difference between the notion of consistency and the notion of computability.
My point is that saying something can be done 'arbitrarily' is pretty strong. I don't think it's really an accurate description of the process of trying to dream up a set theory in practice, and I don't think that process is that different from trying to write down a semantically motivated but also computational type theory, like book HoTT.
Yes, that's why I said "sans axioms". My understanding is that these proof assistants are built on a type-theoretic core that is constructive and hence implementable, with classical properties added on top as axioms.
Honestly I have the most experience with Isabelle/HOL at this point, and I don't know how much of the computational content of the ambient constructive type theory really comes through to the end user. It seems like most of the handling of stuff like purely computational equality is done by high-level tactics like auto and simp and by the ATPs integrated via Sledgehammer. We would need someone more familiar with the bowels of Isabelle/HOL to be sure about this, but part of my evidence is that libraries written by the devs themselves, like HOL-Algebra, use Hilbert choice operators pretty freely in basic definitions (such as the inverse function in a group), and choice operators in Isabelle/HOL explicitly don't have computational rules. Another piece of evidence is just that the ATPs Sledgehammer calls are all purely classical and are mostly based on stuff like superposition calculus, which can only prove things by contradiction.
In general this is something that I don't find convincing in the rhetoric of some type theorists (the idea that the computational content of constructive type theory is necessary for a practical proof assistant). I think that a proof assistant built on purely classical logic with good tactics and ATP integration could probably be about as usable as something like Coq or Lean. The problem in my mind is that developing good tactics is the kind of thing that cost the kind of money that a lot of people who might try to build alternative proof assistants don't have.
It wasn't intended to be. It was intended as a description of the amount of computation needed in to be able to implement a set theory (even a classical one).
Ah, I was misunderstanding then.
Mike Shulman (Jun 17 2024 at 18:21):James E Hanson said:
My point is that the list reads like a list of (in the context of constructive math) HoTT can do this, set theory can't.
Right, that's the point of the list. I've already agreed with you that there are issues with (iii) and (iv) that needs to be fixed and are being discussed at the github issues. But the point of (iii) and (iv) is that there are advantages in purely set-level math, so it doesn't matter that they aren't using higher-dimensional types, which is what it sounded to me like you were complaining about.
My point is that saying something can be done 'arbitrarily' is pretty strong. I don't think it's really an accurate description of the process of trying to dream up a set theory in practice, and I don't think that process is that different from trying to write down a semantically motivated but also computational type theory, like book HoTT.
Having spent a good deal of the last few years of my life trying to write down a semantically motivated but also computational type theory (H.O.T.T.), and also having written a paper exploring a wide array of variations of axioms for constructive set theories, I am confident in asserting that the process is very different. How about replacing the word "arbitrarily" by something like "with much greater freedom"?
Honestly I have the most experience with Isabelle/HOL at this point, and I don't know how much of the computational content of the ambient constructive type theory really comes through to the end user.
I was not claiming that any of it comes through to the end user, or even to the authors of libraries and sledgehammer tactics. I'm talking about the absolute core of the implementation.
Mike Shulman (Jun 17 2024 at 18:35):Regarding the last point, note also that Isabelle/HOL is a simple type theory, and the argument about the need for constructivity in implementation is mostly about dependent type theories, since those are the ones where you need conversion-checking as part of type-checking. So it doesn't really matter what Isabelle/HOL can or can't do for my point.
James E Hanson (Jun 17 2024 at 20:47):@Mike Shulman
How about replacing the word "arbitrarily" by something like "with much greater freedom"?
I would be happier with that, yes.
I will admit that I have phrased some of my criticism in an overly harsh way. I shouldn't have used the term 'bad faith' for instance. But I do think that even the issues you posted to the HoTT book GitHub page as a result of this argument highlight a lack of academic due diligence when it comes to some of the offhand remarks about set theory in the book. Nearly one single page (the end of page 13 together with page 14 of hott-ebook-13-g2e736d1.pdf) of the introduction contains several errors.
Returning to what you said here for a moment.
These four numbered points are not "comparing HoTT to set theory" in a general way. They are in the section of the introduction about constructivity, and are introduced with the following paragraph:
[...]
In other words, the sole purpose of these numbered points is to argue that constructive HoTT is easier, or more elegant, than constructive set theory, for a mathematician coming from a classical background.
I don't buy this as precise explanation of what that section is doing rhetorically; I don't think that's what it's 'solely' doing. The 'circumlocutions' quote in (iii) only really makes sense in the context of classical set theory given that it explicitly talks about cardinality. Both initial cardinals and Scott cardinals don't even work in IZF. (Likewise, when I challenged you on this particular point earlier, you insisted on talking about cardinals rather than ordinals, since cardinals are clearly handled in a more inelegant way in set theory.) This means that in point (iii) at least, the comparison is really more correctly seen as between classical set theory and constructive type theory, not between constructive set theory and constructive type theory. The HoTT book could have made the point here that constructive set theory doesn't seem to be even able to define canonical representatives of cardinalities at all—no locution at all is certainly worse than circumlocution—but it didn't. With no comment about the status of cardinals in constructive set theory from the book, how are we to know that we cannot, 'simply by rephrasing some definitions,' perhaps find a far more elegant description of cardinals in constructive set theory?
This makes we wonder again about my direct question from earlier, which you did not address:
Did any of the authors of the HoTT book talk to any constructive/predicative set theorists (like Rathjen or Lubarsky) about whether this construction could be done in previously studied constructive set theories (since you said this section is about constructivity, not about predicativity)?
Moving on, I think that point (iv) and the comment about consistency strength are not only both incorrect, but are also somewhat mutually incompatible. IZF can prove the existence of free Cauchy sequence completions of metric spaces and IZF with collection (and therefore of course ZFC) can actually implement the HoTT definition somewhat directly without explicitly relying on embedding into the Cauchy filter completion of the space (although it does not result in a uniquely defined set). In IZF with a designated inaccessible set (satisfying second-order collection), the construction can be done directly and canonically. (I think you would find the second construction ugly to be sure, but the current wording in the book makes it sound like such a feat is literally impossible.) As you pointed out, these seemingly require impredicativity and IZF with collection and/or univereses are pretty strong constructive set theories, so if we require predicativity then yes the idea of higher inductive types yields something new in this context (and that is a valuable insight), but the comment about consistency strength only makes sense if we assume that all set theories are too strong to be predicative.
So, yes, I do feel comfortable saying that this quote
Moreover, in univalent foundations this seems to happen more often. For instance:
[...]
(iv) In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved. But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles; see Chapter 11.
is disingenuous in effect. The phrase 'version of this definition' is vague. It does not make it clear at all that it is actually an inequivalent definition which, moreover, also works in some constructive set theories (drastically contrasting the implication of the previous sentence, which is that in set theory one "requires" LEM or countable choice to make a Cauchy sequence definition of the reals work well). There's nothing uniquely set-theoretic about the naive definition of Cauchy reals (after all, it's fairly trivial to write down in HoTT), and there's nothing fundamentally univalent about the free completion definition, especially if the regime of set theories in which this distinction starts to matter most (weak, predicative theories) is implicitly excluded by a comment later on in the same page anyway.
Mike Shulman (Jun 17 2024 at 23:38):Insofar as the phrasing of point (iii) applies only to classical set theory, that means it is badly written and should be improved. The intent of that section of the introduction is to talk about constructivity. The reason for mentioning that cardinals as initial ordinals uses AC was to make the point that that definition is unavailable constructively.
Are you sure there isn't a constructive version of Scott's trick? Of course you can't take the least such that , but can't you do something like define the ordinal rank of any set by well-founded induction (assuming a constructive axiom of foundation) and use ?
Mike Shulman (Jun 17 2024 at 23:48):Thanks for the apology about bad faith (at least I hope I may construe that as an apology). Please keep in mind that the HoTT Book was written by a lot of people over a very short span of time; I think it's amazing that it's as consistent and readable as it is. After the initial release we've improved it in many ways, and we try to continue to be open to further improvements. The more you can phrase your comments as suggestions for improvement rather than attacks on the community, the less defensive we will feel and the easier it will be to come to an agreement about how to improve it.
Mike Shulman (Jun 18 2024 at 00:01):I can apologize on behalf of myself, at least, for unintentionally causing offense, and I doubt if it was intentional on the part of any of the other authors either. I don't think there's anything wrong with talking about the benefits of a new theory, but we can and should strive to do it as correctly and politely as possible.
Mike Shulman (Jun 18 2024 at 00:04):I'm also sorry that I missed one of your questions from earlier. I don't know who the other authors may or may not have talked to or when. As you probably know, Peter Aczel was one of the authors.
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 01:05):<
James E Hanson said:
strictly speaking type theories with
Proparen't using propositions-as-types
To expand on this point a bit, propositions-as-types is a philosophical paradigm, a matter of outlook: one who regards all types as propositions (and all propositions as types) is doing propositions-as-types.
As the nLab notes, not all type theories fit with this outlook. Yet, MLTT, HoTT, and CuTT are all among those that do, and the presence of Prop does not alter this fact. For a follows propositions-as-types adherent, Prop would _merely_ be an quirky terminological choice used by the community for those propositions in particular that imply their own contractibility.
It's true that looking through the lens of propositions-as-types, the statement "univalence is incompatible with LEM" would make perfect sense, as it reflects the belief that LEM equates to ∏ P:Type.P∨¬P, which implies uniqueness of identity proofs.
However, I doubt there's much (or any) overlap between those deeply invested in propositions-as-types and those online HoTT enthusiasts who argue that univalence is incompatible with LEM.
Mike Shulman (Jun 18 2024 at 01:15):I don't think one can say that any particular formal system adopts a particular philosophical paradigm. In particular, I think many practitioners of HoTT would not regard all types as propositions; only those types that lie in (h)Prop.
Can anyone point to some examples of these "online HoTT enthusiasts" who claim univalence is incompatible with LEM?
Mike Shulman (Jun 18 2024 at 01:15):Maybe that was your point too?
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 01:18):I have a quick administrative query. The conversation seems to have evolved into three separate discussions.
Question A: Could we consider dividing these topics into separate threads now? The discussion about Leinster’s course has clearly outgrown its initial focus. Splitting off the second topic would allow easier access to the interesting points raised there on the social aspects, e.g. by @James E Hanson and @Chris Grossack (they/them), which should be of wider general interest than the technical aspects being discussed now.
Question B: If we agree that splitting this up is a good idea, sorting the posts might still put an overwhelming amount of work on the moderators. Is there a way for others watching the discussion to contribute?
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 01:23):Mike Shulman said:
Maybe that was your point too?
Yes, I think we're largely making the same point here.
To summarize: Propositions-as-types is a user's outlook, not a formal system's technical property. HoTT is compatible with practitioners using propositions-as-types, but most practitioners do not subscribe to propositions-as-types. I don't think the online claims of "univalence is incompatible with LEM" come from the very few HoTT users who do.
(Instead, it might be coming from people who are not all that familiar with HoTT in the first place, or are confused. That's harder to stop than asking for the propositions-as-types enthusiasts to put up a disclaimer. But maybe somebody could write a quotable blog post / FAQ that could be linked whenever "univalence is incompatible with LEM" comes up online?)
Mike Shulman (Jun 18 2024 at 01:27):https://ncatlab.org/nlab/show/homotopy+type+theory+FAQ#IsHoTTLimitedToConstructiveMathematics ?
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 01:53):Mike Shulman said:
https://ncatlab.org/nlab/show/homotopy+type+theory+FAQ#IsHoTTLimitedToConstructiveMathematics ?
Yeah, in particular Andrej Bauer's linked post is fairly close to what I had in mind.
Mike Shulman (Jun 18 2024 at 02:31):It's curious to me to hear that there are still people who are confused about this. I'd like to know where they got that impression. Could chapter 3 of the HoTT Book be written to make this point more clearly?
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 03:23):I think it's the end result of a game of telephone, and the only feasible way to address it is to monitor the forums/venues where such statements are likely to be made, and offer immediate correction/explanation with helpful URLs.
As an added difficulty, some of them are venues that are uncomfortable to monitor for many experts, such as subreddits or various nontypetheory math mailing lists. It's easy to underestimate the reach of such venues in propagating half-truths ("surely a practicing topologist won't take a statement found on /r/math at face value, right?" They will, they won't read a textbook to doublecheck, they will repeat it, and they won't remember that it originally came from /r/math, and when an opportunity comes around to learn about HoTT, they'll dismiss it.)
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 03:36):Full disclosure: controversially, IMHO the really right approach would have been the IAS year participants coming up with terminology that's more compatible with the existing literature, but that ship has sailed.
The whole confusion started because initially, LEM/choice/etc. meant one thing to most people in the know, but eventually LEM/choice/etc. came to predominantly refer to some other thing.
Mike Shulman (Jun 18 2024 at 03:44):Which meanings are you referring to by your two things?
Mike Shulman (Jun 18 2024 at 03:44):The meanings of LEM/choice advocated by the HoTT book coincide with those used by all non-type-theorist mathematicians. That seems to me like clearly the right choice in the long run.
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 03:49):Sorry, by "really right" I didn't intend to mean "in the long run, this would have been better for general well-being of mathematicians", but "the right way to avoid this particular specific problem".
The right call in the long term might inded be to cause this particular problem to avoid other, bigger problems down the road.
Mike Shulman (Jun 18 2024 at 03:49):Indeed.
Mike Shulman (Jun 18 2024 at 03:50):Wouldn't it be even worse if it were true that univalence was inconsistent with "LEM"?
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 03:57):I am definitely not the right person to answer that question ;)
Tongue firmly in cheek, and purely for context: To me, the IAS year was akin to one where all Hungarian-speakers started speaking "English with a Hungarian accent" instead. Sure, it'd have been more confusing to keep 'a' as the definite article like in Hungarian. But it might have been better not to start speaking English in the first place ;)
Mike Shulman (Jun 18 2024 at 03:58):Do you mean that you were used to "LEM" meaning the one that's incompatible with univalence?
dusko (Jun 18 2024 at 03:58):i just scanned this amazing conversation. i don't have anything of substance to contribute to the content (though lawvere would come out swinging that propositions-as-types wasn't about propositions and types but about the structure of logical operations and the logical meaning of structure...) --- BUT i have a historic comment. (it will probably fall flat, and the effect will be as if i didn't say anything. nothing to lose :)
i think that this thing that when someone says that your favorite theory is nonsense, that you feel personally insulted --- that is a recent development. science wasn't always like that. category theory was called nonsense, in full sincerity, by the best friends of the founders of category theory and no friendships were broken. einstein and bohr rubbished each other's worlds but never took personal offense. naphta and settembrini in Zauberberg unleashed at each other the entire forthcoming war without any injury to the mutual respect.
there were two people at one of my early departments who saw model theory quite differently. so they would stand at a blackboard in the common room all morning yelling at each other, one of them cursing in Hungarian. at lunchtime, someone would walk up to them and say lets go for lunch, and they would let go of each other's virtual neck and walk down to the food court with everyone. if you would make a joke how they might kill each other they would smile at each other. then we would all eat lunch together, and they would talk with about departmental affairs. then they would remember what they were talking about on the blackboard, walk back to it, and within half an hour someone would be yelling again.
i am not saying that everyone should work like that. but we should be able to say that topology is pointless or that proof theory is bureaucracy, simply and freely, with no fear of insulting anyone personally. it was all done, mostly in good humor, and much more, through the 90s, with no harm that i can think of. maybe i was blind. in any case, i only recently noticed that it changed...
feynman explained how in science we can only know for sure when we are wrong. in the meantime, we pursue theories that seem right but eventually they all turn out to be wrongheaded in one way or another. otherwise, there would be a point when the true theories have been achieved and all you can do is teach. no more research. the theories that do claim to be true forever are a.k.a. religions. so both set theory and type theory will hopefully turn out to be rubbish with respect to some big new problem some day. awaiting the next coming of such a day, we should be allowed to say that particular theories are rubbish without insulting any particular theorists, or their students. and we should not take it personally if the theories are not yet rubbish and we are wrong.
while communities should be spaces of comfort and respect, sciences are spaces of uncertainty and doubt. it would be good to draw a clear demarcation line and avoid imposing the requirements of one on the other.
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 04:20):Mike Shulman said:
Do you mean that you were used to "LEM" meaning the one that's incompatible with univalence?
No, I mean only that when terminology drifted. it resulted in confusion. When onlookers are confused, the best way to deal with it is to acknowledge that the drift happened, explaining to the onlookers that HoTT allows them to do their mathematics classically the way they're used to, and make resources at various levels explaining this, so the appropriate one can be linked quickly whenever confusion rears its head.
Alas, one has to be persistent, because old statements will circulate in the community, and the venues that working type theorists don't frequent actually reach lots of mathematicians, so the confusion will perpetuate itself for a long time.
This is all why I expect that rewriting the HoTT book won't help with this particular state of affairs (to the extent that it's still an issue: I'm not sure!) and think that only "more activism" could.
Zoltan A. Kocsis (Z.A.K.) (Jun 18 2024 at 04:27):dusko said:
i just scanned this amazing conversation.
That's a heartwarming story, thanks for sharing it! I myself hope these debates to resemble, if anything, the debate of the pot and kettle in the Rumjacks song.
The field of Foundations does see more high risk debates, with means of living and more on the line, though. Although I pushed back on the opinion that this particular debate has any effect like that upthread, we do have existence proofs of such debates (just think of the age of Brouwer-Hilbert), and it's good to reassure each other that we all try our best not to let our opinions provide munition, even against our wishes, for someone's ideological crusade or personal vendetta! Even if ultimately only the crusaders and mobsters are at fault.
Notification Bot (Jun 18 2024 at 08:15):310 messages were moved here from #theory: category theory > Tom Leinster on set theory by Morgan Rogers (he/him).
Morgan Rogers (he/him) (Jun 18 2024 at 08:17):I'm just now catching up with this discussion.
This has not really been about Tom Leinster's ETCS course for a while, so I split the topic (as @Zoltan A. Kocsis (Z.A.K.) suggested; I left the rest as is, since it has primarily been a discussion between @James E Hanson and others).
Thanks to @Chris Grossack (they/them) for their humanizing comments earlier, I fully agree that the human angle was being neglected up to that point.
fosco (Jun 18 2024 at 10:48):dusko said:
i just scanned this amazing conversation. i don't have anything of substance to contribute to the content (though lawvere would come out swinging that propositions-as-types wasn't about propositions and types but about the structure of logical operations and the logical meaning of structure...) --- BUT i have a historic comment. (it will probably fall flat, and the effect will be as if i didn't say anything. nothing to lose :smile:
I also curse in Hungarian at my friends, when we have a mathematical disagreement. Afaics we remain friends.
Kevin Carlson (Jun 18 2024 at 17:31):dusko said:
while communities should be spaces of comfort and respect, sciences are spaces of uncertainty and doubt. it would be good to draw a clear demarcation line and avoid imposing the requirements of one on the other.
This is an important perspective, but surely you haven’t failed to notice the difficulty of getting jobs for set theorists, category theorists, and type theorists? It was all well and good for Mac Lane to argue with whoever about whether category theory was worthless, having invented it as a rather senior mathematician! The Duskonian attitude only really works if you assume that the arc of academic hiring inevitably bends toward truth (ideally on the timespan of a single career), whereas I think I’m probably not alone on this server in perceiving that category theorists have actually been unfairly underhired, especially in the land of category theory’s birth, for the whole life of the subject, and at least partly as a result of all the constant negative muttering about abstract nonsense. The fact that category theory is now providing a fair number of jobs at private institutes and startups is, if anything, just proof that academic hiring committees have been opposed to category theory for political reasons more than intellectual ones, for generations. I imagine James is feeling similar things when people are excessively negative about set theory.
Zoltan A. Kocsis (Z.A.K.) (Jun 19 2024 at 03:01):@Kevin Carlson:
I pushed back when @James E Hanson implied that negativity about set theory among practitioners of foundations contributes significantly to the difficulties set theorists face on the academic job market, and it's only right that I shall maintain the same stance regarding category theorists too.
As I wrote above, most departments prefer candidates with expertise in core areas like algebra, combinatorics, differential equations, geometry, or number theory, which impacts hiring decisions 1000x more than any academic namecalling between niche fields ever could. Over the last three decades or more, Foundations research in general has not been popular among experts in these key areas, and trying to attributing this to disputes within the foundation fields seems dubious at best.
After all, a few foundational fields have successfully countered this unfavorable view, and they could only do so by doing things that the core areas found immediately valuable. E.g. the classical model theorists settled relative Mordell-Lang, provided explicit bounds on the density of rational points on transcendental curves, proved a bunch of new graph regularity lemmas, etc. They provided tools that the practitioners of the core fields could and did use frequently: and indeed, combinatorialists and number theorists now hire classical model theorists with some frequency, and care little whether other logicians namecall them or not. Pure category theory has not (maybe could not) make a concentrated effort like that. This does not decrease the worth of category theory and category theorists: I don't think a field's worth should be measured by how many number theory conjectures it settles! But it does explain the hiring gap adequately.
I don't think any department every hired based on "diversity of fields" principle. Quite the opposite. Sure, if a department suddenly lacks expertise in a core area (like having no analysis experts at all), they might hire to fill that void, but usually, they prefer candidates who are already known collaborators, or are expected to become collaborators very quickly. If nobody in a department ever has use for results from Hodge Theory, they won't hire a Hodge Theorist, because there will always be other applicants who fit the department better and could be immediate collaborators, coauthors on grants, etc. This is true even though Hodge Theory is highly regarded among pure mathematicians and is not associated with any negative stereotypes.
It seems improbable that a department dominated by, idk, stable homotopy theorists would dismiss hiring a category theorist because they consider categories abstract nonsense. However, "this particular category theorist doesn't do the kind of category theory that helps with our work stable homotopy theory" is much more likely to come up, and one has to admit, is a perfectly valid observation, and not a "political reason".
In the end, they'll probably hire a candidate some people in the department already know in some respect. This pattern holds across all fields: familiar candidates are favored over outsiders, unless filling a very glaring gap is necessary. And for better or worse, most departments are dominated by people from the core areas, who do not use category theory, or any kind of foundations research. By itself, this does not even imply bias; after all, they same people are often eager to jump on new tools if they think it'd help with their work. But even if there is bias, it's certainly not caused by academic conflicts within foundations.
There could be evidence that would change my mind -- it would involve examples of math departments that are dominated by foundations, but for mysterious reasons refuse to hire from certain areas. In those situations, intra-foundations conflict would look like the most plausible culprit. E.g. if Leeds had no category theorists at all, I'd certainly be alarmed. But that's not what I see: despite all conflicts, reverse mathematicians, proof theorists, category theorists, set theorists, model theorists seem to all flock together whenever the opportunity to do so arises.
Moreover, while category theory has found applications in the private sector, this also doesn't show that there was bias against it in academia.
One could compare with automata theorists. It was not easy and is still not easy to get a job as an automata theorist in a CS department (it's impossible to get one in a math department).
But Amazon hired automata theorists in large numbers in Cambridge. Alexa's ability to understand human speech, a decade before LLMs, was largely a result of their work. It's a remarkable achievement. Is this evidence that automata theorists were underhired?
Absolutely not. The research that contributed to Alexa
a.) required the scientists to command a very large number of subordinate research engineers to make this a reality; far larger than any academic department would be willing or able to hire (and even if they were willing, research engineers like to work for research engineer salaries, way above academic pay tables).
b.) had enormous impact, but produced very little content suitable for academic publication, far less than targeted foundational research would (and at far higher cost!). Alexandra Silva's academic output alone far exceeds anything that came out of Amazon's large team.
c.) was not feasible within an academic setting. Even if Amazon had the inclination to fund the same researchers while they still worked in academia, the resources required to do this far exceed anything managable via Standard Innovation Vouchers or other industry grants/gifts. And that's before noting that academic overheads are massive (50+%!) and these positions do not allow researchers to focus solely on research due to other academic duties like administration, occasional teaching, and supervision.
All in all, this sort of application is not right for academic settings, and it would be very difficult to argue that computer science departments significantly missed out by not hiring more automata theorists, especially compared to possibly hiring fewer experts in fields like security, databases, or programming languages.
The ambitious industrial applications of category theory also require substantial investment (in a recent high profile case $30mil+), large teams of engineers, and will yield limited academic publications over an extended period. So while category theory has found applications in industry, I don't find this convincing evidence that math academia is somehow biased against it.
(I'm coming from a place of experience w.r.t. industrial research: the work we did at CSIRO for Hensoldt and Boeing was more impactful than my academic work. But it also yielded a grand total of 0 publications. Even if I could have found a university that tolerated me producing no publications for 3 years while also not doing any teaching or admin whatsoever, they would not tolerate me also hiring a research assistant and a bunch of students to help me, who also produce no publications in the same time period)
Kevin Carlson (Jun 19 2024 at 06:06):Thanks, @Zoltan A. Kocsis (Z.A.K.). To be clear, I didn't mean at all that intra-foundations arguments have led to low academic hiring of category theorists. I mean instead to point to an attitude of mathematicians in the "core" fields looking down on the area. So, this might be off topic and I'll try to constrain myself to one more reply.
Anyway, it's impossible to definitively settle this kind of question, but I remain quite convinced that the fact that category theory has had a continuous advance in its involvement in and relevance to, first, such prototypically core fields as algebraic geometry and topology, and later to nearly every part of pure math, and more recently to applied fields, all the while with the overwhelming majority of departments not so much as offering a course in the field, let alone employing a specialist, is substantially a result of bias. One of the most important books of the century so far for topology is literally called Higher Topos Theory, but it was written by someone who was not trained by category theorists, does not describe himself as a category theorist, and is not conceptualized by the community as a category theorist; the most famous mathematician of my generation is engaged in a program of finally invading analytic geometry with category theory; of the leading category theorists in the US, I can think of exactly one who is tenured at a math department of an R1 university (though I have no reason to believe Mike couldn't get such a job if he wanted to.) At the Topos Institute we've thus far been able to support ourselves doing work that continuously produces public academic outputs with no mass employment of engineers whatsoever, entirely on grant money, making us an example I think is pretty much unique among mathematical research institutes using tools traditionally identified with pure math. There is no bound to the amount of evidence one can prefer to explain away, but I would be completely at a loss to name another field of math with such a combination of usefulness to other fields both pure and applied and an almost absolute lack of hiring into the most traditionally desirable postiions.
Zoltan A. Kocsis (Z.A.K.) (Jun 19 2024 at 07:19):Kevin Carlson said:
So, this might be off topic and I'll try to constrain myself to one more reply.
Indeed, this then might be a different conversation than I thought I was having ;) My ultimate interest is whether intra-foundations debates influence hiring of people working in foundations (and therefore we should tone them down or stop having them) or not. It seems to me that they do not, and my previous long comment is meant to explain why I believe that.
You raise a very interesting point below regarding on the impact of category theory vs. the amount of category theory positions. I'll try to respond briefly to that, but then I'll rest too.
At the Topos Institute we've thus far been able to support ourselves doing work that continuously produces public academic outputs with no mass employment of engineers whatsoever, entirely on grant money, making us an example I think is pretty much unique among mathematical research institutes using tools traditionally identified with pure math.
First of all, I think the Topos Institute is absolutely amazing! Indeed I use some of the software maintained by Evan et al. there, and follow the tons of great logic research coming out of there. I think all of it is certainly R1 department quality or above! However, I don't think much or any of it concerns the topics associated with R1 departments.
And landing a job in an R1 department, or any academic department for that matter, depends on previous collaboration with people from those departments on their specific research topics. This approach seems entirely appropriate and unbiased to me, even if it means that departments' topics change extremely slowly, and thus the fields represented at R1 institutions change very slowly.
You write:
There is no bound to the amount of evidence one can prefer to explain away, but I would be completely at a loss to name another field of math with such a combination of usefulness to other fields both pure and applied and an almost absolute lack of hiring into the most traditionally desirable postiions.
Does a self-styled category theorist who made significant contributions to derived algebraic geometry really have a harder time getting hired than a self-styled homotopy theorist with the same contribution? While open to persuasion (perhaps in another thread?), I harbor very serious doubts. By all means, call me out if I dismiss or explain away evidence for this, but I don't remember encountering any evidence that needed to be explained!
The impact of category theory on pure mathematics is clear. And departments or institutes shouldn't recruit from different fields (no matter how adjacent) when they have a lineup of familiar collaborators to recruit. The category theorists who impacted the relevant fields are presumably among those familiar collaborators, and are therefore part of the same hiring pipeline. Category theorist or not, Lurie himself certainly was, and his early, brief stint in logic did not seem to disadvantage him. The right way to change this seems to be by make contributions to R1 deparment topics, getting people into R1 departments, then once they have tenure and can branch out, they can invite the rest of the category theorists in (again, seems to have worked for model theorists). Even better is to make alternative "most desirable positions" and I think category theorists are doing amazing work on that at the moment!
I 100% think that R1 departments should have more category theorists. And more set theorists for that matter. I just don't think the current state arose because of bias against category theory (and certainly not bias that could have been averted if we had fewer intra-foundations conflicts, which was the original point I wanted to make).
Kevin Carlson (Jun 19 2024 at 07:26):I suppose the alternative narrative is something like, after the founders of category theory were intimately involved with cutting-edge homological algebra etc, their students became more inward-facing and stopped collaborating as usefully with other mathematicians, and thus naturally less of them found good positions outside of self-sustaining communities like Australia. This might all make for a very interesting more serious historical effort to understand for someone some day.
James E Hanson (Jun 19 2024 at 18:08):Mike Shulman said:
Are you sure there isn't a constructive version of Scott's trick?
So while IZF with collection should be able to do something like Scott's trick 'locally,' I doubt it can be done in a uniformly definable way. So for instance if there is a definable class equivalence relation that only has set-many equivalence classes, then there will be a rank at which you have seen inhabitants of each equivalence class. This feels to me to be very similar to the phenomenon that Friedman used to show that IZF doesn't have the existence property. My intuition about the issue is that while you can grab ranks of elements of a proper class, you can't really settle on some 'canonical' choice of 'sufficiently low' rank.
In particular though, this might mean that there can be class equivalence relations in IZF with no 'Scottification' if they don't have set-many equivalence classes.
Mike Shulman (Jun 19 2024 at 18:39):Do you see something wrong with the approach I sketched?
James E Hanson (Jun 19 2024 at 18:40):Regarding terminology surrounding LEM, large parts of the HoTT book seem to me to be written from the philosophical point of view of propositions-as-types and more generally the type-theoretic paradigm of intermingling logic and stuff as much as possible. For instance, there's a fair amount of discussion of the idea of proof relevance, and Exercise 7.7 uses the notation to discuss type-level generalization of LEM that are inconsistent with univalence. I think it's a pretty natural jump to go from 'well everything should be thought about in untruncated terms' to 'fully untruncated LEM is the correct meaning of LEM.'
Also, if you'll permit me to make a slightly hostile broad statement, I feel like this all feeds into a common ideological stance among people who are really invested in HoTT. A fair number of type theorists don't really like LEM in the first place, so what better way to dismiss it as 'wrong' than to decide that it's inconsistent with univalence, a principle that 'all mathematicians already believe anyway'?
James E Hanson (Jun 19 2024 at 18:40):Mike Shulman said:
Do you see something wrong with the approach I sketched?
The problem is that you have to choose an in the equivalence class. Which one do you use?
Mike Shulman (Jun 19 2024 at 18:41):Maybe we could try to avoid the hostile broad statements?
Mike Shulman (Jun 19 2024 at 18:42):FWIW, that doesn't accord with my experience at all.
James E Hanson (Jun 19 2024 at 18:47):Which part of it doesn't accord with your experience?
James E Hanson (Jun 19 2024 at 18:48):For instance, do you disagree with the claim 'a fair number of type theorists don't really like LEM'?
Mike Shulman (Jun 19 2024 at 18:50):I have seen no evidence that any type theorists have pushed for the untruncated meaning of "LEM" in the hope of discrediting "LEM" by its incompatibility with univalence.
Mike Shulman (Jun 19 2024 at 18:55):It is true that there was some disagreement among the authors of the book as to the importance of truncated vs untruncated logic, and the result is a compromise. Many of us (including me) would have preferred, for instance, to use words like "there exists" and "proposition" in the truncated sense, as that matches ordinary mathematical practice more. And in the past 10 years, that usage seems to have caught on, for the most part, in the HoTT community. But at the time, at least, when truncation in type theory was a more recent innovation, some of the authors were resistant to abandoning the traditional PAT word usage.
Mike Shulman (Jun 19 2024 at 18:57):I think it's a pretty natural jump to go from 'well everything should be thought about in untruncated terms' to 'fully untruncated LEM is the correct meaning of LEM.'
The book is, of course, very clear that this is not the correct meaning of LEM. None of the authors thought that it was. If you have suggestions about how this could be made more clear, I'd be happy to hear them.
James E Hanson (Jun 19 2024 at 20:25):Mike Shulman said:
I have seen no evidence that any type theorists have pushed for the untruncated meaning of "LEM" in the hope of discrediting "LEM" by its incompatibility with univalence.
I'm not saying that it's a conscious effort. I'm saying that this point of view would be pretty reasonable to develop in the context of these kinds of ideas.
For what it's worth, I just googled 'cubical agda LEM' to look at how you state LEM without Prop and, while I know that Reddit is perhaps a 'seedier' part of the internet, for me one of the first results is the following conversation on the Agda subreddit in which two of the three top level comments state something to the effect of 'LEM is inconsistent with univalence.'
When I google 'LEM univalence,' I see a number of results that also seem confused on the issue, including a post on Hacker News and a question on the Computer Science Stack Exchange. Maybe it would help if there was something like a blog post on the n-Category Café titled 'Univalence Is Not Inconsistent with LEM' that might show up in such searches.
Nathanael Arkor (Jun 19 2024 at 20:30):You could add a remark to the nLab page on [[univalence axiom]]?
Madeleine Birchfield (Jun 19 2024 at 20:30):The untruncated and -truncated versions of LEM for in exercise 7.7 aren't LEM, they are global choice principles, and probably deserve a better name than to indicate the relationship with global choice. i.e., the default should be global choice, and it just so happens when either of or is does the axiom degenerate to LEM.
Madeleine Birchfield (Jun 19 2024 at 21:01):James E Hanson said:
Regarding terminology surrounding LEM, large parts of the HoTT book seem to me to be written from the philosophical point of view of propositions-as-types and more generally the type-theoretic paradigm of intermingling logic and stuff as much as possible.
I opened up an issue for the HoTT book to change the default viewpoint of the HoTT book to propositions as (-1)-truncated types and Steve Awodey responded that it would be too big of a change, so I don't think that the propositions as types default viewpoint will change anytime soon for the HoTT book.
https://github.com/HoTT/book/issues/1160
Mike Shulman (Jun 19 2024 at 21:23):I'm not saying that it's a conscious effort. I'm saying that this point of view would be pretty reasonable to develop in the context of these kinds of ideas.
I've seen no evidence of that either. This sort of admittedly-hostile and unfounded speculation about what's going on in other people's minds reminds me that I had reasons for quitting this thread some time ago, but somehow seem to have gotten drawn back in.
Mike Shulman (Jun 19 2024 at 21:24):Maybe it would help if there was something like a blog post on the n-Category Café titled 'Univalence Is Not Inconsistent with LEM' that might show up in such searches.
I suppose that might be worth a try. How about "Univalence is consistent with classical logic"?
Madeleine Birchfield (Jun 19 2024 at 22:24):I feel that canonicity is a bigger barrier to LEM/classical logic being more widely accepted by type theorists than any existing attachments to propositions as types. Type theorists seem to regard having every term reduce down to a canonical form as very important, and LEM blocks reduction to a canonical form. I'm not even sure if MLTT or HoTT with LEM satisfies homotopy canonicity, where every term is identifiable with a canonical form via the identity type.
James E Hanson (Jun 19 2024 at 23:17):Nathanael Arkor said:
You could add a remark to the nLab page on [[univalence axiom]]?
That would probably be reasonable but, as a matter of principle, I'm not sure I should be contributing to a wiki with an explicitly stated editorial agenda that I don't agree with.
James E Hanson (Jun 19 2024 at 23:31):Mike Shulman said:
I suppose that might be worth a try. How about "Univalence is consistent with classical logic"?
Considering the fact that I have actually encountered a type theorist (or at least someone who seems to know about type theory) online who used the term 'classical' to refer to non-univalent but constructive type theory, I'm not sure this would be pointed enough.
James E Hanson (Jun 19 2024 at 23:36):Mike Shulman said:
This sort of admittedly-hostile and unfounded speculation about what's going on in other people's minds reminds me that I had reasons for quitting this thread some time ago, but somehow seem to have gotten drawn back in.
I don't think my statement is unfounded, and I feel like you're not really trying to interpret my words 'as charitably as possible' right now. I'm not trying to say these things as a judgment. I think it's just a fact that a lot of type theorists don't like LEM. LEM really doesn't fit well into the way type theorists think about logic. After that I was forwarding a hypothetical about why such an attitude might be psychologically compatible with the idea that LEM is inconsistent with univalence.
Madeleine Birchfield (Jun 20 2024 at 00:07):Nathanael Arkor said:
You could add a remark to the nLab page on [[univalence axiom]]?
James E Hanson said:
That would probably be reasonable but, as a matter of principle, I'm not sure I should be contributing to a wiki with an explicitly stated editorial agenda that I don't agree with.
Also, somebody else had already done so: https://nforum.ncatlab.org/discussion/8476/univalence-axiom/?Focus=117570#Comment_117570
David Michael Roberts (Jun 20 2024 at 00:15):James E Hanson said:
That would probably be reasonable but, as a matter of principle, I'm not sure I should be contributing to a wiki with an explicitly stated editorial agenda that I don't agree with.
All the more reason to do so! You just have to be happy with the wiki philosophy that things can be edited. But if it's not added in the first place, the information won't mysteriously appear on its own.
David Michael Roberts (Jun 20 2024 at 00:19):But I'm curious what you think of neutral mathematics, @James E Hanson . No negation of LEM, but no taking it as given. So it holds in some models but not others, and not making a commitment to either philosophical position.
Madeleine Birchfield (Jun 20 2024 at 00:23):James E Hanson said:
I think it's just a fact that a lot of type theorists don't like LEM. LEM really doesn't fit well into the way type theorists think about logic.
I don't think this really has anything to do with logic. The big problem is when type theorists get caught up on computational aspects of implementing type theory as a programming language or proof assistant such as decidable judgmental equality or canonicity or normalisation. All of a sudden, axioms like propositional resizing (impredicativity), excluded middle, UIP, univalence, choice, and replacement become problematic and cannot be used or else some important computational property breaks like canonicity.
This is why many type theorists are not just constructivists but also predicativists and reject the set of truth values/subobject classifier/type of all propositions as well; it has nothing to do with logic and everything to do with the axiom not interacting well with computation. It's also why type theorists spent so much time developing cubical type theory and are now developing higher observational type theory, so that they can make univalence behave well with computation.
If tomorrow a dependent type theory lands on Earth which has LEM and satisfies all the desirable computational properties of a type theory such as decidable equality, canonicity, normalisation, etc, then it is very likely type theorists will be more accepting of LEM because a major roadblock for acceptance has been removed.
James E Hanson (Jun 20 2024 at 00:29):@David Michael Roberts I'm not talking about constructivism. (I like constructive math, clearly, but for the record I really don't buy a lot of the rhetoric that's used to try to convince mathematicians that they should be interested in it.) What I'm actually talking about is the nPOV. I'm not really sold on the sentiment expressed in this quote:
Around the nLab it is believed that higher algebra, homotopy theory, type theory, category theory and higher category theory provide a point of view on Mathematics, Physics and Philosophy which is a valuable unifying point of view for the understanding of the concepts involved.
I think that claiming these things have a unifying role in physics and philosophy is especially reaching, but I also am not really sold on it in the context of mathematics.
Although, as came up before, this depends a lot on how extremely one interprets this position. For instance this statement is pretty clearly unobjectionable:
Rather, the nLab starts from the premise that higher algebra, homotopy theory, type theory, category theory and higher category theory are a true and useful point of view, and one of its aims is to expose this point of view generally and in a multitude of examples, and thereby accumulate evidence for it.
James E Hanson (Jun 20 2024 at 00:32):Madeleine Birchfield said:
...become problematic and cannot be used or else some important computational property breaks like canonicity.
I thought that impredicativity didn't actually interfere with canonicity. System F is impredicative but has strong normalization, for instance.
This is why many type theorists are not just constructivists but also predicativists and reject the set of truth values/subobject classifier/type of all propositions as well; it has nothing to do with logic and everything to do with the axiom not interacting well with computation.
I feel like this still works with my point. Proposition-level-LEM is most easily stated if you have Prop. It doesn't seem like as natural of a principle in the context of something like Agda.
David Michael Roberts (Jun 20 2024 at 00:35):I wasn't specifying constructivism in my first comment. The second comment was independent of the first, and related to the LEM discussion.
The nPOV is not a rigid rule. And there is a lot of stuff on there that is really wholly unrelated to any higher category stuff. Sure, the fundamental theorem of algebra, say, is discussed from both a classical and constructive viewpoint, but there's really nothing that can be said that involves n-categories. Lots of maths really is just 1-categorical (or even 0-categorical, for that matter), and no amount of n-categories will help. It's just that there are things where n- and -categories really do help and when the nLab started that approach really wasn't known or being emphasised. That nPOV statement is over 15 years old now, and the community (at the nLab and more widely) has changed a lot.
James E Hanson (Jun 20 2024 at 00:46):David Michael Roberts said:
The nPOV is not a rigid rule.
I didn't say it was a rigid rule. I said it was an explicitly stated editorial agenda, which I think is pretty hard to argue with when you have statements like 'In particular, the nLab has a particular point of view, which we may call the nPOV, the higher algebraic, homotopical, or n- categorical point of view.' and 'So at the nLab, we don’t care so much about being neutral.'
It's just that there are things where n- and ∞-categories really do help and when the nLab started that approach really wasn't known or being emphasised.
I'm not debating that, but that's also not what the page says. The page makes some concessions to the idea that other points of views may be valid, but then it does also contain the quote I mentioned earlier. It presents the statement
higher algebra, homotopy theory, type theory, and/or category theory is the right language to describe the world, or at least the world of mathematical ideas.
as a claim to be debated, rather than explicitly stating it, but despite this kind of hedging the way it's framed makes it pretty clear that this is supposed to be the philosophical stance of the website and I do not agree with that stance.
That nPOV statement is over 15 years old now, and the community (at the nLab and more widely) has changed a lot.
Then maybe the page should be changed, because from my point of view it still feels like a pretty accurate description of the philosophical stance of a lot of people in the social sphere of nLab.
Madeleine Birchfield (Jun 20 2024 at 00:52):James E Hanson said:
Madeleine Birchfield said:
...become problematic and cannot be used or else some important computational property breaks like canonicity.
I thought that impredicativity didn't actually interfere with canonicity. System F is impredicative but has strong normalization, for instance.
This is why many type theorists are not just constructivists but also predicativists and reject the set of truth values/subobject classifier/type of all propositions as well; it has nothing to do with logic and everything to do with the axiom not interacting well with computation.
I feel like this still works with my point. Proposition-level-LEM is most easily stated if you have
Prop. It doesn't seem like as natural of a principle in the context of something like Agda.
The thing with dependent type theories like Agda/Coq/Book HoTT is not that they don't have a Prop, but that they have a Prop for every single universe in the theory. However, the Prop for the universe lies in the next universe up, so is inaccessible to anybody working inside of that universe. In addition, it is impossible to prove that any two universes' Prop are equivalent to each other. One can only prove that if a universe is a subuniverse of another universe, than the first universe's Prop is a subset of the second universe's Prop.
The impredicativity axiom (propositional resizing) says that there is a special Prop at the base universe (level 0) which is equivalent to every universe's Prop. And I believe it is this resizing axiom in dependent type theory in particular that falls afoul of canonicity.
LEM is also easily stated for each Propof the universe, so it is as easy to state in Agda/Coq/Book HoTT as it is in a constructive set theory, since all the rules are indexed by universe level anyways in Agda/Coq/Book HoTT.
James E Hanson (Jun 20 2024 at 00:57):David Michael Roberts said:
But I'm curious what you think of neutral mathematics, James E Hanson . No negation of LEM, but no taking it as given. So it holds in some models but not others, and not making a commitment to either philosophical position.
I guess if you really want to have a second conversation about this, I feel like the versions of 'neutral constructive mathematics' I've seen aren't really that neutral. Classical mathematical logicians who are interested in working in weak systems (like people studying weak arithmetic or reverse mathematics) often work with systems in which full induction on the natural numbers isn't provable. In basically all but the very weakest type theories you still have full induction on the natural numbers. Edward Nelson wouldn't have considered Agda to be predicative for instance.
Similarly, there are a handful of philosophical/practical reasons why someone might want to consider various sub-intuitionistic logics (for instance if you're interested in polytime realizability). I haven't seen anyone trying to argue for neutral (constructive) math talk about how interesting universes where modus ponens fails might be.
Madeleine Birchfield (Jun 20 2024 at 01:06):The fact that Agda, Coq, Book HoTT, and Lean all have Prop derivable from universes is one reason why I don't really consider any of them to really be predicative. Prop is a size issue in these theories in the same way that Set is a size issue more generally in mathematics. You can still construct power sets as function sets into a Prop and the Dedekind real numbers impredicatively using the usual definition but you have to index everything by universe level and track which universe level the objects belong to.
Compare that to the version of MLTT without universes or predicative constructive set theories like CZF where in general you don't have a Prop at all.
Madeleine Birchfield (Jun 20 2024 at 02:07):James E Hanson said:
I guess if you really want to have a second conversation about this, I feel like the versions of 'neutral constructive mathematics' I've seen aren't really that neutral.
This is an artifact of how constructive mathematics developed historically. Neutral constructive mathematics arose out of trying to find a common minimal basis for the main schools of constructivism at the time (Bishop's constructivism, Russian constructivism, Brouwer's constructivism, etc). All of them worked in an impredicative set theory with power sets defined in intuitionistic first-order logic, but all accepted different axioms which contradicted with each other, as well as weaker versions of the axiom of choice. It was in this atmosphere that the idea of "neutral" constructive mathematics developed, one which none of the weaker choice axioms or the additional axioms would hold, so the theorems in neutral constructive mathematics can be proven in all the main schools of constructivism as well as in classical mathematics. Since every single one of the relevant main constructive schools accepted impredicativity/power sets, in the end neutral constructive mathematics became synonymous with working in IZF/IBZ or in an elementary topos or in intuitionistic higher-order logic. So neutral constructive mathematics really should be called neutral impredicative constructive mathematics from the perspective of predicativists.
Madeleine Birchfield (Jun 20 2024 at 03:06):When one tries to define a neutral predicative constructive mathematics the problem is that no one really works in anything that is neutrally predicative constructive - one has to find some foundation that is able to support both the classical predicativists who reject general function sets as well as the constructive predicativists who reject the subset classifier. CZF and MLTT aren't predicative enough since they both support function sets or function types.
James E Hanson (Jun 20 2024 at 03:16):@Madeleine Birchfield This is something I'm kind of uncertain about. Is it clear that the really weak forms of constructive predicativism and the really weak forms of classical predicativism are really 'the same kind of thing'? They seem to behave somewhat differently to me.
Josselin Poiret (Jun 20 2024 at 10:16):Madeleine Birchfield said:
I feel that canonicity is a bigger barrier to LEM/classical logic being more widely accepted by type theorists than any existing attachments to propositions as types. Type theorists seem to regard having every term reduce down to a canonical form as very important, and LEM blocks reduction to a canonical form. I'm not even sure if MLTT or HoTT with LEM satisfies homotopy canonicity, where every term is identifiable with a canonical form via the identity type.
Depends on which kind of type theorist you're talking about. Some of them just use type theories as an internal language for topoi, where they're plenty happy using LEM if the corresponding topos validates it. However, as you said, many type theorists are interested in the computational content of terms, and in this case there is no corresponding interpretation of LEM in the usual computational interpretation of MLTT.
Through double-negation elimination though, one can give computational content to LEM: recall that under DNE, , hence the DNE of LEM is (using the involutive properties of ). This translation fails the usual witness property that from a proof of one can actually find such an . Instead, it merely means that is impossible to prove a general counterexample. Similarly for : you don't know which one is true, but it is impossible for both to be provably false. View this instead as a program interacting with the outside world: it never reveals any witness of its claims, you can only give it counterarguments. In this case, if you give it and , it will prove to you that you're lying, and that's it.
IMO one could distinguish constructive and intuitionistic: the former is about specific interpretations of a logic, while the latter is a specific type of logic that so happens to have a constructive interpretation, and a pretty nice one. Some inconsistent type theories can have constructive interpretations as e.g. processes that might fail: they might produce actual facts but you won't know until you run them.
Josselin Poiret (Jun 20 2024 at 10:23):Madeleine Birchfield said:
I'm not even sure if MLTT or HoTT with LEM satisfies homotopy canonicity, where every term is identifiable with a canonical form via the identity type.
that's not possible: you'd be able to decide any constructive fact and get a constructive proof of it! The only way this could be true would be by modifying the notion of canonical forms to include blocked computations of LEM.
Josselin Poiret (Jun 20 2024 at 10:26):Madeleine Birchfield said:
If tomorrow a dependent type theory lands on Earth which has LEM and satisfies all the desirable computational properties of a type theory such as decidable equality, canonicity, normalisation, etc, then it is very likely type theorists will be more accepting of LEM because a major roadblock for acceptance has been removed.
that's not true if you take the POV of neutral mathematics: even if you're a classic mathematician, you might want to prove stuff synthetically in a non-Boolean topos and there you cannot rely on LEM even if you have it externally. You will thus still want constructive type theories.
Josselin Poiret (Jun 20 2024 at 10:29):Madeleine Birchfield said:
This is why many type theorists are not just constructivists but also predicativists and reject the set of truth values/subobject classifier/type of all propositions as well; it has nothing to do with logic and everything to do with the axiom not interacting well with computation.
I wouldn't say that it's common for type theorists to be predicativists: Coq and Lean are impredicative at heart, and that's used quite often.
James E Hanson said:
I thought that impredicativity didn't actually interfere with canonicity. System F is impredicative but has strong normalization, for instance.
System F has strong normalization if your metatheory is impredicative. I don't think you can prove System F to be normalizing in e.g. Agda without propositional resizing, there's some ordinal analysis fact about this IIRC.
Josselin Poiret (Jun 20 2024 at 10:31):Madeleine Birchfield said:
The fact that Agda, Coq, Book HoTT, and Lean all have
Propderivable from universes is one reason why I don't really consider any of them to really be predicative.Propis a size issue in these theories in the same way thatSetis a size issue more generally in mathematics.
How is Prop 0 a size issue when it can inhabit Type 1?
Madeleine Birchfield (Jun 20 2024 at 11:05):Josselin Poiret said:
Madeleine Birchfield said:
The fact that Agda, Coq, Book HoTT, and Lean all have
Propderivable from universes is one reason why I don't really consider any of them to really be predicative.Propis a size issue in these theories in the same way thatSetis a size issue more generally in mathematics.How is
Prop 0a size issue when it can inhabitType 1?
I say Prop 0is a size issue because it doesn't inhabit Type 0 without a resizing axiom that many people don't use.
Josselin Poiret (Jun 20 2024 at 11:46):is that truly a problem? it is a universe, so it's expected to be "too big" in a sense
Madeleine Birchfield (Jun 20 2024 at 11:49):Josselin Poiret said:
is that truly a problem? it is a universe, so it's expected to be "too big" in a sense
That's my whole point - Prop in Agda/Coq/book HoTT behave the same way that Set and nGrpd do in Agda/Coq/book HoTT - Set 0 and nGrpd 0 lie in Type 1 but do not lie in Type 0. So you have to keep track of all the universe levels.
Josselin Poiret (Jun 20 2024 at 11:55):But why would that lead you to not consider Agda predicative?
Madeleine Birchfield (Jun 20 2024 at 11:57):In the context of predicativism I think one has to make a distinction between "power sets exist but aren't small" and "power sets don't exist in the theory at all". I don't really consider the former to be predicative because you can still do everything you can in impredicative mathematics, only with the additional bureaucracy of keeping track of size or universe levels.
The latter is much more restrictive since certain constructions (i.e Dedekind reals via Dedekind cuts) aren't really possible without power sets.
Josselin Poiret (Jun 20 2024 at 12:03):Madeleine Birchfield said:
I don't really consider the former to be predicative because you can still do everything you can in impredicative mathematics, only with the additional bureaucracy of keeping track of size or universe levels.
you cannot: see what I mentioned about strong normalization of System F, or the existence of complete lattices
Josselin Poiret (Jun 20 2024 at 12:05):impredicativity manages to bump up the logical strength of the theory
Madeleine Birchfield (Jun 20 2024 at 12:06):Josselin Poiret said:
you cannot: see what I mentioned about strong normalization of System F, or the existence of complete lattices
Complete lattices in Agda/Coq/book HoTT are a size issue as well, they are defined complete relative to a universe in the same way that Grothendieck toposes are defined to have all coproducts relative to a universe.
Josselin Poiret (Jun 20 2024 at 12:13):while you might see it as just a size issue it does end up affecting logical strength, and this restriction is IMO exactly the one of predicativism: one cannot build possibly self-referential objects, ie. objects quantified over what they themselves are
Morgan Rogers (he/him) (Jun 20 2024 at 15:34):James E Hanson said:
Similarly, there are a handful of philosophical/practical reasons why someone might want to consider various sub-intuitionistic logics (for instance if you're interested in polytime realizability). I haven't seen anyone trying to argue for neutral (constructive) math talk about how interesting universes where modus ponens fails might be.
I asked a bunch of logicians about this a few years ago, I certainly think it's an interesting thing to think about.
Morgan Rogers (he/him) (Jun 20 2024 at 15:52):James E Hanson said:
Nathanael Arkor said:
You could add a remark to the nLab page on [[univalence axiom]]?
That would probably be reasonable but, as a matter of principle, I'm not sure I should be contributing to a wiki with an explicitly stated editorial agenda that I don't agree with.
It seems like your own principles are in conflict with one another here. You want the nLab to change because you disagree with how things are presented there, but you also don't want to change the nLab (yourself) because you disagree with how things are presented there?
You've made clear that you're not sold on the nPOV, but that doesn't really justify you not contributing to a resource that is used by plenty of people who may share your scepticism. Contributing to a community wiki doesn't constitute an endorsement of the entire corpus of text contained in the wiki.
James E Hanson (Jun 20 2024 at 17:39):Josselin Poiret said:
System F has strong normalization if your metatheory is impredicative. I don't think you can prove System F to be normalizing in e.g. Agda without propositional resizing, there's some ordinal analysis fact about this IIRC.
Well first of all, Arai recently claimed to have a proof-theoretic ordinal for full second-order arithmetic (see Theorem 1.4 here). Given the tight relationship between System F and , this should also in some sense characterize the behavior of term normalization in System F. This should mean that some weak theory like PRA together with the statement that that computable ordinal is computably well-founded should be able to prove that System F has strong normalization. I don't know if this counts as 'predicative' though, since at the high end of consistency strength that term seems to be a bit vague and philosophical.
Second of all, how many people familiar with the matter actually don't believe that terms in System F strongly normalize? In other words, why does it matter whether the proof potentially requires an impredicative metatheory? We know that there are always going to be computable well-orders that are arbitrarily hard to show are actually well-ordered.
James E Hanson (Jun 20 2024 at 17:59):Morgan Rogers (he/him) said:
It seems like your own principles are in conflict with one another here. You want the nLab to change because you disagree with how things are presented there, but you also don't want to change the nLab (yourself) because you disagree with how things are presented there?
I have not made conflicting statements. I didn't make a statement one way or the other about whether I want the nLab to change. I said that if David is right and the nPOV page isn't really an accurate description of the nLab community anymore, then maybe they should change the nPOV page. The nPOV page is linked from the front page of the website and from numerous other articles.
You've made clear that you're not sold on the nPOV, but that doesn't really justify you not contributing to a resource that is used by plenty of people who may share your scepticism. Contributing to a community wiki doesn't constitute an endorsement of the entire corpus of text contained in the wiki.
First of all, I don't think I really need strong justification to not contribute free labor to a project, but I also think that objecting to the nPOV absolutely does justify it. Right now the website literally and proudly says 'we don't care about being neutral.' This is the mission statement of the website, not just some random page on it. The other thing is just that people who share my skepticism already are pretty skeptical of nLab as an unbiased reference (and why shouldn't they be, it literally says it doesn't care about being neutral).
I feel like David didn't really understand my objection to the nPOV. My objection isn't that higher category theory isn't useful. Higher category theory seems to me to be a really natural (and useful) development of category theory. My objection is that I don't think category theory in general is as universally useful as nLab seems to think it is (and I feel like this is pretty clear if you look at my earlier arguments about set theory). The average nLab article seems to be written from the point of view that literally everything is best phrased in the most categorically generalized terms possible, and I just don't find that credible.
Nathanael Arkor (Jun 20 2024 at 21:14):First of all, I don't think I really need strong justification to not contribute free labor to a project
Given how much time you have dedicated to addressing misunderstandings here on Zulip, which has a much smaller audience than the nLab, that would already seem to me justification enough to contribute?
Nathanael Arkor (Jun 20 2024 at 21:18):This is the mission statement of the website, not just some random page on it.
The majority of the active contributors to the nLab at the moment are not motivated by that page. Most contributors simply treat the nLab as an online wiki for category/type theory-related mathematics. Why not at least try starting a discussion there about the aspects you find problematic? I am sure Urs will be happy to engage in a discussion.
Nathanael Arkor (Jun 20 2024 at 21:21):The other thing is just that people who share my skepticism already are pretty skeptical of nLab as an unbiased reference (and why shouldn't they be, it literally says it doesn't care about being neutral).
I think this is missing the point of the nLab. You should never take any reference to be unbiased. But a reference can be useful even if it is biased. And if you feel there is bias, then you can address it. I don't think Urs will object to such changes, despite what the "nPOV" page says.
Nathanael Arkor (Jun 20 2024 at 21:21):The nPOV page was written in the early days of the nLab. A lot has changed since then in the attitudes to what is appropriate on the nLab.
Nathanael Arkor (Jun 20 2024 at 21:22):The average nLab article seems to be written from the point of view that literally everything is best phrased in the most categorically generalized terms possible, and I just don't find that credible.
I don't think that's accurate. I would say it is more accurate to say that the average nLab article is written from the point of view that many things in mathematics can be phrased categorically, and that this is often useful for category theorists.
Nathanael Arkor (Jun 20 2024 at 21:23):For non-category theorists, it is not likely to be helpful. But the nLab is not a resource for general mathematicians: this is not a sign of bias, but rather a sign of target audience.
Kevin Carlson (Jun 20 2024 at 21:32):It might be worth highlighting that nLab presents itself as "not neutral" in contrast to the fact that "neutral point of view" is a central design factor for Wikipedia. This is a very tight constraint on a wiki; I think even in 2010 the idea of the n-point of view was more to signal the nLab as lacking an editorial constraint Wikipedia has, in being willing to be opinionated, moreso than in imposing an editorial constraint that content must be consistent with the n-point of view. Certainly nobody ever complains about anything plausibly relevant that gets added to the nLab for not being ideologically correct.
John Baez (Jun 20 2024 at 22:15):I think a not insignificant factor was the joke that "nPOV" has a double meaning. I don't think people back then knew that the nLab would become so important that they had to be careful about what they said.
Madeleine Birchfield (Jun 20 2024 at 22:31):Nathanael Arkor said:
The nPOV page was written in the early days of the nLab. A lot has changed since then in the attitudes to what is appropriate on the nLab.
If there is any discrepancies between what the nPOV page says and current attitudes of what is appropriate on the nLab then the nPOV page should be updated to reflect current attitudes rather than those of 15 years past, or replaced with a new page which reflects current attitudes if current attitudes are very far from the nPOV.
Madeleine Birchfield (Jun 20 2024 at 22:36):As far as I can tell the nPOV isn't really relevant for a lot of the new content being put on the nLab, especially those related to string theory and quantum information theory and quantum computing. It's more like Urs Schreiber is treating the nLab as his own personal notebook and creating nLab articles for whatever is currently related to his research.
Kevin Carlson (Jun 20 2024 at 22:48):I've just made some minor edits to the n-point of view page that I think are clearly consistent with how the nLab works these days and hopefully won't make anybody mad--in particular I've made it say that only parts of the nLab are relevant to the n-point of view and that skeptics of that point of view are welcome to contribute.
Kevin Carlson (Jun 20 2024 at 22:48):I agree that "whatever Urs wants to write about" is a more fundamental principle determining what lands on the nLab than the n-point of view!
David Michael Roberts (Jun 21 2024 at 01:49):I think Urs (and others, of course) would much prefer people add decent content rather than worry about editorial bias or whatever. Just do due diligence to try to make the content mathematically worthwhile (we've had examples of ... the other sort) and also at least in visual style fit the general mold of how pages work.
Todd Trimble (Jun 21 2024 at 06:10):If James H. would like to add content to articles on model theory, for example, that would be hugely appreciated. Just aim to be explanatory at the level of a second-year grad student, or so. Don't worry about n-stuff.
David Michael Roberts (Jun 21 2024 at 06:59):And, not to put too fine a point on it: n is a variable here, and can be 1 or even 0. No one in their right mind would think that classical point-set topology (of which there is a nonzero amount on the nLab eg https://ncatlab.org/nlab/show/Introduction+to+Topology+--+1) is somehow better understood using n-categories with n > 1.
David Michael Roberts (Jun 21 2024 at 07:01):In that big page you get:
In passing, some basics of category theory make an informal appearance, used to transparently summarize some conceptually important aspects of the theory, such as initial and final topologies and the reflection into Hausdorff and sober topological spaces.
David Michael Roberts (Jun 21 2024 at 07:06):I tweaked the page [[nPOV]] very slightly again ("the nLab starts" -> "the nLab started") and so the "no commitment to being neutral" paragraph now reads:
In particular, at the nLab, there is no commitment to being neutral. There are certainly other valid points of view on mathematics, but describing them and being neutral towards them is not the purpose of the nLab. Rather, the nLab started from the premise that higher algebra, homotopy theory, type theory, category theory and higher category theory are a useful point of view, and one of its aims is to expose this point of view generally and in a multitude of examples, and thereby accumulate evidence for it.
If you feel skeptical about the n-point of view, you should still find the nLab useful, as the largest site for detailed category-theoretic information online. You are very much welcome to contribute relevant content even if you are such a skeptic.
Josselin Poiret (Jun 21 2024 at 07:50):James E Hanson said:
Second of all, how many people familiar with the matter actually don't believe that terms in System F strongly normalize? In other words, why does it matter whether the proof potentially requires an impredicative metatheory?
This is something I'm interested about as well: is there anything to understand out of this impossibility? why would the normalization of some simple syntax require such a metatheory, and what does it say about the system? what can we expect from system F predicatively?
John Baez (Jun 21 2024 at 07:50):Madeleine Birchfield said:
As far as I can tell the nPOV isn't really relevant for a lot of the new content being put on the nLab, especially those related to string theory and quantum information theory and quantum computing. It's more like Urs Schreiber is treating the nLab as his own personal notebook and creating nLab articles for whatever is currently related to his research.
And that's fine.
If you want a reasonably accurate statement of the purpose of the nLab, don't read the nPOV statement: read the section Purpose on the home page of the nLab. Not only is this more accurate, more people are likely to read it, so it's more likely to influence what people do.
Todd Trimble (Jun 21 2024 at 08:03):David Michael Roberts said:
And, not to put too fine a point on it: n is a variable here, and can be 1 or even 0. No one in their right mind would think that classical point-set topology (of which there is a nonzero amount on the nLab eg https://ncatlab.org/nlab/show/Introduction+to+Topology+--+1) is somehow better understood using n-categories with n > 1.
Well, with all due respect to [[relational beta-module]], which uses Rel as a 2-category.
Alexander Campbell (Jun 21 2024 at 08:18):David Michael Roberts said:
And, not to put too fine a point on it: n is a variable here, and can be 1 or even 0.
And perhaps even -1 or -2...
Damiano Mazza (Jun 21 2024 at 08:43):Yes I think that most people I know who "don't like the nLab" (whatever that means) are only comfortable with :wink:
Morgan Rogers (he/him) (Jun 21 2024 at 09:51):James E Hanson said:
Morgan Rogers (he/him) said:
It seems like your own principles are in conflict with one another here. You want the nLab to change because you disagree with how things are presented there, but you also don't want to change the nLab (yourself) because you disagree with how things are presented there?
I have not made conflicting statements. I didn't make a statement one way or the other about whether I want the nLab to change. I said that if David is right and the nPOV page isn't really an accurate description of the nLab community anymore, then maybe they should change the nPOV page.
People have been very accommodating to your position here, but I want to flag that complaining about something publicly and then denying that you expressed a desire for it to change under the pretext that you technically "didn't make a statement one way or the other" is borderline trolling behaviour.
Relatedly, I observed that your response to Mike opening issues on GitHub about the HoTT book in no way acknowledged that someone had gone out of their way to address your complaints. I appreciate that you are in a minority in this discussion, and that might be putting pressure on you (having seven different people replying to you is a lot), but please show some respect for the concessions that people are making to your arguments.
Graham Manuell (Jun 21 2024 at 12:16):I think it is very important that people are allowed to advocate for alternative foundations or approaches to mathematics, so I disagree with James's positions there, but for what it's worth I think he is being very reasonable when he says he doesn't want to edit the nLab because he thinks it advocates for a position he doesn't agree with. Even if he agreed with the nLab philosophy in every way he still would be under no obligation to edit it.
Graham Manuell (Jun 21 2024 at 12:26):Josselin Poiret said:
James E Hanson said:
Second of all, how many people familiar with the matter actually don't believe that terms in System F strongly normalize? In other words, why does it matter whether the proof potentially requires an impredicative metatheory?
This is something I'm interested about as well: is there anything to understand out of this impossibility? why would the normalization of some simple syntax require such a metatheory, and what does it say about the system? what can we expect from system F predicatively?
For what it's worth Nik Weaver has argued that (some) ordinals beyond the Feferman-Schütte ordinal should still be regarded as predicative.
John Baez (Jun 21 2024 at 13:21):I've never understood Weaver's argument for considering ordinals beyond the Feferman-Schütte to be predicative. Does anyone understand this debate (which may be everyone against Weaver)?
David Michael Roberts (Jun 21 2024 at 13:33):@Todd Trimble as a 2-category or as a (1,2)-category?
And if I see a proof of a classic point set topology theorem (say about metrizability or whatnot) that uses the 2-category structure of Rel and beta-modules therein, I certainly will give it all due reverence :-)
Todd Trimble (Jun 21 2024 at 13:49):David Michael Roberts said:
Todd Trimble as a 2-category or as a (1,2)-category?
And if I see a proof of a classic point set topology theorem (say about metrizability or whatnot) that uses the 2-category structure of Rel and beta-modules therein, I certainly will give it all due reverence :-)
Yeah, I had considered saying "locally posetal 2-category", anticipating such pedantry.
Graham Manuell (Jun 21 2024 at 14:40):John Baez said:
I've never understood Weaver's argument for considering ordinals beyond the Feferman-Schütte to be predicative. Does anyone understand this debate (which may be everyone against Weaver)?
I don't understand it either, but very large countable ordinals confuse me in general. Weaver does have some credibility in being one of only people involved who calls themself a predicativist.
John Baez (Jun 21 2024 at 16:11):I'm not sure if I'm less confused than you, or more. I spent some time studying large countable ordinals up to around the Feferman-Schütte ordinal, which I explained here. But things get a bit strange when people say
The Feferman-Schütte ordinal is the smallest ordinal that cannot be described without self-reference.
John Baez (Jun 21 2024 at 16:12):even though I don't think anyone claims that's the definition of it.
James E Hanson (Jun 21 2024 at 21:00):Morgan Rogers (he/him) said:
People have been very accommodating to your position here, but I want to flag that complaining about something publicly and then denying that you expressed a desire for it to change under the pretext that you technically "didn't make a statement one way or the other" is borderline trolling behaviour.
I am sorry. I am not trying to be a troll. I don't entirely like being accused of making self-contradictory statements (although I certainly do sometimes), so I reacted in a brash way. I should have phrased my response more carefully.
James E Hanson (Jun 21 2024 at 21:15):Nathanael Arkor said:
Given how much time you have dedicated to addressing misunderstandings here on Zulip, which has a much smaller audience than the nLab, that would already seem to me justification enough to contribute?
You're right that the time commitment of the originally suggested change would be quite small compared to the amount of time I've spent here, but I don't really think these are directly comparable.
James E Hanson (Jun 21 2024 at 21:17):Nathanael Arkor said:
I don't think that's accurate. I would say it is more accurate to say that the average nLab article is written from the point of view that many things in mathematics can be phrased categorically, and that this is often useful for category theorists.
For non-category theorists, it is not likely to be helpful. But the nLab is not a resource for general mathematicians: this is not a sign of bias, but rather a sign of target audience.
Todd Trimble said:
If James H. would like to add content to articles on model theory, for example, that would be hugely appreciated. Just aim to be explanatory at the level of a second-year grad student, or so. Don't worry about n-stuff.
I know that Nathanael and Todd might not be thinking the same thing here, but I don't really see how to entirely square these two comments. A lot of intermediate model theory has seemingly never actually been written down in categorical language. Obviously I could theoretically put the work in to translating it, but that is a lot of effort.
Todd Trimble (Jun 21 2024 at 21:24):You don't have to put it down in categorical language -- that's what some of us are saying. Just having an exposition from an expert, written at not-too-advanced level (I said "second-year grad student"), would be very welcome.
The one thing you should know going in is that other people might come in later and see about translating some of it into language congenial to those who like category theory. There's a mostly unstated rule that the regulars try not to erase the competent work of others, but just add to it ("yes and") where they believe it appropriate and useful.
Some people might be uncomfortable knowing that other people might fiddle with an article they started. But if you can make your peace with that, then having expert input from an expert like you, written in your native tongue but more or less ab initio, would be a huge boon.
James E Hanson (Jun 21 2024 at 21:29):Josselin Poiret said:
This is something I'm interested about as well: is there anything to understand out of this impossibility? why would the normalization of some simple syntax require such a metatheory, and what does it say about the system? what can we expect from system F predicatively?
Do you think it's somehow less mysterious than the consistency strength of second-order arithmetic itself? To me the relationship seems pretty clear. The polymorphism in System F directly corresponds to the impredicativity of defining sets of naturals by quantifying over the collection of all sets of naturals.
Madeleine Birchfield (Jun 21 2024 at 21:32):James E Hanson said:
I know that Nathanael and Todd might not be thinking the same thing here, but I don't really see how to entirely square these two comments. A lot of intermediate model theory has seemingly never actually been written down in categorical language. Obviously I could theoretically put the work in to translating it, but that is a lot of effort.
Categorical language is not a requirement for the nLab at all. A lot of the stuff Urs Schreiber puts on the nLab isn't in categorical language, and it would probably be extremely hard to put condensed matter physics stuff like [[nitrogen-vacancy center in diamond]] in categorical language.
James E Hanson (Jun 21 2024 at 21:41):Graham Manuell said:
Weaver does have some credibility in being one of only people involved who calls themself a predicativist.
I have a lot of respect for Weaver—I really like his book on Lipschitz algebras, for instance—but I don't find all of his arguments about foundational issues convincing. If you look at section 7 of "Is set theory indispensable?" for instance, it seems like his argument that ZFC is probably not arithmetically sound is more or less 'I find it hard to believe that it is.' He also at times has made the case that while it's coherent to imagine exhaustively searching a countable collection (thus justifying classical reasoning about the naturals), it is not coherent to imagine exhaustively searching an uncountable collection. (See section 3.2 of "The concept of a set" for instance.) There's certainly a difference between these and a fair amount of philosophical subtlety, but I don't see where he's getting his extreme confidence in classical reasoning about the naturals and extreme distrust of classical reasoning about uncountable objects. I actually think ordinal Turing machines provide a pretty clear mental picture of a context in which one is in some sense mechanically searching an uncountable collection of objects, in contrast to his statement 'This is because we have no clear conception of what it would be like to look through all real numbers, or all countable ordinals, even if supertasks were allowed.'
James E Hanson (Jun 21 2024 at 21:43):So in particular, I'm not sure I would weight his opinion of what 'the first impredicative countable ordinal' is more heavily than others', since it's already a fairly philosophical question in the first place.
Graham Manuell (Jun 22 2024 at 18:55):I haven't read the whole paper yet, but I don't think that is a fair characterisation of Weaver's argument in section 7. He is saying that if you reject the Platonist arguments for ZFC, then there doesn't seem to be much reason to believe it is sound. I suppose the idea is that the evidence for soundness of ZFC is really just evidence of the soundness of much much weaker theories and in the absence of any any evidence it is probably more likely for a random consistent theory to be unsound. If you have non-Platonist reasons for believing ZFC is sound, I for one would be very interested in hearing them.
I am just giving him extra weight in the sense that "predicativism is what predicativists believe".
James E Hanson (Jun 23 2024 at 14:29):Graham Manuell said:
I think it is very important that people are allowed to advocate for alternative foundations or approaches to mathematics, so I disagree with James's positions there,
Graham, thank you for the supporting words, but I'm not sure I agree that this is a summary of my position.
Graham Manuell (Jun 23 2024 at 18:19):Sorry. I didn't mean to suggest your position is literally "people should not be allowed to advocate for alternative approaches". What I meant was that I think it is important for people to advocate for alternative approaches, and because of this I disagree with your position, which apparently includes that people need to be very careful about implications of their advocacy on the dominant paradigm, because it alienates people and/or possibly contributes to the lack of jobs in set theory. I think holding people to such a high standard for even off-the-cuff remarks in a talk could have a chilling effect.
James E Hanson (Jun 26 2024 at 19:35):@Graham Manuell I don't think that people shouldn't be allowed to advocate for alternative approaches, but I think that the root of my problem is that a lot of the criticism people levy isn't substantive and just ends up devolving into mockery that feeds into broader cultural hostility. The fact that (under the most commonly used encoding of natural numbers) 2 is an element of 3 isn't really a practical impediment to formalizing mathematics in ZFC. The only real problem with it is aesthetic, but this is sometimes presented by itself as conclusive evidence of the insufficiency of set theory for formalizing mathematics.
This kind of criticism starts veering into territory that is implicitly hostile to really fundamental ideas in classical mathematical logic, like implying that things like the axiom of foundation are 'artifical.' The cumulative hierarchy is a good way of thinking about the large-scale behavior of well-foundedness. It's a good way of judging the strength of closure properties and consistency strength more generally. We saw this way back at the beginning of this conversation when I answered Mike's question about whether every set being in a Grothendieck universe is enough to imply replacement. But it's hard to accept the fact that it is useful if you're trying to maintain that it's a fundamentally 'artificial' way of thinking about sets, which seems to me to be Mike's position, for instance.
I feel like it's possible to make these criticisms in a more nuanced way. In Barwise's book Admissible sets and structures, Barwise also complains about most of the issues Mike brought up with regards to set theory (with the notable exception of constructivity). He primarily works with KPU, a weak, predicative set theory with urelements (that don't necessarily all live in one set). He doesn't even take the axiom of infinity as a given (which makes his life harder in places, as he points out). Near the beginning of the book he makes some pretty similar criticisms to the ones I'm talking about here.
But then he also spends the entirety of a 400+ page book working with a well-founded material set theory because it can actually be a useful way of organizing things. He uses things like transitive closures and Mostowski collapse frequently. He spends a lot of time working with ranks of sets, despite the fact that it's an 'evil' concept that isn't easily visible in the corresponding category of sets.
Obviously I can't reasonably expect people to not make off-the-cuff remarks like calling ZFC 'wacky,' but I also need to be free to criticize that kind of thing because it's often justified in really tenuous ways and because it is legitimately hostile.
Graham Manuell (Jun 27 2024 at 09:26):Yes. I also think that your counter-criticism is good. I think it has been helpful to hear your viewpoint and I am glad you chose to speak out. I guess I am a little uncomfortable with singling out specific people, but on the other hand, it is kind of necessary or criticism can get a bit vague.
I also agree that the way things are coded in a foundation is not terribly important. That being said, when using a system of mathematics, not being able to express 'nonsense' statements can also be viewed as an advantage. This is like how many people prefer strongly typed programming languages even if they need to sacrifice some expressivity. (I do concede that one is less likely to accidentally make one of these kinds of 'type errors' in mathematics than in programming, but sometimes issues of invariance under equivalence can be a little subtle, for example.)
The HoTT book is advocating for new approach to foundations. It is clearly not going to be an unbiased account. I'm not even convinced that it would be better if it were an unbiased account. If you or someone else wanted to write something on why ZFC was actually better (or equally good) at doing what HoTT is trying to do, or why ZFC is worse that those things, but better at other things, that would be very nice. But I don't think it would have been too useful to spend time in the book itself talking about the advantages of set theory.
I'm sure there are many people in the category theory community who have a misinformed impression of set theory or who are needlessly hostile to it (though I'd think it is not nearly as bad as the average mathematician outside of category theory), but I don't really think this is due to the nlab or the HoTT book or anything like that.
Ryan Wisnesky (Jun 28 2024 at 01:40):some of this discussion remains me of an old joke in computer science: for every person who wants to make invalid states non-expressible (prohibit "nonsense"), is another person that "doesn't want to give up the free real estate", i.e., who wants use the "nonsense". leading to another empirical truth in computer science, that once a system is widely used, every observable aspect of it will be depended on by someone, including the "nonsense", and this is one way how 'technical debt' arises.
John Baez (Jun 28 2024 at 09:55):Someone should do a study of technical debt in mathematics.
James E Hanson (Jun 29 2024 at 18:29):Graham Manuell said:
I guess I am a little uncomfortable with singling out specific people, but on the other hand, it is kind of necessary or criticism can get a bit vague.
I don't know how to approach this because when I talk in broad terms, people get mad at me for making sweeping statements about entire groups of people (even when I'm trying to be careful by making hedging clarifications like 'some X say Y'), but then when I talk about specific people people to try to illustrate what I think is a broader trend, people get uncomfortable like you are now and the conversation tends to get bogged down in litigating what those specific people thought.
James E Hanson (Jun 29 2024 at 18:42):Ryan Wisnesky said:
some of this discussion remains me of an old joke in computer science: for every person who wants to make invalid states non-expressible (prohibit "nonsense"), is another person that "doesn't want to give up the free real estate", i.e., who wants use the "nonsense". leading to another empirical truth in computer science, that once a system is widely used, every observable aspect of it will be depended on by someone, including the "nonsense", and this is one way how 'technical debt' arises.
I have had a type theorist literally tell me that they think set theory research is riddled with technical debt, but given the fact that the fields claiming to have more generally correct ways of doing things (i.e., structural set theory and type theory) haven't been able to easily replicate basic 86-year-old ideas from set theory research (e.g., Gödel's L), I don't feel like this is supported by anything other than a broad sense of superiority. I haven't seen a single remotely compelling argument that the kinds of things people highlight as 'junk' in set theory (e.g., $0 \in 1$, coding ordered pairs as sets, etc.) are actually junk from the point of view of the kind of metamathematics set theorists do.
Benedikt Peterseim (Jun 29 2024 at 21:03):@James E Hanson I’ve sorted out my thoughts a bit and I get the feeling that this discussion suffers at least a bit from “talking past each other”. Maybe the following distinction is useful (it has probably been made before somewhere?):
Foundations to do mathematics in: this is about the UI/UX of mathematics, about the correspondence between formalism and concepts. Does the formalism reflect well how we do mathematics in practice? How suitable is the formalism for the computer implementation of mathematics in a proof assistant? What concepts can the formalism conveniently/natively express (e.g. univalence/structuralism in HoTT, infinitesimals/differentiation in SDG, continuity principles in synthetic topology etc.)?
Foundations to study the (meta-)mathematics of: This is about the CPU of mathematics, what its powers and limitations are. How different chip architectures relate. For example, what relative consistency results can we prove between theories? E.g. independence of CH, relative consistency of “all subsets of the reals are Lebesgue measurable”, equiconsistency of Lean’s type theory with ZFC+countable many inaccessible cardinals etc. etc. What general tools and concepts can we develop to find such proofs? E.g. Gödel’s constructible universe, forcing, large cardinal axioms etc. etc.
My point is that "junk theorem arguments" are entirely about 1. and not about 2. Theorems like are not meaningful to the vast majority of mathematicians (an empirical fact!) and this is just a particularly simple example of how ZFC-as-a-formalism does not reflect mathematical practice well and deserves criticism as a foundation in the sense of 1. (and in this sense only). This says nothing about how useful ZFC is for 2. One can both agree that ZFC deserves criticism as a foundation in the first sense, and also agree that it is indispensable as a foundation in the second sense, and, for the current lack of evidence to the contrary, maybe always will be indispensable for that purpose.
James E Hanson (Jun 29 2024 at 22:24):@Benedikt Peterseim I agree that that's a good summary of my broad point although I disagree with some of the specifics.
First of all, people do use ZFC's insufficiency for 1 as evidence of its insufficiency for 2 sometimes. People sometimes imply that there's no reason why it would make sense to bother making a proof assistant fundamentally based on set theory, but the metamathematical content of 2 can feed back into 1. For instance, in a correctly designed proof assistant based on set theory, we'd know how to programmatically convert verified ZFC proofs of certain low-complexity statements into verified ZF proofs of the same statement using Shoenfield absoluteness. This is the kind of technology nobody's really bothered to implement 'natively' in type theories, and which does actually seem difficult to do cleanly in that context.
Secondly, I think there's more in common type theories that don't line up with mathematical practice than advocates of type theory seem to be willing to admit. The issue of definitional vs. propositional equality is the primary one. This is just philosophically ugly and absolutely results in headaches in actually working with these kinds of systems (cf. "dependent type hell"). The propositions-as-types philosophy, while a really beautiful idea, also isn't really how most mathematicians think. Also a fair number of specific junk theorem arguments people use in regards to 1 apply equally well to some of the stuff that goes on in type theory, as I talked about before.
Finally, I don't agree with the assertion that is not meaningful to the majority of mathematicians "as an empirical fact!" because that's the standard set-theoretic coding of , which is absolutely a meaningful fact to all mathematicians. If set theory doesn't get to use things like defined notation, then the only fair comparison would be if type theory doesn't either, but if you expand out $0<1$ into type-theoretic primitives (especially in a type theory that implements as a W-type), you get something that doesn't really immediately read as being about the natural numbers and being less than either. There's structural content there that means that it does actually mean the same thing, but I would argue that there's also structural content behind .
Jean-Baptiste Vienney (Jun 29 2024 at 22:54):I would like to say that the encoding of natural numbers as Church numerals which is in the area of proposition-as-types will not seem less esoteric to the usual mathematician than the encoding of natural numbers as sets. And no one will understand easily either Euclid's algorithm written in assembly language.
Jean-Baptiste Vienney (Jun 29 2024 at 23:00):It changes nothing to the value of being able to encode everything as sets, everything as -terms, or everything in assembly language.
Benedikt Peterseim (Jun 30 2024 at 06:39):James E Hanson said:
Benedikt Peterseim For instance, in a correctly designed proof assistant based on set theory, we'd know how to programmatically convert verified ZFC proofs of certain low-complexity statements into verified ZF proofs of the same statement using Shoenfield absoluteness. This is the kind of technology nobody's really bothered to implement 'natively' in type theories, and which does actually seem difficult to do cleanly in that context.
Interesting! It does seem mostly interesting from the point of view of pure logic, though, or what audience would you in intend such a feature in proof assistant for? I’d guess that converting proofs from ZCF to proofs in ZF wouldn’t be something that people interested in practical formalisation (like software verification, or formalising Fermat’s Last Theorem) would necessarily care about? If there are any nice applications of these techniques that would be super interesting to know about!
Benedikt Peterseim (Jun 30 2024 at 06:47):James E Hanson said:
Benedikt Peterseim Secondly, I think there's more in common type theories that don't line up with mathematical practice than advocates of type theory seem to be willing to admit. The issue of definitional vs. propositional equality is the primary one. This is just philosophically ugly and absolutely results in headaches in actually working with these kinds of systems (cf. "dependent type hell"). The propositions-as-types philosophy, while a really beautiful idea, also isn't really how most mathematicians think.
I’ve only worked with Lean (which doesn’t use plain propositions-as-types, as you probably know), and the distinction between definitional and propositional equality hasn’t really been an issue. Could you also elaborate on why you find it “just philosophically ugly”?
Benedikt Peterseim (Jun 30 2024 at 06:52):James E Hanson said:
Finally, I don't agree with the assertion that is not meaningful to the majority of mathematicians "as an empirical fact!" because that's the standard set-theoretic coding of , which is absolutely a meaningful fact to all mathematicians. If set theory doesn't get to use things like defined notation, then the only fair comparison would be if type theory doesn't either, but if you expand out $0<1$ into type-theoretic primitives (especially in a type theory that implements as a W-type), you get something that doesn't really immediately read as being about the natural numbers and being less than either. There's structural content there that means that it does actually mean the same thing, but I would argue that there's also structural content behind .
I see your point: if we use "<" as notation for , this does make meaningful to everyone if we just write it using the more familiar notation. Any proof assistant will use notations, so the really shouldn’t be considered an issue. If you put it this way, I agree.
However, the point that I got from " is junk" is a different one: it’s simply that ZFC-set theory isn’t strongly typed, while mathematical practice is, for the most part. The empirical fact I was referring to was that for most mathematicians’ brains, statements like “” or "" immediately throw a type error. Statements like this, which probably almost everyone would recognise as "nonsense" intuitively, are simply supposed to illustrate the lack of types and their importance to recognise "nonsense". It’d say that it’s pretty much consensus among programmers that having at least some support for types is extremely convenient for debugging purposes. Even lower-level languages like C do have types. Raw ZFC-based set theory doesn’t, you have no way to automatically “detect nonsense” as we seem to be able to do intuitively.
The other point of the “ argument” that I see is perhaps too obvious for you to also see: ZFC encodes everything as sets. This is not a problem in itself, but I think it’s completely reasonable to feel at odds with the ontology of “everything is a set” and hence prefer something like ECTS as a foundation-to-do-mathematics-in, for conceptual reasons. But, of course, that’s just a choice you have to make based on what you find conceptually clear.
Amar Hadzihasanovic (Jun 30 2024 at 08:05):I would just like to point out that there is a tradition in type theory of treating types not as an immutable attribute with which each object is born, but instead as something that is attributed to objects in some prior, untyped “substrate” based on their computational behaviour (it is an if it acts like an , that is, if it passes all “tests” that determine whether something is an ). The two viewpoints are called the “essentialist” and “existentialist” viewpoint in this paper by Joinet and Seiller.
From the latter point of view, “junk theorems” are certainly possible in the untyped substrate, but that can be seen as a consequence of the fact that objects can work for multiple purposes at once. I think this is reflected to a certain extent in naive mathematical practice: I do not think that a mathematician treats the natural numbers 0 and 1 with multiplication as intrinsically different objects from the Boolean 0 and 1 with AND.
Amar Hadzihasanovic (Jun 30 2024 at 08:09):Girard's programme of “transcendental syntax” makes a strong argument for the second viewpoint in the foundations of logic, as being the one that enables a “monist” foundation, which eliminates the “meta level”: the tests for programs of type are themselves programs of a dual type -- “testing” is in fact a symmetric process (programs of type are tests for type ).
From this point of view, set-theoretic foundations are “not pure enough as a foundation” not because of no typing/junk theorems/etc but because they rely on an extrinsic logical substrate.
Just wanted to point this out because it seemed, in this discussion, that the only “type theorist's critique” to set-theoretic foundations can come “from one side”.
James E Hanson (Jul 02 2024 at 01:45):Benedikt Peterseim said:
It does seem mostly interesting from the point of view of pure logic, though, or what audience would you in intend such a feature in proof assistant for?
Lots of mathematicians who aren't logicians care about choiceless proofs. Otherwise papers like this wouldn't get written.
Could you also elaborate on why you find it “just philosophically ugly”?
Madeleine already discussed this earlier in the conversation:
This has been one of my problems philosophically with most dependent type theories used today: the fact that there are two different notions of equality (judgmental equality vs identity type) and thus two different notions of subsingleton/proposition, and (at least) two notions of nearly everything else (sets, fields, n-types, etc).
The fact that you can know that is morally the same thing as without being able to literally exchange the type with the type is pretty ugly to me (especially in a type theory with UIP), and if anything Lean is a far worse offender in this regard because of its issues with things like definitional equality not being transitive (see section 3.1.1 of Mario Carneiro's thesis). (Univalence complicates this point in the context of other type theories, but you can still have terms that are equal in a unique way that fail to be definitionally equal, so this kind of philosophical ugliness is still present there too.)
However, the point that I got from "0∈1 is junk" is a different one: it’s simply that ZFC-set theory isn’t strongly typed, while mathematical practice is, for the most part.
I feel like there are some important common exceptions. A lot of mathematicians think of the primes as a literal subset of and as a literal subset of and as a literal subset of and so on, but this is impossible to implement in type theories without subtyping (and really sort of conflicts with the core philosophy of type theory). In a type theory, a prime would usually be something like an ordered pair consisting of a natural number and a proof that that natural number is prime, but go up to a mathematician on the street and ask them what the second coordinate of a prime number is.
That said, I feel like I'm already pretty familiar with the fact that mathematical practice is usually typed and the other stuff you said after this point in your response, and I feel like it's missing the point. As soon as we're using notation like and , we've already implicitly accepted the conceit that we're doing some amount of elaboration on top of the basic formal system. There's nothing in ZFC that even specifies what and mean. The von Neumann ordinal encoding is just a particular choice. (Although, as I argued earlier, I think it's a pretty reasonable choice of encoding for ordinals in particular.)
These kinds of conceptual collisions, while certainly rarer in type theory, can happen there too. If I write down two types that happen to be constructed in exactly the same way, then they are the same type. If I'm actually working in low-level MLTT, then any manually constructed finite types of the same size might actually collide. This means that I might have finite representations of and living on the same type, along with the four suites of cards and the four seasons.
A reasonable response to that point is that in an actual proof assistant, there's a certain amount of intensionality built into the user interface. The system will let you name type synonyms and might be set up to avoid those kinds of collisions. But to me this is where there's really a double standard at play. When set theory is being criticized in this way, it isn't allowed to implement any amount of vernacular or elaboration, despite the fact that even set theorists do this regularly and proof assistants like Mizar implement a fair amount of elaboration on top of set theory. The double standard is that type theory with practical elaboration and implementation of vernacular is being compared to set theory with a level of elaboration chosen by the critic specifically to make set theory look bad, rather than an earnest attempt to implement a usable system on top of it. A proof assistant based on set theory with good UX would feel a lot closer to mathematical practice than literally writing out type-theoretic proofs in natural deduction.
Even lower-level languages like C do have types.
Sure but x86 and ARM don't have types because there are contexts in which the added complexity of having a type system actually interferes with other goals (such as physically building a machine that correctly implements the language on bare metal), and as I argued earlier in this conversation I actually think that having a really low-level proof assistant kernel, such as one based on set theory, might make sense even for practical use (as opposed to just metamathematics) from the perspective of trust. Type theory has an objectively worse track record than set theory with inconsistency. Coq and Lean have both added things to their kernels that ended up being inconsistent and Agda is currently suspected to be inconsistent.
Benedikt Peterseim (Jul 02 2024 at 06:27):James E Hanson said:
Benedikt Peterseim said:
However, the point that I got from "0∈1 is junk" is a different one: it’s simply that ZFC-set theory isn’t strongly typed, while mathematical practice is, for the most part.
I feel like there are some important common exceptions. A lot of mathematicians think of the primes as a literal subset of and as a literal subset of and as a literal subset of and so on, but this is impossible to implement in type theories without subtyping (and really sort of conflicts with the core philosophy of type theory). In a type theory, a prime would usually be something like an ordered pair consisting of a natural number and a proof that that natural number is prime, but go up to a mathematician on the street and ask them what the second coordinate of a prime number is.
That said, I feel like I'm already pretty familiar with the fact that mathematical practice is usually typed and the other stuff you said after this point in your response, and I feel like it's missing the point. As soon as we're using notation like and , we've already implicitly accepted the conceit that we're doing some amount of elaboration on top of the basic formal system. There's nothing in ZFC that even specifies what and mean. The von Neumann ordinal encoding is just a particular choice. (Although, as I argued earlier, I think it's a pretty reasonable choice of encoding for ordinals in particular.)
These kinds of conceptual collisions, while certainly rarer in type theory, can happen there too. If I write down two types that happen to be constructed in exactly the same way, then they are the same type. If I'm actually working in low-level MLTT, then any manually constructed finite types of the same size might actually collide. This means that I might have finite representations of and living on the same type, along with the four suites of cards and the four seasons.
A reasonable response to that point is that in an actual proof assistant, there's a certain amount of intensionality built into the user interface. The system will let you name type synonyms and might be set up to avoid those kinds of collisions. But to me this is where there's really a double standard at play. When set theory is being criticized in this way, it isn't allowed to implement any amount of vernacular or elaboration, despite the fact that even set theorists do this regularly and proof assistants like Mizar implement a fair amount of elaboration on top of set theory. The double standard is that type theory with practical elaboration and implementation of vernacular is being compared to set theory with a level of elaboration chosen by the critic specifically to make set theory look bad, rather than an earnest attempt to implement a usable system on top of it. A proof assistant based on set theory with good UX would feel a lot closer to mathematical practice than literally writing out type-theoretic proofs in natural deduction.
Sure, I don’t think I really disagree with anything you write here. All I wanted to point out earlier was that the “junk theorem arguments” about ZFC are not completely invalid in every context. They do have a point, and it’s about the conceptual content of foundations. The fact that everything is a set in ZFC, with “everything” forming the cumulative hierarchy, is the conceptual content that informs the axioms of ZFC. An argument that points out a discrepancy between this concept of a set and the structuralist one should be allowed. I’m just writing this because you seem to argue that it’s a bad (even bad-faith) argument, always, in any context, as a result of “double standards”. One can also make such “junk theorem” arguments about type theory, of course, like your example of a prime number being a pair of a natural number and a proof that it’s prime. This clarifies conceptually how type theory treats what would be just “subsets” in mathematical English. These are a simple but fair points both ways, illustrating the conceptual differences between different foundations. Everyone can then decide for themselves which concept of a set/type/etc. they prefer to think about. (E.g. I personally tend to think of bare sets as “discrete spaces” up to bijection, and not as sets of sets of sets ….) I’m most probably still not telling you anything new here, I’m sorry for that, but I do hope that clarifies what I wanted to say earlier.
James E Hanson (Jul 02 2024 at 07:37):@Benedikt Peterseim I don't think that junk theorem arguments about ZFC are invalid in every context; I just think that when is really overstated as an example. The HoTT book itself even uses the notation for the type of Booleans, so clearly there's something at least a little conceptually reasonable about thinking of "" as an "element" of "".
In any case, while I do think that a lot of the discourse contrasting type theory with set theory implicitly involves double standards, I don't think it's usually in bad faith. I shouldn't have used that phrase earlier in this discussion, and I should have been more careful with my phrasing here. For that I'd like to apologize.