Количество элементов Prop, Set и Type_i в Coq

Question

Можем ли мы назначить кардиналов в Coq Prop, Set и каждому Type_i? Я вижу только определение конечных кардиналов в библиотеке Coq, поэтому, возможно, нам понадобится определение больших кардиналов для начала.

В соответствии с семантикой доказательства несоответствия, например, здесь , Set и Type_i образуют возрастающую последовательность недоступных кардиналов . Можно ли это доказать в Coq?

Prop кажется более сложным из-за непредсказуемости. Неуместность доказательства означает, что мы идентифицируем все доказательства того же P : Prop и интерпретируем Prop как пару {false, true}. Таким образом, кардинал Prop будет равен 2. Однако для любых двух доказательств p1 p2 : P Coq не принимает eq_refl p1 в качестве доказательства p1 = p2. Таким образом, Coq не полностью идентифицирует p1 и p2. А с другой стороны, непредсказуемость означает, что для любых A : Type и P : Prop, A -> P имеет тип Prop. Это делает намного больше жителей, чем в Set.

Если это слишком сложно, может ли Coq доказать, что Prop и Set неисчислимы? По теореме Кантора 1038 * Кок легко доказывает, что не существует сюрприза nat -> (nat -> Prop). Это не очень далеко от доказательства того, что нет сюрпризов nat -> Prop. Но тогда нам нужен фильтр Prop -> (nat -> Prop), который изолирует, у Prop есть свободная переменная nat. Можем ли мы определить этот фильтр в Coq, поскольку мы не можем сопоставить шаблон с Prop?

Answer 1

Невозможно показать, что Prop неисчислимо внутри Coq. Модуль ClassicalFacts в стандартной библиотеке показывает, что аксиома вырожденного высказывания forall A : Prop, A = True \/ A = False эквивалентна наличию исключенной средней и пропозициональной экстенсиональности. Поскольку теоретическая модель множества Кока подтверждает эти две аксиомы, Кок не может опровергнуть вырождение.

Конечно, можно показать, что Set и Type бесконечны, так как они содержат все типы Fin n натуральных чисел, ограниченные n, и эти типы доказуемо отличаются друг от друга, так как имеют разные кардинальное. Я подозреваю, что можно показать, что они неисчислимы, адаптируя обычный аргумент диагонализации - то есть предположим, что некоторая обратимая функция подсчета e : nat -> Set, и попытаться закодировать что-то вроде типа всех натуральных чисел, которые «не содержат самих себя". Я не знаю, как вы будете доказывать, что эти типы - недоступные кардиналы.