Разверните, пожалуйста, слова "...мне кажется, что интуитивное понятие "один и тот же объект" нельзя полностью формализовать".
Ну, формализация
интуитивных понятий - дело вообще тёмное. Но у меня соображения такие. Пусть имеется какая-нибудь теория с каким угодно набором аксиом, только непротиворечивая и потому имеющая модель. "Раздвоим" все объекты модели, считая, например, объектами теории не элементы модели, а упорядоченные пары

и

, причём,

, где

- элементы теории, а

и

- некие метки, доступные нам (в метатеории), но недоступные в (предметной) теории просто в силу определения равенства.
С интересом жду Вашей реакции на пятую страницу книги Френкеля.
Мне кажется, что я на неё
уже отреагировал. Давая определения множествам

и

, мы, вообще говоря, можем не знать, что эти определения эквивалентны, и что на самом деле

. Пока эквивалентность определений не доказана, мы не можем делать каких-либо обоснованных выводов из этого равенства, и если это равенство нам для чего-то понадобилось, то должны явно указывать это предположение (например:
Теорема (
![$[V=L]$ $[V=L]$](https://dxdy-04.korotkov.co.uk/f/b/e/4/be4c41001b1a91464d592ba553955ea782.png)
). Для каждого бесконечного кардинала

выполняется

).
А когда равенство

будет доказано, мы будем знать, что определения эквивалентны, а

и

- два имени одного и того же множества.
... нельзя полностью формализовать интуитивное понятие "конечное множество".
В той же книге Френкеля на странице 29: "a set

finite if the existence of mapping of

onto a subset

of

implies

."
Это просто определение конечного множества (если не ошибаюсь, принадлежащее Дедекинду; кроме того, здесь, вероятно, имелось в виду взаимно однозначное отображение или ещё какое-то условие, иначе непонятно, что делать с постоянным отображением

,

).
Существует другое определение, которому в настоящее время отдают предпочтение: множество конечно, если оно равномощно отрезку натурального ряда (пустой отрезок тоже допустим; имеется в виду стандартная модель натурального ряда, определяемая в теории множеств).
Оба определения равносильны, если справедлива аксиома выбора (хотя бы счётная), но без аксиомы выбора возможны конечные в смысле Дедекинда множества, которые не равномощны никакому отрезку натурального ряда. Это выглядит очень занятно: в множестве можно найти сколько угодно попарно различных элементов, но составить из них бесконечную последовательность нельзя.
Но я имел в виду другое. К сожалению, я не могу вспомнить, где я об этом читал, и подробностей тоже не помню. Смысл, если не ошибаюсь, состоял в том, что для любого набора аксиом, определяющих конечные множества в некоторой модели, можно построить другую модель, в которой выполняются те же аксиомы, но некоторые "конечные" множества оказываются бесконечными.
Например, арифметика Пеано равносильна теории, полученной из

заменой аксиомы бесконечности её отрицанием и добавлением схемы аксиом индукции. Все множества в этой теории конечны. Однако известно, что арифметика имеет нестандартные (даже несчётные) модели, в которых есть "бесконечные" натуральные числа.