Mon 16 Jan 2023 12:07 - 12:30 at Studio 1 - Logical Foundations Chair(s): Robbert Krebbers

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 answer this question partially by contributing an assumption-free 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 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 machine-checked in Coq but should transport to other foundations – they do not rely on impredicativity, on choice principles, or on large eliminations.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

11:00 - 12:30
Logical FoundationsCPP at Studio 1
Chair(s): Robbert Krebbers Radboud University Nijmegen
11:00
22m
Talk
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systemsdistinguished paper
CPP
Christina Kohl University of Innsbruck, Aart Middeldorp University of Innsbruck
11:22
22m
Talk
Formalizing and computing propositional quantifiersremote presentation
CPP
Hugo Férée Université Paris Cité / IRIF, Sam van Gool Université Paris Cité / IRIF
11:45
22m
Talk
Encoding Dependently-Typed Constructions into Simple Type Theoryremote presentation
CPP
Anthony Bordg University of Cambridge, Adrián Doña Mateo The University of Edinburgh
12:07
22m
Talk
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
CPP
Yannick Forster Inria, Felix Jahn Saarland University, Gert Smolka Saarland University