Hacker News Reader

I’m a bit confused about the functions always being continuous. Step functions being ill-defined makes sense, but how about modulos? f(x) = x mod 1 should be trivially discontinuous. I should also be able to contruct the set of integers Z (using the unit 1 and succession operator) and identify the largest integer that is smaller than x by intersecting [x-1, x) with Z. Do I need to show the intersection always contain only one element?

View on HN

Well, x mod 1 is just x minus a series of Heaviside step functions, each of which are non-constructive. The core problem is determining if your real number x is equal to an integer. You might be able to prove that x is close to a particular n, but there may not be a constructive proof of either x<n, x=n, or x>n. Hence you don't know if x mod 1 should be x-(n-1) or x-n.

I think your definition depends on being able to decide for every real x whether n ∈ [x-1, x), for which you need that n < x. According to the slides that is not generally possible in constructive mathematics.

Reply on news.ycombinator.com