> do you use Cantor-style diagonalization for the fixed-point theorem? If you think Kleene's recursion theorem and Cantor's diagonalization are the same sort o

> do you use Cantor-style diagonalization for the fixed-point theorem? If you think Kleene's recursion theorem and Cantor's diagonalization are the same sort of argument, then I'd say yes. I don't know if people historically had an issue with Cantor's argument or not. Certainly the modern presentation with decimals can be dicey if you are not careful because, as you note, some real numbers have two representations as decimals, one with repeating 9's and another with repeating 0's. But this issue can be avoided so long as you are careful. e.g convert all non-5's to 5's and convert 5's to 6's, thus staying far away from the dangerous 0/9 zone of digits. The constructed decimal sequence only has 5's and 6's and thus is a real number with a unique decimal representation. There is no problem with Cantor's argument, and it can easily be formalized. It would be a reasonable exercise to do at some point in an introductory course for proof assistants.