Retrieve I-th computable from table: computable by assumption.
Get K-th digit from a given computable: computable by definition.
Get I-th digit of I-th computable: computable as composition of (1) and (2).
Invert given digit: trivially computable.
Get an inverted I-th digit of I-th computable: computable as composition of (3) and (4).
I’ve actually written formal refutation of any bijection between N and 2N in Idris 2.
Demonstration
total stands for functions which are defined everywhere on their stated domain (as opposed to partial), and computations for which are proven to always halt (if there’s no such guarantee, function is covering). %default total means that all functions below must be total.
Void type means that a contradiction was obtained from given arguments.
%default total
data Bijection : Type -> Type -> Type where
||| A bijection between two types.
||| @ a the first type
||| @ b the second type
||| @ fwd mapping from first type to the second
||| @ bck mapping from second type to the first
||| @ fb_producer proof that fwd . bck = id
||| @ bf_producer proof that bck . fwd = id
DoMap : {0 a,b : Type} -> (fwd: a -> b) -> (bck: b -> a)
-> (fb_producer: (av : a) -> (bck $ fwd av) = av)
-> (bf_producer: (bv : b) -> (fwd $ bck bv) = bv)
-> Bijection a b
map_fneq : {0 a,b : Type} -> {f : a->b} -> {g : a->b} -> f = g -> (v:a) -> f v = g v
map_fneq (Refl {x = f}) v = Refl
bool_inv : {v : Bool} -> (v = not v) -> Void
bool_inv {v = True} prf = uninhabited prf
bool_inv {v = False} prf = uninhabited prf
diagonal : (Bijection Nat (Nat -> Bool)) -> Void
diagonal (DoMap f g _ bf_prf) = bool_inv conflict where
H : Nat -> Bool
H i = not $ f i i
h_hi_by_idx : f (g H) (g H) = H (g H)
h_hi_by_idx = map_fneq (bf_prf H) (g H)
h_hi_by_def : H (g H) = (not $ f (g H) (g H))
h_hi_by_def = Refl
conflict : f (g H) (g H) = (not $ f (g H) (g H))
conflict = trans h_hi_by_idx h_hi_by_def
I interpreted your algorithm for listing computables to be something like “enumerate the Turing machines that output ‘.’ then 0s and 1s and list what they print”, without worrying about the fact that some computables repeat. This technically lists all computables even though some machines will get stuck in some non-halting behavior that prints nothing after printing finitely many 0s and 1s. But you can’t figure out the nth digit of an arbitray thing in the list because you don’t always know if a machine will continue to print 0s or 1s or get indefinitely “stuck”.
It seems that you actually meant that you could have an algorithm that begins by enumerating the Turing machines that print computables and never get stuck in some non-halting configuration. This can’t be done.
If you have any surjection: N→S⊂(N→{0,1}) and diagonalize against it, you know the result is not in S. This fact doesn’t depend on the actual nature of the surjection N→S, just that S is the image. Here S is the computables.
I interpreted your algorithm for listing computables to be something like “enumerate the Turing machines that output ‘.’ then 0s and 1s and list what they print”, without worrying about the fact that some computables repeat.
I’m pretty sure my argument did not mention how computables are listed at all, rather proving that for any specific listing the inverse-diagonal is computable as well.
If you have any surjection: N→S⊂(N→{0,1}) and diagonalize against it, you know the result is not in S. This fact doesn’t depend on the actual nature of the surjection N→S, just that S is the image. Here S is the computables.
Yes. However, it’s the specific choice of set “computables” which creates the contradiction: I agree with “inverse-diagonal for rationals is an irrational number” and like.
Once again: for any “user-provided” computable table of computable digit sequences, I can, in finite time, get value for any specific position in table; therefore, each digit of inverse sequence is computable; therefore, I conclude that the inverse-diagonal sequence is itself computable (if I’m not mistaken in definitions).
My claim is that such a table does not exist because it leads to a contradiction. If you add it as an assumption, you can obtain a false conclusion because the assumption itself can never hold.
Retrieve I-th computable from table: computable by assumption.
Get K-th digit from a given computable: computable by definition.
Get I-th digit of I-th computable: computable as composition of (1) and (2).
Invert given digit: trivially computable.
Get an inverted I-th digit of I-th computable: computable as composition of (3) and (4).
I’ve actually written formal refutation of any bijection between N and 2N in Idris 2.
Demonstration
totalstands for functions which are defined everywhere on their stated domain (as opposed topartial), and computations for which are proven to always halt (if there’s no such guarantee, function iscovering).%default totalmeans that all functions below must be total.Voidtype means that a contradiction was obtained from given arguments.I interpreted your algorithm for listing computables to be something like “enumerate the Turing machines that output ‘.’ then 0s and 1s and list what they print”, without worrying about the fact that some computables repeat. This technically lists all computables even though some machines will get stuck in some non-halting behavior that prints nothing after printing finitely many 0s and 1s. But you can’t figure out the nth digit of an arbitray thing in the list because you don’t always know if a machine will continue to print 0s or 1s or get indefinitely “stuck”.
It seems that you actually meant that you could have an algorithm that begins by enumerating the Turing machines that print computables and never get stuck in some non-halting configuration. This can’t be done.
If you have any surjection: N→S⊂(N→{0,1}) and diagonalize against it, you know the result is not in S. This fact doesn’t depend on the actual nature of the surjection N→S, just that S is the image. Here S is the computables.
I’m pretty sure my argument did not mention how computables are listed at all, rather proving that for any specific listing the inverse-diagonal is computable as well.
Yes. However, it’s the specific choice of set “computables” which creates the contradiction: I agree with “inverse-diagonal for rationals is an irrational number” and like.
Once again: for any “user-provided” computable table of computable digit sequences, I can, in finite time, get value for any specific position in table; therefore, each digit of inverse sequence is computable; therefore, I conclude that the inverse-diagonal sequence is itself computable (if I’m not mistaken in definitions).
My claim is that such a table does not exist because it leads to a contradiction. If you add it as an assumption, you can obtain a false conclusion because the assumption itself can never hold.