Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Gödel's L

Spencer Breiner (Jul 08 2024 at 19:14):

After seeing numerous comments in other threads, I'm hoping someone can help me understand the obstacles to a categorical/structural approach to the constructible universe. Naively, this looks somewhat similar to the construction of an initial model as a trans-finite induction. Is the problem that this sequence never "converges", leading to tricky size issues?

dusko (Jul 08 2024 at 21:46):

the constructible universe is the effective version of von Neumann's cumulative universe. and von Neumann's cumulative universe is the initial algebra for the powerset functor. that is the primordial example that took us up to another universe.

that is, btw, why lawvere was claiming that, in contrast with the finite arithmetic of the NNO as an initial algebra, there was no categorical account of arithmetic universes and transfinite arithmetic. then joyal came up with algebraic set theory as a categorical theory of arithmetic universes...

there should also be constructible universes inside the constructive universes. in a realizability topos one could i think effectively enumerate all predicates and just write down the usual construction in the internal language.

David Michael Roberts (Jul 08 2024 at 23:36):

It's not size issues at all, since algebraic set theory can deal with that stuff perfectly well, and can talk about $V$ as a single object.

It's figuring out how to build something like $\mathrm{Def}(X)\subseteq P(X)$ as in https://en.wikipedia.org/wiki/Constructible_universe#What_L_is , but in a structural way.

As usually defined, this absolutely is talking about subsets of X that are definable in the language that involves $\in$. The parameters $z_i$ are not an issue, just being able to access those subsets carved out by first-order formulas (with bounded quantifiers) _in the language of ZF_ seems to be really hard, when starting from a structural set theory.

Todd Trimble (Jul 08 2024 at 23:53):

and von Neumann's cumulative universe is the initial algebra for the powerset functor.

Obviously not literally, because Lambek's theorem on initial algebras (the algebra structure of the initial algebra of an endofunctor is an isomorphism) together with Cantor's theorem guarantees this is impossible.

that is, btw, why lawvere was claiming that, in contrast with the finite arithmetic of the NNO as an initial algebra, there was no categorical account of arithmetic universes and transfinite arithmetic. then joyal came up with algebraic set theory as a categorical theory of arithmetic universes...

Let's say Joyal and Moerdijk. Actually Lawvere was plainly allergic to the research program of giving a categorical account of the cumulative hierarchy; it was anathema to him.

there should also be constructible universes inside the constructive universes. in a realizability topos one could i think effectively enumerate all predicates and just write down the usual construction in the internal language.

I also believe this should be possible, and conjecture you wouldn't need to go all the way to realizability toposes.

dusko (Jul 09 2024 at 06:31):

Spencer Breiner said:

[...] understand the obstacles to a categorical/structural approach to the constructible universe [...]

so cycling up this hill, i started wondering what might be the obstacles to constructing the constructible universe as a category. the objects are goedel's definable sets, and the morphisms are the definable functions. it is an honest category, eg by the makkai-reyes' coherent logics.

now i am not asking this out of a duty to plant a category in every park, but if goedel construed his definable sets as effectively constructible, and the constructible universe is constructed in a constructive universe, then all of the constructive universe should be effectively constructible. do we get that if we add the constructible functions to constructible sets? well if the constructive universe is a topos (eg realizability), then the answer is no. the constructible universe as a category is not a topos because it obviously does not have the effective quotients. we could process it through a tripos, but then the constructible functions would be identified not up to the logical equivalence of the defining predicates, but extensionally, up to the definable equivalences modulo the logical equivalence :(

but if we, so to say, apply goedel on goedel, and assume that the language is enumerated and each definable predicate is characterized by a computable function, then the definable functions are also computable --- and i think the category of all constructible sets is the constructive universe without the extensional collapse: a monoidal computer. if the theory indices are well-ordered, then even a program-closed category... which is "morally" what it should be if we take goedel's choice of words seriously. (the memories of the brouwer-hilbert battle were fresh and the word "construction" had a very distinct meaning.)

i did NOT check any this and may be hallucinating (having spent most of the day in the company of LLMs)... but i would bet some small money that it is true :)

