О существовании множества бесконечного по Дедекинду

[alex_dorin]

Здравствуйте !
Я получил очень странный результат : присоединение к аксиомам ZF(C) утверждения о существовании
множества бесконечного по Дедекинду превращает систему в противоречивую.
После изъятия аксиомы объединения такого противоречия средствами логических пруверов за обозримое время не выявлено.
Так как в ZF утверждение о существовании множества бесконечного по Дедекинду громоздкое, как доказать совместимость этого утверждения с аксиомой объединения ?
С уважением
А. Дорин

[Xaositect]

Давайте детали - где можно посмотреть доказательство противоречия?

[alex_dorin]

К сожалению запись всех конструкций на tex для меня проблема. Эти предложения я записываю в формате dfg, затем конвертирую в
формат tptp. Использование пруверов E, Metis, Vampire, Z3 дает одинаковый результат (естественно с разными протоколами доказательства).

[Xaositect]

Скиньте ссылку на исходный файл и доказательство. Правилами запрещены только рекламные ссылки, в нашем случае можно.

[Someone]

alex_dorin в сообщении #1027288 писал(а):

присоединение к аксиомам ZF(C) утверждения о существовании
множества бесконечного по Дедекинду превращает систему в противоречивую.

Я не понял. Множество называется бесконечным по Дедекинду, если оно равномощно собственному подмножеству. В ZFC все бесконечные множества такие.
Или речь идёт о существовании множеств, конечных по Дедекинду, но не равномощных никакому натуральному числу?
Известно, что в ZFC таких множеств нет: наличие аксиомы выбора позволяет найти подмножество, равномощное натуральному ряду, в любом множестве, которое не равномощно никакому натуральному числу (естественно, $0$ считается натуральным числом).
Поэтому речь может идти только о ZF.

[alex_dorin]

Никакого противоречия не обнаружено. Найдена синтаксическая ошибка в задании при работе с логическими пруверами.
Приношу мои извинения