I'm looking at the https://arxiv.org/abs/1904.09193 paper (version 2, from 2021) and think it has a few errors. I think I found three small places where the paper needs to be corrected (in the sense that the corrected version is valid - none of the key conclusions are undermined by this).

  1. On page 5 it says "Lemma 3.5. Let Q ∈ $2^{N_∞}$ be given. If Q(ω) = 1 and ∀n ∈ N. Q(n) = 1, then ∀p ∈ $2^{N_∞}$ . Q(p) = 1." I believe the second $2^{N_∞}$ should be $N_∞$ (because Q ∈ $2^{N_∞}$, you'd want to evaluate Q at an element of $N_∞$)

  2. A few lines down is the statement "Theorem 3.6 ([Esc13, Theorem 3.15]). There is a function ε : $2^{N_∞}$$N_∞$ such that for every Q ∈ $2^{N_∞}$ , if Q(ε(Q)) = 1, then ∀p ∈ $2^{N_∞}$ . Q(p) = 1.". The last $2^{N_∞}$ should be $N_∞$ for the same reason.

  3. At the end of the proof of that theorem, in "Hence Q(p) = 1 for every p ∈ $2^N$", $2^N$ should be $N_∞$ again for the same reason.

Perhaps this is a social question - how do I contact an author? - but I also wanted to post here to see whether what I am proposing is right and in case other people are hitting this when trying to read this paper.

P.S. I formalized these proofs at https://us.metamath.org/ileuni/nninfall.html and https://us.metamath.org/ileuni/nninfsel.html in case that helps.

  • 4
    $\begingroup$ The preprint lists the authors' institutional affiliations (but not their emails, unfortunately). The institution website will have homepage for their faculty where you can find their contact info - googling authorname institutionname will usually work. If what you found are indeed typos (even if only one out of the three is a genuine typo), the authors will probably appreciate your feedback. $\endgroup$ Aug 13, 2022 at 20:53
  • 4
    $\begingroup$ Assuming you have a valid arXiv account (or if you know someone who does), on the arXiv page you can click "view email" of the corresponding author who uploaded the pre-print. That e-mail will most likely be current (as every time you upload/update a pre-print arXiv asks you to update it if necessary). The uploader for the pre-print you mentioned is swansea.ac.uk/staff/p.r.a.pradic $\endgroup$ Aug 13, 2022 at 21:13

1 Answer 1


It may interest you that Martín Escardó also formalized the proofs, see Cantor-Schröder-Bernstein-gives-EM in his TypeTopology library.

Regarding contacting the authors, I am pretty sure this Pierre Pradic is the right one. Chad has always made it hard to be tracked down. If you search the coq-club mailing list archives from 2011 or so, you'll find his email address.

  • $\begingroup$ Oh nice. I figured I probably wasn't the first to formalize Schroeder-Bernstein implies excluded middle, but I was only aware of the Escardó paper on omniscience of NN_infinity, not his formalization linked above. $\endgroup$ Aug 14, 2022 at 2:45
  • 2
    $\begingroup$ I was able to email Pierre Pradic and there is now a version 3 of the paper at arxiv.org/abs/1904.09193 (published 15 Aug 2022) with the corrections. Thanks for all the help. $\endgroup$ Aug 21, 2022 at 5:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.