4 ms·

I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subse

I agree, but I also want to clarify that cantors argument was about subsets of the naturals (N), or more precisely functions from N to Bool (the decidable subsets). This is where the diagonal argument makes sense. So to conclude that there are more reals than naturals, the classical mathematical argument is: a) There are more functions N to Bool than naturals. b) There are as many reals as functions from N to Bool. Now, we of course agree the mistake is in b) not in a).

skissane 1y ago
> So to conclude that there are more reals than naturals, the classical mathematical argument is: > a) There are more functions N to Bool than naturals. > b) There are as many reals as functions from N to Bool. > Now, we of course agree the mistake is in b) not in a). Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false
- IngoBlechschmid 1y ago
  Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again. There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
  - skissane 1y ago
    Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either? If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
    - btilly 1y ago
      It should be true in the stronger sense. 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))) This function can be recognized as Cantor diagonalization, written out as a program. 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.
      - skissane 1y ago
        > 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. 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
        btilly 1y ago
        It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised. 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.
- gylterud 1y ago
  Bringing in computability from an external point of view is a mistake here. Markov had no issue with a. He would only disagree with b.

skissane 1y ago

> So to conclude that there are more reals than naturals, the classical mathematical argument is: > a) There are more functions N to Bool than naturals. > b) There are as many reals as functions from N to Bool. > Now, we of course agree the mistake is in b) not in a). Given certain foundations, (a) is false. For example, in the Russian constructivist school (as in Andrey Markov Jr), functions only exist if they are computable, and there are only countably many computable functions from N to Bool. More generally, viewing functions as sets, if you sufficiently restrict the axiom schema of separation/specification, then only countably many sets encoding functions N-to-Bool exist, rendering (a) false

IngoBlechschmid 1y ago
Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again. There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.
- skissane 1y ago
  Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either? If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?
  - btilly 1y ago
    It should be true in the stronger sense. 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))) This function can be recognized as Cantor diagonalization, written out as a program. 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.
    - skissane 1y ago
      > 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. 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
      - btilly 1y ago
        It's just a straight up liar's paradox. If enumerate is a function that works as advertised, then unenumerated is as well. If enumerate tries to list unenumerated, then enumerate can't work as advertised. 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.
gylterud 1y ago
Bringing in computability from an external point of view is a mistake here. Markov had no issue with a. He would only disagree with b.