There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.
(defn unenumerated (n) (not ((enumerate n) n)))
If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.
This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.
Okay, but if we take the position that only non-halting (for all inputs) programs represent functions over N, if your program “unenumerated” never halts for some N, it doesn’t represent a function, so your argument isn’t a case of “using the enumeration of all functions to produce something which doesn’t belong to the enumeration”
Obviously an enumeration of all computable functions isn’t itself computable. But if we consider Axiom CompFunc “if a function over N is computable then it exists” (so this axiom guarantees the existence of all computable functions, but is silent on whether any non-computable functions exist) and then we consider the additional Axiom CountReals “there exists a function from N to all functions over N”, then are those two axioms mutually inconsistent? I don’t think your argument, as given, directly addresses this question
For the argument that I gave to work, you need what you might call Axiom ComposeFunc, you may always compose a new function by taking an existing function and doing something that is known to be valid with it. Obviously this axiom is true about the computable universe. But, more than that, it is also true about any generalization of "function" that behaves like most would expect a function to have.
Now it is true that your Axiom CompFunc and Axiom CountReals do not necessarily contradict each other. But CompFunc, ComposeFunc and CountReals do contradict each other, and the contradiction can be built by following Cantor's diagonalization argument.
It isn’t true in NFU though, correct? At least not in the general case. Because Cantor’s argument fails in NFU
So it has non-computable functions, but also has a type system that tries to avoid allowing self-reference. And that type system gets in the way of Cantor's argument.
I clearly hadn't thought of this possibility. It is a constraint of a kind that doesn't show up in the computable universe.
And so, going back, if the the Russian constructivist school does indeed center on computability, then my first answer to you was correct.
The (un)countability of the reals is known to be independent of NFU-it is consistent both with the reals being countable and them being uncountable. There are two different axioms which it is standard to add to NFU to decide this-AxCount≤ which implies the reals are countable and AxCount≥ which implies the reals are uncountable.
I guess I was suggesting that in the same way, an additional axiom could be added to computable set theory which renders the reals countable or uncountable. If an additional axiom asserting the countability of the reals involves the existence of a function from the naturals to functions over the naturals, that would obviously be introducing an uncomputable function-but for that to produce an inconsistency, it would need to enable Cantor’s argument-and, given your “ComposeFunc” in the computable universe is already restricted to only operating over computable functions, it is reasonable to limit its application to computable functions in an extension, which would mean the addition of this uncomputable function would still not permit Cantor’s argument
diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)
diag f n = not (f n n)
The following argument is also constructive. Just like in classical mathematics, crustructive mathematics proves the negation of A by assuming A and deriving a contradiction. (But you cannot prove A by assuming it’s negation and deriving a contraction):
Assume a surjectiom f :: nat -> Bool. Then there is x such that f x = diag f. Since these two functions are equal, they take equal values when we evaluate them in any point. In particular f x x = diag f x, but since diag f x = not (f x x), by definition, we have that f x x = not (f x x). This is a contradiction since not does not have fixed points.
( I made nat a type variable here since this works for any type / set )