A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory - Archive ouverte HAL Access content directly
Conference Papers Year :

A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory

(1, 2) , (2) , (2)
1
2

Abstract

The Cantor-Bernstein theorem (CB) from set theory, stating that two sets which can be injectively embedded into each other are in bijection, is inherently classical in its full generality, i.e. implies the law of excluded middle, a result due to Pradic and Brown. Recently, Escardó has provided a proof of CB in univalent type theory, assuming the law of excluded middle. It is a natural question to ask which restrictions of CB can be proved without axiomatic assumptions. We give a partial answer to this question contributing an assumptionfree proof of CB restricted to enumerable discrete types, i.e. types which can be computationally treated. In fact, we construct several bijections from injections: The first is by translating a proof of the Myhill isomorphism theorem from computability theory-stating that 1-equivalent predicates are recursively isomorphic-to constructive type theory, where the bijection is constructed in stages and an algorithm with an intricate termination argument is used to extend the bijection in every step. The second is also constructed in stages, but with a simpler extension algorithm sufficient for CB. The third is constructed directly in such a way that it only relies on the given enumerations of the types, not on the given injections. We aim at keeping the explanations simple, accessible, and concise in the style of a "proof pearl". All proofs are machinechecked in Coq but should transport to other foundationsthey do not rely on impredicativity, on choice principles, or on large eliminations.
Fichier principal
Vignette du fichier
myhill-cantor-cpp23.pdf (531.73 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03891390 , version 1 (09-12-2022)

Licence

Copyright

Identifiers

Cite

Yannick Forster, Felix Jahn, Gert Smolka. A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory: Proof Pearl. CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575690⟩. ⟨hal-03891390⟩
0 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More