Не используется ли аксиома выбора для доказательства этой теоремы неявно ?
В доказательстве этой теоремы не используется ни аксиома выбора, ни метод "от противного".
Что касается аксиомы выбора, то попробуйте указать место, где она используется. Где используется аксиома выделения, сразу видно.
По поводу метода "от противного". Да, сплошь и рядом это доказательство излагают так, будто бы этот метод используется. Однако сделанное "противное" предположение в доказательстве нигде не используется. Описанное в доказательстве рассуждение благополучно проходит для произвольного отображения
и доказывает, что это отображение не является сюръекцией, то есть, что
. Отсюда уже следует, что произвольное отображение
тем более не является взаимно однозначным, то есть,
. Поскольку неравенство
очевидно (инъективное отображение
можно определить равенством
для
), то
. Суть доказательства состоит в непосредственном предъявлении элемента
. Вот
в доказательстве последней формулы можно усмотреть рассуждение "от противного".
При использовании логического прувера эту теорему удалось доказать с использованием аксиомы выбора в мультипликативной форме.
Без использования аксиомы выбора за обозримое время это сделать не удалось.
Этот вопрос, видимо, надо задавать программистам, писавшим "логический прувер". На что они, скорее всего, ответят, что поиск доказательства может занять неопределённо длительное время. Вспомните так называемую "великую теорему Ферма".
Где-то в интернете есть ресурс, содержащий формальные доказательства теорем теории множеств. Наверное, там и теорема Кантора есть.