其中是谓词公理Coq的可拓性

Question

Coq FAQ说公理:

Extensionality of predicates: ∀ P Q:A→ Prop, (∀ x, P(x) ↔ Q(x)) → P=Q

与Coq一致。这是在哪个图书馆断言的?它既不是逻辑的，也不是经典的

Answer 1

Ensembles库中的Extensionality_Ensembles与您发布的公理等效。

Answer 2

我认为这个公理没有在当前的标准库中声明;它是一个非常强大的(正如你在ClassicalFacts.v中看到的)，所以你需要自己声明它。你的特殊情况是由它+函数的扩展性我认为:

Require Import ClassicalFacts.
Require Import FunctionalExtensionality.
Axiom pe : prop_extensionality.
Lemma pred_extensionality A (P Q : A -> Prop) :
  (forall x, P x <-> Q x) -> P = Q.
Proof. now intros H; apply functional_extensionality; intros x; apply pe. Qed.