offtopic: `DecidableEq α` implies `#α ≤ ℵ₀`?

Stream: maths

[Jz Pan]

I think this is true if classical is not allowed to use, since you can't have a program which stops in a finite time and decides the equality of uncountably many elements. Is this correct? And this result cannot be proved inside Lean, right?

[Yury G. Kudryashov]

There is a formalization of something equivalent to a Turing machine in the library, but how do you formally state your theorem without assuming that the type is countable? What's the input of a program that implements DecidableEq?

[Daniel Weber]

Jz Pan said:

I think this is true if classical is not allowed to use, since you can't have a program which stops in a finite time and decides the equality of uncountably many elements. Is this correct? And this result cannot be proved inside Lean, right?

I'm not sure how to prove that there isn't any quotient of ℕ → ℕ, for instance, with a decidable relation (when given the functions as oracles) but uncountably many equivalence classes

[Daniel Weber]

I figured out how: for any function f look at the execution of rel f f. If you only look at the values of f this computation queries, you get a function f' : ℕ →₀ ℕ. Now note that if f' = g' then surely rel f g, and because ℕ →₀ ℕ is countable there can only be a countable number of congruence classes.

[Daniel Weber]

I think you should be able to prove your statement using structural induction on α, then, but yeah, it couldn't be proven in Lean, as choice is consistent

[Daniel Weber]

Daniel Weber said:

I figured out how: for any function f look at the execution of rel f f. If you only look at the values of f this computation queries, you get a function f' : ℕ →₀ ℕ. Now note that if f' = g' then surely rel f g, and because ℕ →₀ ℕ is countable there can only be a countable number of congruence classes.

Actually this can generalized to "when you run the algorithm to decide x = x you can only check a part of x for which there are countably many options"

[Jz Pan]

Daniel Weber said:

If you only look at the values of f this computation queries, you get a function f' : ℕ →₀ ℕ.

Yes that was what I thought. But I think this part cannot be formalized inside Lean...

[Johan Commelin]

Not an expert, but I guess it is consistent to assume the implication as an axiom (in the absence of choice).
But you can't prove the implication without axioms, exactly because it contradicts choice. If it were provable, then Lean + choice would be inconsistent.

[Yury G. Kudryashov]

You can replace DecidableEq with something explicit involving turing machines, but I don't know how to do it without assuming that α is countable.

[Daniel Weber]

Yury G. Kudryashov said:

You can replace DecidableEq with something explicit involving turing machines, but I don't know how to do it without assuming that α is countable.

You could define Turing Machines with oracle access to a restricted part of Lean