Intuition of why the Schroeder Bernstein is "non-computable"

Stream: new members

[Leo Shine]

Hello I've been working through the Mathematics in Lean textbook and I wanted to check I had an intuitive grasp of why the Schroeder Bernstein theorem is "non computable"

is the problem that to compute the bijection the theorem demonstrates needs potentially an infinite number of applications of f and g on the various subsets to work out whether we should use f or g ^-1?

[Kevin Buzzard]

Not really. It's simply that "computable" means "there is an algorithm" and if you are just doing regular mathematics and you have an element of a set $Y\cup Z$ then mathematically you know that this element is either in $Y$ or in $Z$ but there is no algorithm to tell you which one you're in (because $Y$ and $Z$ probably aren't defined by a Turing machine or whatever, they are just arbitrary), so you have to use the law of the excluded middle and this is noncomputable.

[Kevin Buzzard]

Basically most questions which involve sets which can be uncountable will be noncomputable because of the very nature of the concept of an algorithm.

[Felix Weilacher]

I don't understand the relevance of uncountability, and I think Leo's original explanation is basically correct.

See https://mathoverflow.net/questions/123482/is-there-a-constructive-proof-of-cantor-bernstein-schroeder-theorem

[Kevin Buzzard]

I am not an expert in this area and my understanding could well be wrong.

[Ming Li]

The other day @Patrick Massot gave a help on a lean code to prove the Shroeder Berstrein theorem, by using a fixed point of a monotone function on a subset of a power set. The latter is sort of Tarski lattice. Using the algorithm [#Algorithm_Tarski] (https://www.sciencedirect.com/science/article/pii/S0304397508003812?ref=pdf_download&fr=RR-2&rr=81b27b339fbf0758), I hope it can be computable.

[Jireh Loreaux]

Do you realize that algorithm is for finite lattices?

[Ming Li]

That's what I am concerned about. Computable depending on the growth of numbers of elements..? Ah, I am not a numerical one

[Jireh Loreaux]

I think that what you are hoping for is false because of this paper: https://arxiv.org/abs/1904.09193

[Jireh Loreaux]

But I'm not a logician, so I may be wrong.

[Jireh Loreaux]

This answer has more information, but in the comments it is noted that there is a related result, the Myhill Isomorphism Theorem, which is a sort of computable version of CSB.

[Ming Li]

As in the comments, it is also noted that excluded middle is used at every computable step along Konig's proof and only at the last step along Tarski's proof; also refer to @Kevin Buzzard's comment above. It seems that the Myhill Isomorphism Theorem is like finite issue, as you pointed out, in computing the Tarski's fixed point.