2009/2/2 Luke Palmer
However! If we have a function f : Nat -> Nat -> Bool, we can construct the diagonalization g : Nat -> Bool as: g n = not (f n n), with g not in the range of f. That makes Nat -> Bool "computably uncountable".
This is making my head explode. How is g not in the range of f? In particular, f is a program, which I can easily implement; given: compiler :: String -> Maybe (Nat -> Bool) mkAllStrings :: () -> [String] -- enumerates all possible strings I can write f as f n = validPrograms () !! n where validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings Now, in particular, mkAllStrings will generate the following string at some index, call it "stringIndexOfG": <source code for compiler> <source code for mkAllStrings> <source code for f> g n = not (f n n) This is a valid program, so the compiler will compile it successfully, and therefore there is some index "validProgramIndexOfG" less than or equal to "stringIndexOfG" which generates this program. But your argument seems to hold as well, so where is the contradiction? -- ryan