процедура хотя бы конечна, не говоря уже о счетности ?
Это не конечный автомат. Главный (первый) цикл — бесконечный. Счетность для него не имеет смысла. Все внутренние циклы конечные, при обнаружении зацикливания определение бракуется. Катастрофичности в ошибке "сходится/не сходится" нет, поскольку эта ошибка покажет себя в дальнейшем. Какой объект брать первым? Не знаю, для алгоритма порядок безразличен, по аналогии, при выращивании кристалла поваренной соли безразлично, какой кристаллик выбрать в качестве затравки. Наверное, наименьший и правильный кристалл, и именно того рода (а не сахара), но это не критерий упорядоченности.
Противоречия эквивалентны? Не знаю, в каком контексте задан вопрос. Предложите пример, из трех различных конкретных противоречий, тогда на них можно будет рассмотреть свойство эквивалентности.
Противоречивые импликации существуют, и их нужно специально отыскивать и пытаться построить, — основное время проверок в алгоритме будет тратится на их поиск.
Пустое множество не существует в том смысле, что его определение противоречиво. Что-то вроде "неопределяемого понятия" или "сухой воды"... IMHO.
Ни одной луне не присуще быть звездой.
Из большинства импликаций не построить аристотелевских силлогизмов. Вы утверждаете, что из этого, конкретного, построили. Тогда главный вопрос, это возможен силлогизм или невозможен. Позвольте уточняющий вопрос:
Если (быть горячим) присуще всякой звезде
и (быть горячим) не присуще ни одной луне,
то ни одной луне не присуще быть звездой.
Какой из терминов в этом силлогизме больший, средний, меньший?