The Cantor-Bernstein theorem: how many proofs?

Dedekind's proof of the Cantor–Bernstein theorem is based on his chain theory, not on Cantor's well-ordering principle. A careful analysis of the proof extracts an argument structure that can be seen in the many other proofs that have been given since. I contend there is essentially one proof that comes in two variants due to Dedekind and Zermelo , respectively. This paper is a case study in analysing proofs of a single theorem within a given methodological framework, here Zermelo–Fraenkel set theory (ZF). It uses tools from proof theory, but focuses on heuristic ideas that shape proofs and on logical strategies that help to construct them. It is rooted in a perspective on Beweistheorie that predates its close connection and almost exclusive attention to the goals of Hilbert's finitist consistency programme. This earlier perspective can be brought to life (only) with the support of powerful computational tools. This article is part of the theme issue ‘The notion of ‘simple proof’ - Hilbert's 24th problem’.