Но это же уже не оригинальная система, там введены ограничения. Это нельзя назвать формализацией непосредственно канторовской системы
Ну что Вы, это настоящая формализация. Если бы Вы были правы, то у нас вообще никаких формализаций не было бы. Нельзя требовать от формализации полной эквивалентности неформальной теории просто потому, что неформальная теория определена только частично.
Все таки есть сомнения, что аксиома сформулированна именно так. Я почему-то не могу найти оригинал
Ну, "именно так" Вы у Фреге и не найдёте. Я как-то искал, нашёл перевод работы Фреге (Frege G., Grundgesetze der Arithmetik, begriffschriftlich abgeleitet, Bd 1—2, Jena, 1893—1903), в которой это положение сформулировано. Оно там сформулировано словами, столь архаичным языком, с таким количеством всяких философствований, что я читал и плевался. Тем более, что пришлось прочесть значительную часть статьи. Смысл состоит в том, что свойства отождествляются с множествами, и каждому свойству соответствует число (количество элементов с этим свойством), возможно, бесконечное. Возможно, тогдашним математикам такая формулировка казалась естественной и понятной. В современной теории множеств вместо аксиомы Фреге присутствует аксиома выделения.
Стало быть, берём свойство, которое в современном языке теории множеств записывается как
, ему соответствует множество
. Свойство, разумеется, существует (мы же его явно выписали и можем проверить для любого множества), а поскольку у нас свойства и множества — одно и то же, то множество, естественно, существует.