证明 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.

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

• 如果我上面的解释不正确，请您解释一下为什么会这样？
• 如果不能证明定理ANeqB，你能给我一个证明吗？
• 如果定理ANeqB可以被证明，你能告诉我我的直觉在哪里失败了吗？

编辑：

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

这改变了我的问题，然后：

• 是否有可能为一些居民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 的某些元素的元素。