TIL that "junk theorems" are a thing in mathematics. Not being a mathematician myself, I found this [1] article a useful primer.
[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...
This is very interesting. What happens if you keep pulling the thread and construct large theories on such abstraction-layer-breaking theorems? Would we arrive at interesting things like pulling the thread on sqrt(-1) for imaginary numbers? Or is it somehow “undefined behavior”, quirks of the various implementation substrates of abstract mathematics that should be (informally) ignored? My gut says the former.
Are the various alternative axiomatic foundations also equivalent at this level or not? I suppose they are since they can implement/emulate each other, not sure.
Maybe I'm too familiar with the set theoretic construction of the natural numbers (0 is the empty set, 1 = {0}, ..., 5 = {0,1,2,3,4}, etc.) but their example of "3 ∩ 4 = 3" or "4 intersect 3 is 3" doesn't seem weird, problematic or even useless to me, it just looks like a handy set theoretic implementation of the min() function.