James E Hanson (Jul 11 2024 at 18:02):

dusko said:

well if the constructive universe is a topos (eg realizability), then the answer is no. the constructible universe as a category is not a topos because it obviously does not have the effective quotients.

@dusko Maybe I'm not understanding what you're describing, but how is this obvious? The constructive version of L that's been studied by constructive set theorists does produce a topos if the background theory is strong enough (like IZF with collection). In particular L relative to the effective topos should be a topos. Moreover it should be relatively straightforward (although not entirely pleasant) to perform this construction starting from the effective topos as a category (rather than in terms of the corresponding model of IZF).

David Michael Roberts (Jul 11 2024 at 22:47):

James E Hanson said:

it should be relatively straightforward (although not entirely pleasant) to perform this construction starting from the effective topos as a category

Isn't the whole point of this discussion that we don't currently know how to do this?

David Michael Roberts (Jul 11 2024 at 23:15):

@dusko if the constructible universe is a model of ZFC, then the sets and the functions in the constructible universe should give an elementary topos, no? Unless this is about working from an intuitionistic base set theory, say IZF, and then the constructible universe doesn't give back a model of IZF? I defer to James' expertise on that one.

Ryan Wisnesky (Jul 11 2024 at 23:26):

fwiw, my own obstacle to a categorical understanding of L is that L talks about "all first order formulas" as part of "Def", and moreover, zfc axiom schemes such as replacement also refer to "all first order formulas". Whereas the Von Neumann universe V (iterated power sets of "all sets") is easy to describe without appeal to syntax, and so easier to handle categorically. What would help my own understanding is, what happens if you change Def to be something other than all first order formulas, where would the categorical construction of L break down? Suppose Def was "all first order formulas of size < 30", what would happen in the categorical definitions? I can't work out the details on my own, despite an intuition that there should be some categorical model of L that is somehow syntax independent which could be used to answer these questions.

David Michael Roberts (Jul 11 2024 at 23:36):

It's not just "all first order formulas", but the fact they are in the language including $\in$. The theory of a well-pointed (boolean) topos is a first-order theory and one can write down first-order formulas in a language for that, but it's not helpful.

James E Hanson (Jul 12 2024 at 03:49):

Ryan Wisnesky said:

fwiw, my own obstacle to a categorical understanding of L is that L talks about "all first order formulas" as part of "Def", and moreover, zfc axiom schemes such as replacement also refer to "all first order formulas". Whereas the Von Neumann universe V (iterated power sets of "all sets") is easy to describe without appeal to syntax, and so easier to handle categorically. What would help my own understanding is, what happens if you change Def to be something other than all first order formulas, where would the categorical construction of L break down? Suppose Def was "all first order formulas of size < 30", what would happen in the categorical definitions? I can't work out the details on my own, despite an intuition that there should be some categorical model of L that is somehow syntax independent which could be used to answer these questions.

If you look at Matthews and Rathjen's paper, you can see that it's possible to define L in terms of a relatively small number of 'fundamental' or 'rudimentary' operations (and this was how Gödel originally defined L). They're able to do this in a constructive context using 13 specific binary functions. It's possible to then define a hierarchy generating L using this directly:

