Дмитрий. Все же Феферман дал мне еще один повод для сомнения. Нет, вы меня в принципе убедили, что нельзя строить конструкцию, не определив ее части. Но как вы прокомментируете Определение 4.39 ii на странице 147?

(ii) 0 делит а тогда и только тогда, когда а=0;

(Reply to this) (Parent) (Thread)

Это не определение, а теорема, и она немедленно следует
из определения b|a: b|a равносильно существованию целого q, такого, что a=bq.
Следовательно, 0|a равносильно существованию целого q, такого, что a=0q=0, то есть a=0.
Однако следует понимать, что верность утверждения «a делит b» не имеет отношения к существованию частного b/a.

(Reply to this) (Parent) (Thread)

Да, виноват это теорема. Хотел написать и 4.38 и 4.39, а вышло...
Но все же, странно, когда вообще так говорят, что «a делит b». Если делит, значит должно быть частное. Здесь очень специфическое понятие операции деления, не совпадающее с ограничением для делителя в теореме 4.37 на стр. 145 и ее расширением в упражнении 1 на стр. 160.

(Reply to this) (Parent) (Thread)

>Если делит, значит должно быть частное.

Вместо «b делит a» можно сказать «a кратно b».
В последнем случае паразитных ассоциаций с делением не возникает.

Вообще, «b делит a» означает лишь то, что частное, если
оно существует, является целым числом.

(Reply to this) (Parent)