I think nobody ever discussed how to organize mathematics properly, in formalizations. People use trees to organize things, but clearly this doesn't work. But people pretend it does.
Conversation
Some of us having been talking about that for over a decade... but publishing mostly at CICM, which seems to be a mistake, because it doesn't reach the audience that needs to hear it.
2
3
what are good references?
1
It's always good to start with the historical work - de Bruijn wrote nice papers on organization wrt Automath in multiple papers in the late 60s and early 70s, available in the collected Automath papers. Understanding the CS message of Universal Algebra is also useful.
1
3
I ought to collect the "oh my, did we ever get this wrong" papers in one place - there are some from both the Mizar and the Axiom folks about how their ideas didn't scale to big libraries.
1
2
The next thread to dig into isn't from people doing math systems in particular, but trying to do 'organization' in general. Here you find ground-breaking work by Burstall and Goguen (CLEAR, OBJ, all progenitors of CASL), Doug Smith (et al)'s work on SpecWare,
1
2
Kapur, Musser and Stepanov (before the STL) on Tecton (stepanovpapers.com/Tecton.pdf) are all really worth reading. [And will make you weep for how poor our current languages still are 40 years later.]
1
2
I first talked about using "tiny theories" as a means to organize a library in the context of an experimental library (cas.mcmaster.ca/~carette/publi) described in 2011. Proper theoretical description led to "theory presentation combinators" cas.mcmaster.ca/~carette/publi
1
2
Before that, Bill and I wrote about the different use cases of collections of theories, and the different solutions that these might have in "High Level Theories" cas.mcmaster.ca/~carette/publi. I'll note that Locales (v2) in Isabelle were influenced by this.
1
2
There's more, but I don't know how many papers of mine you really want to read 🤣🤔
1
Thanks for the reminder about these papers - would love to this stuff collected together somewhere. Perhaps like the 'effects-bibliography'? This stuff excites me so much… more from a software perspective than a mathematics perspective – but I love how much these things overlap.
Collecting this stuff is a good idea. Not sure if effects-bibliography is appropriate. But some kind of online 'review' paper could work.
1