Hacker News new | ask | show | jobs
by andyjohnson0 172 days ago
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...

3 comments

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.
By itself it's not a problem, but it's certainly useless. Perhaps you can tell me what use "3 ∩ 4 = 3" has.

The problem is that these properties get in the way of proving arithmetic theorems because if you are being absolutely strict, you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers. This introduces a lot of noise and makes formal proofs very frustrating, somewhat like when you're programming and you have to bend the type system of your compiler to accept your code even though the program is conceptually correct and you end up spending effort on type coercions, casts, "unsafe" blocks etc... mathematically this makes your proof significantly longer, more brittle, and harder to reuse because it accidentally depends on details of the chosen encoding rather than on the intrinsic properties of arithmetic.

> Perhaps you can tell me what use "3 ∩ 4 = 3" has.

As I said:

> a handy set theoretic implementation of the min() function.

i.e. if you wanted (for whatever reason) to define min(a, b) directly and briefly in your set theoretic reconstruction of the natural numbers, you can just use intersect operator and define it as "a ∩ b".

Perhaps because in terms of the interesting distinction you introduce:

> you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers

this particular operation seems to be part of the former rather than of the latter.

It's a leaky abstraction, in software terms. Ideally, an abstraction models the semantics of the problem domain "opaquely"; ideally our natural numbers have only the properties of the natural numbers and no others. An additional property leaking through is not like handy "bonus", but a point of confusion. You can't rely on it in proofs involving natural numbers without being careful to delineate which conclusions follow from the construction vs. which are inherent.
Arithmetic is not a categorical theory, meaning there is no unique model for it: https://math.stackexchange.com/questions/4667959/are-there-n...
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.

This was helpful, thanks.
the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory.

don’t be mislead about what a junk theorem is!

Thank you. I was following along until that paragraph and got the opposite interpretation too.
Yah, I read that and thought "this seems like gibberish: maybe I am reading LLM slop".