• $L_\alpha$ is the closure of $L_{<\alpha} \cup \{L_{<\alpha}\}$ under the basic operations.
• $L_{<\alpha} = \bigcup_{\beta < \alpha}L_\beta$.
• $L = \bigcup_{\alpha \in \mathrm{Ord}} L_\alpha$.
  (They don't precisely use this definition because they don't want to assume the axiom of infinity, so they can't just take closures of sets.)

James E Hanson (Jul 12 2024 at 04:01):

David Michael Roberts said:

Unless this is about working from an intuitionistic base set theory, say IZF, and then the constructible universe doesn't give back a model of IZF? I defer to James' expertise on that one.

There is a constructive definition of L. Lubarsky originally showed that in IZF with collection, L is provably a model of IZF + collection + V=L. Matthews and Rathjen worked out a fair amount of the behavior of L in weaker constructive set theories. Specifically they showed that IKP (intuitionistic Kripke-Platek set theory) proves that IKP holds in L.

James E Hanson (Jul 12 2024 at 04:33):

David Michael Roberts said:

Isn't the whole point of this discussion that we don't currently know how to do this?

I think something like this would (partially) work: Start with the definition of $V(\mathrm{Set})$ in terms of 'extensional well-founded APGs' from Mike's paper. In a topos you should actually be able to identify extensional well-founded APGs that 'look like $L_\alpha$ for an ordinal $\alpha$ using the definition I sketched above. Then you should be able to show that for any ordinals $\alpha$ and $\beta$ with $\alpha \leq \beta$, an APG that looks like $L_\alpha$ is isomorphic to an initial segment of an APG that looks like $L_\beta$. (I should note that this is roughly similar to Mathias's 'somewhat structural' construction of L in Mac Lane set theory without choice in terms of 'L-strings'.)

This should be enough to define pieces of the 'category of L sets' internally. I'm a little hazy on when you would then be able to actually get a category externally, but I would bet that constructive well-pointedness would be enough.

That said I'm not completely sure the resulting thing would always even be cartesian closed when the topos isn't Boolean. The proof of power set in L in constructive set theories seems to rely in an essential way on a collection axiom. You don't need this classically because you can lean on always being able to find 'the least ordinal such that...' Moreover, even if you don't have replacement, you can use the condensation lemma to show that L satisfies power set. (Mathias uses condensation frequently in his paper to make up for the lack of replacement.) I think that some weak version of the condensation lemma is probably constructively provable if you have the right kind of choice (specifically enough choice to prove a 'constructively reasonable' version of the downward Löwenheim–Skolem theorem), and so with this amount of choice you might be able to show that the resulting category is a topos even if your original topos was not Boolean.

James E Hanson (Jul 12 2024 at 04:43):

Also, the existence of exponentials doesn't really seem fundamentally easier in this context, despite the fact that it's often weaker than power set constructively.

David Michael Roberts (Jul 12 2024 at 07:54):

But building a model of material set theory and then extracting its L is not the goal. Perhaps something can be learned from this, but it's not clear what. I agree that Gödel operations are a good place to look, but they are really entangled with the material nature of ZF etc sets, and one would have to do a bit of work to extract structural versions, if at all. One should really look for things that work on functions, not sets, I suspect.

James E Hanson (Jul 12 2024 at 18:09):

David Michael Roberts said:

But building a model of material set theory and then extracting its L is not the goal. Perhaps something can be learned from this, but it's not clear what. I agree that Gödel operations are a good place to look, but they are really entangled with the material nature of ZF etc sets, and one would have to do a bit of work to extract structural versions, if at all. One should really look for things that work on functions, not sets, I suspect.

One of my problem with this enterprise is that I'm not sure what people would really find satisfying. Can you actually state the goal in a precise way?

It should possible to write down a more 'explicitly structural' construction in something like ETCS, but what I'm envisioning is still going to involve carefully assembling everything by transfinite recursion and having a global 'addressing structure' that resembles the cumulative hierarchy on some level. This addressing structure is going to be somewhat intrinsically 'evil' in that it will involve strict notions.

Here's a rough sketch of the idea (written in 'naive' classical structural set theory):

Given a small (not necessarily full) subcategory $C$ of Set, an address book for $C$ is a pair of sets $O$ and $H$ with bijections $\ulcorner\cdot\urcorner : \mathrm{ob}(C) \to O$ and $\ulcorner\cdot\urcorner : \mathrm{hom}(C) \to H$ along with partial maps encoding sources and targets of morphisms, identity morphisms, and compositions of morphisms, as well as fixed choices of finite products, coproducts, equalizers, and coequalizers.

Given a triple $(C_\alpha,O_\alpha,H_\alpha)$ as above, we need to define a 'successor' $(C_{\alpha+1},O_{\alpha+1},H_{\alpha+1})$. The intuitive idea is that we add $O_\alpha$, $H_\alpha$, and $\bigoplus_{a \in O_{\alpha}} \ulcorner a \urcorner$ and then also add in the appropriate maps and then generate the category $C_{\alpha+1}$ and the new address book $(O_{\alpha+1},H_{\alpha+1})$ as freely as possible (while only using finitary limits and colimits). We also need to add in new morphisms whenever we see functional relations on cartesian products. Then at limit stages we take the direct colimit of everything.

If you start with $C_0$ being the category consisting of just an empty set and then iterate, you should get something equivalent to the category of sets in L. (Incidentally, this picture does make the generalization to L over a structure immediate; you just take $C_0$ to be the category of definable sets with definable maps in the structure.)

The key is that we're avoiding operations that aren't set-theoretically absolute or in other words aren't fully predicative. Finite limits and colimits are all absolute, but things like power sets and exponentials aren't. The only infinitary operation we're explicitly allowed to do is the coproduct in the successor and the direct colimit at limit ordinals. Everything else needs to be built from those using the given finitary operations.

dusko (Sep 10 2024 at 20:40):

James E Hanson said:

dusko said:

well if the constructive universe is a topos (eg realizability), then the answer is no. the constructible universe as a category is not a topos because it obviously does not have the effective quotients.

dusko Maybe I'm not understanding what you're describing, but how is this obvious? The constructive version of L that's been studied by constructive set theorists does produce a topos if the background theory is strong enough (like IZF with collection). In particular L relative to the effective topos should be a topos. Moreover it should be relatively straightforward (although not entirely pleasant) to perform this construction starting from the effective topos as a category (rather than in terms of the corresponding model of IZF).

the ZF and IZF models define what is a type (set) in our universe. to get a topos, we take as morphisms the effective total single-valued equivalence relations. in the constructive universe where we live as programmers, we take computable functions as morphisms. the quotients in that universe would only be effective if the equivalence relations induced by computable functions were decidable. then the construction of realizability topos could stop at assemblies and wouldn't have to go throubh the extensional collapse.

SORRY that i am coming so late to this. i got stuck on a problem in the summer and stayed away from eveerything. honestly sorry.

James E Hanson (Sep 10 2024 at 21:43):

@dusko I can't tell whether you're actually talking about $L$ as it is typically defined in (constructive) set theory or something else entirely. Could you give a precise definition of 'the constructible universe' or 'the constructive universe'?

dusko (Sep 10 2024 at 22:12):

James E Hanson said:

dusko I can't tell whether you're actually talking about $L$ as it is typically defined in (constructive) set theory or something else entirely. Could you give a precise definition of 'the constructible universe' or 'the constructive universe'?

constructible universe and constructive universes are very different things.

the constructible universe $L$ is Goedel's version of von Neumann's cumulative hierarchy, restricted to the subsets constructible by comprehending the definable predicates.

constructive universe is the universe of constructive logic. Brouwer defined it in terms of spreads, but already Heyting and Kolmogorov defined it in terms of types --- and constructive functions. nowadays all people who write programs live in constructive universes.

in the times when still very few people wrote programs, some great logicians tried to define constructive universes as constructible universes without the excluded middle. the words seemed to suggest that it could be done. the obstacle was that executing the inductive definition of the cumulative hierarchy while avoiding the logical principles that imply the excluded middle required a lot of theology, which deterred many logicians who preferred constructing stuff to splitting hairs.

that is how i experienced the difference (as a student of students of Arend Heyting and Bertus Brouwer).

dusko (Sep 10 2024 at 22:22):

the precise definitions of mathematical constructions, i am sure you will agree, are not really suitable for chat groups, unless people want to argue that their colocutors don't know what they are talking about. nowadays i omit even the explicit references since most people (or at least those of us who still who still try to be students) love to find them in collaboration with AIs.

John Baez (Sep 10 2024 at 22:31):

The title of this thread is "Goedel's L", and it began as a discussion of whether Goedel's constructible unverse L can be defined and studied in topos theory. So I can understand why @James E Hanson is asking what's going on now. Earlier in this thread, Dusko said L is not a topos because it obviously doesn't have effective quotients, and James expressed doubt about that claim. Did you two ever come to agreement on that?

dusko (Sep 11 2024 at 01:03):

if i remember correctly, the question was whether $L$ could be constructed internally in toposes and i first remembered that this was lawvere's "NNO but no L" claim, and joyal's "L using open maps".

i may have caused confusion because then it occurred to me that $L$ could be executed in an intentional constructive universe, say of computably enumerable types and computable functions given by any programming language we like. (i guess people who work with realizability toposes would recognize this as the category of enumerations, or assemblies. but outside of the realm of our expertise, this really is the world where all these computations around us live, not only in our phones and computers, but also in our cells and viruses.) so it is like a realizability topos before the extensional collapse is inflicted upon it. well that is not a topos because a computable surjection is not necessarily a coequalizer of its kernel. the kernel is computable, but not decidable.

sorry for sowing confusion.

(or to be completely honest, i think the confusion originates from imagining that constructivism is this poor man's version of hilbertian math, just without the excluded middle --- which i love and respect, but it is different from the constructivist world in which each of us has been living ever since we wrote our first programs.)

James E Hanson (Sep 11 2024 at 01:14):

John Baez said:

Did you two ever come to agreement on that?

No. Classical $L$ is a topos because it's a model of $\mathsf{ZFC}$. Constructive $L$ in $\mathsf{IZF}$ (under the existing definition) is similarly a model of $\mathsf{IZF}$ and therefore a topos (modulo some specifics of your choice of semantics for $\mathsf{IZF}$). $L$ is known to possibly fail to satisfy the exponentiation axiom in $\mathsf{CZF}_{\mathcal{P}}$ (see Theorem 7.12 here), which probably makes it not even cartesian-closed. I believe that models of $\mathsf{CZF}_{\mathcal{P}}$ are always toposes, so it would seem that the normal construction of $L$ can't be internalized into arbitrary toposes in a way that produces toposes.

That said, quotients are not really the operant issue here. I believe that Matthews and Rathjen's results establish that $L$ in $\mathsf{CZF}$ does in fact have quotients. They show that $L$ in $\mathsf{IKP}$ satisfies $\mathsf{IKP}$, and $\mathsf{IKP}$ is strong enough to build quotients. Since $\mathsf{CZF}$ contains $\mathsf{IKP}$, this means that $\mathsf{CZF}$ (and therefore type theories like $\mathsf{MLTT}$ which can interpret $\mathsf{CZF}$) is strong enough to show that $L$ has quotients.

Moreover, it should be noted that assuming a base theory of $\mathsf{ZF}$ (or just $\mathsf{IZF}$), it should be possible to actually build a topos $L$ inside the realizability topos.

James E Hanson (Sep 11 2024 at 01:16):

dusko said:

the precise definitions of mathematical constructions, i am sure you will agree, are not really suitable for chat groups, unless people want to argue that their colocutors don't know what they are talking about. nowadays i omit even the explicit references since most people (or at least those of us who still who still try to be students) love to find them in collaboration with AIs.

This is not really how academic conversations are supposed to work. When I can't fit a definition into some online communication medium, I find a reference and point to it. Would you be able to provide references in this case?

James E Hanson (Sep 11 2024 at 01:18):

dusko said:

i first remembered that this was lawvere's "NNO but no L" claim, and joyal's "L using open maps".

What are these claims that you're talking about? Are they written down somewhere? Failing that can you describe them in more detail?

I ask because I actually spent a little bit of time looking for comments made by Lawvere about Gödel's $L$ in particular, and I was only able to find a couple of fairly minor references.

David Michael Roberts (Sep 11 2024 at 02:44):

I'd be perfectly happy to have that in general, L for a general topos is merely an infinitary pretopos as subcategory (or something like a locally internal category over the topos).

David Michael Roberts (Sep 11 2024 at 02:57):

In fact, I strongly think that L really should be defined as an locally internal category, not an abstract category, and it certainly can't be an internal category.

James E Hanson (Sep 11 2024 at 07:42):

@David Michael Roberts Yeah, locally internal categories seem like the right approach to me.

David Michael Roberts (Sep 11 2024 at 07:47):

So something like "a topos L inside the realisability topos" is a bit of a misnomer, but I understand what you were meaning

David Michael Roberts (Sep 11 2024 at 07:49):

All that aside, does L in a CZF_P model satisfy any of the nice properties (or analogues thereof) of L inside a ZFC model? EG, does it have any shadow of GCH? It feels antithetical to ask if it satisfies AC.... :upside_down:

David Michael Roberts (Sep 11 2024 at 07:54):

Maybe DC indexed by arbitrary ordinals? Just making a random guess, that seems quite strong

David Michael Roberts (Sep 11 2024 at 07:55):

In a classical theory that implies AC, it seems, but I don't know about in CFZ_P

dusko (Sep 11 2024 at 08:02):

James E Hanson said:

dusko said:

the precise definitions of mathematical constructions, i am sure you will agree, are not really suitable for chat groups, unless people want to argue that their colocutors don't know what they are talking about. nowadays i omit even the explicit references since most people (or at least those of us who still who still try to be students) love to find them in collaboration with AIs.

This is not really how academic conversations are supposed to work. When I can't fit a definition into some online communication medium, I find a reference and point to it. Would you be able to provide references in this case?

hmm. would i be able to? well i might be able, but you will miss the fun of finding them yourself. you can find the history of constructive universes in troelstra-van dalen's book, and their categorical structure in my Programs as Diagrams.

but since i don't belong to the part of the society that considers "academic conversations" to be something desirable and follows how things are "supposed to work", this time i will check out of this conversation intentionally, with all the best wishes for your academic work.

David Michael Roberts (Sep 11 2024 at 08:05):

Well, one could always write academic papers and give no references, and tell readers to find out the source of claims themselves, but that is not exactly helpful ^_^

Kevin Carlson (Sep 11 2024 at 15:34):

What a pointless waste of everybody’s time.

James E Hanson (Sep 11 2024 at 17:32):

David Michael Roberts said:

All that aside, does L in a CZF_P model satisfy any of the nice properties (or analogues thereof) of L inside a ZFC model? EG, does it have any shadow of GCH? It feels antithetical to ask if it satisfies AC.... :upside_down:

This is getting pretty close to topics I'm currently considering writing a paper about, but the general picture is that we don't know very much about how $L$ behaves in constructive contexts. It's open whether $\mathsf{IZF} + \neg \mathsf{LEM}$ proves $V = L$, for instance. One thing I've been looking at is whether there's other definitions one might try. I believe I have a definition that would give non-trivial inner models in some anti-classical contexts (such as sheaf toposes over $\mathsf{ZF}$), but it's still a bit preliminary to talk about. The idea though is just that the normal construction is indexed by arbitrary ordinals, but it makes sense to restrict to more special classes of ordinals, such as the plump ordinals, and this gives an analogously more restricted construction.

David Michael Roberts said:

Maybe DC indexed by arbitrary ordinals? Just making a random guess, that seems quite strong

I spent a little bit of time thinking about something like this version of choice in constructive contexts, but I wasn't able to make any real progress with understanding it. There's some subtlety with how you define it, of course. Ordinary DC fails in a lot of sheaf toposes, but there's a weak version of Zorn's lemma that holds in any sheaf topos over $\mathsf{ZFC}$. (I believe this is mentioned in the Elephant.) This version of Zorn's lemma should give you a weak form of DC, specifically the existence of paths in trees of height $\omega$ that cannot be properly extended (as opposed to paths actually indexed by $\omega$, which is what DC gives you). Moreover, it should also given you analogous weak DC for taller trees.

David Michael Roberts (Sep 12 2024 at 06:09):

Though, now I think about it, better than AC or variants would be something relating to ordinals (or whatever appropriate kind) or Zorn, as you say.

James Deikun (Sep 12 2024 at 16:18):

$L$ and $L(X)$ have an alternate description as "the smallest model containing all the ordinals" and "the smallest model containing all the ordinals and $X$" which seems like it would generalize better to the structural world than the version using formulas. I wonder why people don't seem to use that? (The parameter for $L(-)$ in a "native" structural sense would need to be more than a single set, but that seems like it could still be worked with.) The really troublesome one would seem to be $L\lbrack-\rbrack$ which is used when constructing sharps.

James E Hanson (Sep 12 2024 at 18:39):

@James Deikun One issue with this approach is that it isn't as robust as one might like. Blass gave an example showing that there can be a countable set of real numbers $A$ such that there is no minimal model $M$ of $\mathsf{ZF}$ with $A \subseteq M$. (Moreover, the axiom that ends up failing in the intersection of all transitive models $M \supseteq A$ is power set, so the 'hull' of $A$ isn't even a topos.) The normal $L$ construction gives you the minimal transitive model $M$ with $A \in M$.

dusko (Sep 13 2024 at 18:47):

David Michael Roberts said:

Well, one could always write academic papers and give no references, and tell readers to find out the source of claims themselves, but that is not exactly helpful ^_^

the only reason i keep coming here is that the main energy that still keeps driving me is to try to be helpful to young people, because we are leaving them such a crappy world. i have no major risks or ambitions to attent to. just the students.

now for "academic conversations" , "academic papers", and references --- the point is that literature research cannot be the same when we have dynamic concept indices trained on most of the the whole web --- including eg the SciHub. i have been teaching grad courses where the students seek out the references themselves since 2021, in 3 countries, and people not only learn more that way, but also often dig up interesting new references.

the autopilot of standardized references is a remnant from last century. in the 1990s, there was the question whether we would standardize the data structures on the web ---the idea of Semantic Web--- or crawl it and somehow mine for concepts --- the idea of Search Engines. the Semantic Web died, and crawling the web made it possible to build the Large Language Models of mind. an alien spaceship behind the moon can download the web, train an LLM and speak to us, without really knowing what. it will be well informed about all of our references. the idea of DOIs and the autopilot of listing references seems, on the other hand, like a remnant of the idea of Semantic Web. and of the XIII century Sorbonne, where people were competing who will know more references.

most importantly, the idea of science as reading and writing academic papers has departed from Francis Bacon's idea of science as interaction with nature, back to the Sorbonne idea of knowing God by winning arguments about books.

there seem to be two perpendicular dimensions of science:

• science as interaction with nature and
• science as a social process.

mathematics subsumes under that. scientists try to disprove hypotheses and build better theories. mathematicians do just that: try if the obvious idea works, and find something interesting when it doesn't. lawvere would say: they explore the nature of concepts. goedel would say: they explore the nature of logic. or Logos.

your and my problem is that the two perpendicular dimensions of science draw from the same source of energy. the more energy we spend on drilling into a problem, the less energy we have left for dealing with the politics of publishing our solution. pushing along the social dimension of science, manoevring your way through an academic career, pulls you away from the confrontation with nature.

it is, of course, arguable, that "together we can do more". but if you are old enough to look back at your academic career, all the peer reviews that you wrote and receivd, all departmental meetings where you fought to avoid teaching calculus I... most academics i know agree that the academic life did not bring them closer to research of nature, but away from it.

dusko (Sep 13 2024 at 18:59):

most universities are run by people who became academics not because they really wanted to give life for science, but because they were reluctant to leave school. so after they graduated they became graduate students, and after they became doctors they became professors. and then as professors, they were the first one to give up on research and become academic politicians. so you get the worst of both worlds: scientists who are not really interested to understand nature, but to dominate the social process, that happens to have something to do with science; and managers and politicians of academia, who never studied to be managers or politicians, which often shows.

and then there are research communities, which also regularly evolve into politics, waving membership cards ("we should promote category theory" is logically not all that different from "we should promote family values" or some other great value, is it?)

so yes, @Kevin Carlson, there is a lot of time wasting, which could be spent on science but is spent on swipes and resentment towards people you never met.

i periodically get desperate when people come to talk about science and end up wasting time on proving that they are smart. this shouldn't be about you and me. we come and go. it should be about understanding the world. that is the one thing that we can share. not social strategies. that is the thing that separates us.

i genuinely love you all, but i keep realizing that don't belong here. and then changing my mind because you ask a question we asked in the 80s. BUT in spite of everyone maintaining all the references, the solutions got forgotten and are sought again. because people do not use references to understand. people read papers to enable writing their own papers. the goal of most academics conversations is not to learn ideas, but to build academic careers. all involved end up unhappy.

Madeleine Birchfield (Sep 13 2024 at 19:07):

I disagree that mathematics subsumes under science. Science requires the scientific method, developing and performing experiments and/or quantitative observations of the real world, and the scientific method is absent in mathematics, which rather deals with mathematical structures and logical proofs.

So your critiques of the state of science of academia, while in my view correct about science, just do not apply here in mathematics.

Madeleine Birchfield (Sep 13 2024 at 19:12):

lawvere would say: they explore the nature of concepts. goedel would say: they explore the nature of logic. or Logos.

And I would say that this is philosophy, which encompasses both science and mathematics, the latter of which are separate sub-branches of philosophy.

dusko (Sep 13 2024 at 19:17):

Madeleine Birchfield said:

I disagree that mathematics subsumes under science. Science requires the scientific method, developing and performing experiments and/or quantitative observations of the real world, and the scientific method is absent in mathematics, which rather deals with mathematical structures and logical proofs.

So your critiques of the state of science of academia, while in my view correct about science, just do not apply here in mathematics.

it is not a matter of agreement and disagreement. for some projection of reality you are right, and if i am honest i am saying something that exists in reality.

mathematics is empiric in the sense that it is interaction with external memory. neither you and i nor an LLM can multiply pairs of 5-digit numbers without the external memory. so you go out of the internal states of your head and try out algorithms. your lab is a piece of paper, or whatever else you use.

the crucial point is that, just like in a lab, your math research is inductive inference. you have a hypothesis, and you push it through on a piece of paper until you make a significant observation and disprove your hypothesis. then you try to improve it. in the end you have overcome the limitations of your original intuition, and bulit something that did not come from your head, but from interaction with your paper lab.

kolmogorov wrote about that.

dusko (Sep 13 2024 at 19:19):

:heart: :working_on_it: :heart:

James E Hanson (Sep 13 2024 at 19:32):

@dusko If you want to be helpful, could you please elaborate on this offhand comment you made?

if i remember correctly, the question was whether L could be constructed internally in toposes and i first remembered that this was lawvere's "NNO but no L" claim, and joyal's "L using open maps".

I have looked for references regarding these comments by Lawvere and Joyal, and I have even consulted an LLM as you suggested, but I am not finding anything. Are these referring to something written or to verbal statements that you personally witnessed?

Madeleine Birchfield (Sep 13 2024 at 19:33):

dusko said:

the crucial point is that, just like in a lab, your math research is inductive inference. you have a hypothesis, and you push it through on a piece of paper until you make a significant observation and disprove your hypothesis. then you try to improve it. in the end you have overcome the limitations of your original intuition, and bulit something that did not come from your head, but from interaction with your paper lab.

This is still significantly different from science. In science, you can't ever prove or disprove a hypothesis, in the same way that you can logically prove or disprove a mathematical conjecture assuming certain axioms. You can only say in science that this hypothesis agrees or disagrees with experimental evidence up to some $\sigma$ or confidence level, and while that level can increase or decrease, it can never go to infinity.