Если я правильно понял, дедекиндовость будет внутренним свойством модели. А метатеория, используемая для построения модели, с этим может быть никак не связана.
Совершенно верно.
Более того, если в роли метатеории тоже используется ZF, и в ней удалось доказать про некоторые множества, что они конечны по Дедекинду и бесконечны одновременно, то ZFC будет противоречива.
Этого я не понял. О каких именно множествах идёт речь? Если о метамножествах — то да. При этом противоречивой будет и ZFC, и ZF. Если же речь идёт о множествах предметной теории (той самой, для которой строится модель), пусть даже она тоже ZF, то никакого противоречия не будет. Это же
другая теория.
