A revised version of the “The countable reals“ paper is available. We threw out the faulty proof of "all maps are continuous", which therefore been relegated to an open problem.
The topos is very good at defying proofs that use the recursion theorem from computability. This is not a surprise, as the topos was constrcuted precisely for the purpose of defiting diagonal arguments.
In realizability LPO (every infinite binary sequence contains 1 or is all 0's) is invalid, which is shown using the recursion theorem. In our topos this doesn't work, but a nice idea of Joe Miller's does, so that's a new result in the revised version. The proof that LPO is invalid uses a principle which we call the "Majority Decision principle". I'll post about it separately.
https://arxiv.org/abs/2404.01256
Andrej Bauer /
npub1gp…tzrxg
2025-04-02 08:48:47
Author Public Key
npub1gpkd59s9m8v4k83e57pj0sufrta69whv6v9q9dqreyqwd5lehdvqutzrxgPublished at
2025-04-02 08:48:47Event JSON
{
"id": "4450c406fde985fd6eebf15b678b525076b610aeb503ac27d4a9840f33dca2ca",
"pubkey": "406cda1605d9d95b1e39a78327c3891afba2baecd30a02b403c900e6d3f9bb58",
"created_at": 1743583727,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/users/andrejbauer/statuses/114267503157583818",
"activitypub"
]
],
"content": "A revised version of the “The countable reals“ paper is available. We threw out the faulty proof of \"all maps are continuous\", which therefore been relegated to an open problem.\n\nThe topos is very good at defying proofs that use the recursion theorem from computability. This is not a surprise, as the topos was constrcuted precisely for the purpose of defiting diagonal arguments.\n\nIn realizability LPO (every infinite binary sequence contains 1 or is all 0's) is invalid, which is shown using the recursion theorem. In our topos this doesn't work, but a nice idea of Joe Miller's does, so that's a new result in the revised version. The proof that LPO is invalid uses a principle which we call the \"Majority Decision principle\". I'll post about it separately.\n\nhttps://arxiv.org/abs/2404.01256",
"sig": "178024bc10bc13ebe2f4e6de8186e49359676c51ccc25bf7ce830674a66d585a14e4163eb0b0b0d5120429d9ee3239320808548b1d6e9876af827da35331e90f"
}