Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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...




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: