证明 Prop 中的两个居民不相等？

Question

是否有可能有一些 A, B : Prop 以便我们可以提供以下证明：

Section QUESTION.
A: Prop := <whatever you want> .
B : Prop := <whatever you want> .
Theorem ANeqB: A <> B.
Proof.
<a proof of this fact>
Qed.

直觉上，我认为不会，因为这会让我们在证明之间 "distinguish"，但如果不在 A 或 B 上计算，就不能做到这一点。然而，Coq 明确禁止我们检查证明，因为它们必须在运行时被擦除。因此，只有 Prop 应该能够检查 Prop（由于擦除），但检查始终是计算性的，因此 Prop 无法检查 Prop。因此，无可检验Prop，上述定理ANeqB无法证明

如果我上面的解释不正确，你能解释一下为什么会这样吗？
如果无法证明定理ANeqB，你能给我指出这个事实的证明吗？
如果定理ANeqB可以被证明，你能告诉我我的直觉错在哪里吗？

编辑：

令我震惊的是，由于我们可以将证明无关性作为一个额外的公理 (Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.)，因此定理 ANeqB 无法在 Coq 中得到证明 --- 如果可以的话，它会使允许 proof_irrelevance 作为一个额外的公理是不合理的。

这就转移了我的问题，那么：

是否可以为一些居民 A 和 B 证明 ANeqB？（proof_irrelevance 更强：它表明我们无法证明 A <> B [实际上，我们可以证明 A = B] 的更强陈述所有 A, B)
如果不是，有人可以提供一个证明 ANeqB 不能在基于 Coq 的公理系统中被证明吗？

Answer 1

我想你可能在想别的事情。 Prop 本身并不是无关紧要的证据。它肯定具有可区分的元素。例如，True <> False.

Section QUESTION.
Definition A: Prop := True.
Definition B : Prop := False.

Theorem ANeqB: A <> B.
Proof.
  unfold A, B.
  intro p.
  destruct p.
  exact I.
Qed.

End QUESTION.

相反，Prop 中的 个元素 可能与证据无关。在公理

Axiom proof_irrelevance: forall (P: Prop) (p q: P), p = q.

p 和 q 本身不是 Prop 的元素，而是 Prop.

的某个元素的元素

证明 Prop 中的两个居民不相等？

Prove two inhabitants in Prop are not equal?

formal-verification

proof

coq