A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive...

on YouTube ↗19m

" summary

Paper proves a constructive Cantor–Bernstein for enumerable discrete types and gives three explicit bijection constructions: a Myhill-style staged build with an intricate termination algorithm that extends partial correspondences by a back-and-forth traversal; a simpler staged extension using a pigeonhole-style argument; and a canonical bijection using enumerations only that avoids the injections. Proofs use a Delta0-1 choice principle, total computability assumptions, are compact (under ~300 LOC) and machine-checked in Coq.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:21Cantor-Bernstein theorem overview
3. 2:31Constructive Cantor-Bernstein
4. 3:57Synthetic computability background
5. 6:10Myhill’s isomorphism theorem
6. 7:13Proof with correspondence sequences
7. 10:45Computability and constructive math
8. 12:11Proof via pigeonhole principle
9. 13:38Applicability beyond Coq
10. 15:25Summary and future work
11. 16:07Q&A