coq 谓语逻辑中的存在量词（系统 F）答案

【问题标题】：Existential quantifier in coq impredicative logic (System F)coq 谓语逻辑中的存在量词（系统 F）
【发布时间】：2013-09-29 20:58:11
【问题描述】：

我试图用 lambda 演算编码的 Coq 逻辑连接词，类型为 System F。这是我写的一堆代码（我认为是标准的东西）

Definition True := forall X: Prop, X -> X.

Lemma I: True.
Proof.
  unfold True. intros. apply H.
Qed.

Section s.
Variables A B: Prop.


(* conjunction *)

Definition and := forall X: Prop, (A -> B -> X) -> X.
Infix "/\" := and.

Lemma and_intro: A -> B -> A/\B.
Proof.
  intros HA HB. split.
  apply HA.
  apply HB.
Qed.

Lemma and_elim_l: A/\B -> A.
Proof.
  intros H. destruct H as [HA HB]. apply HA.
Qed.

Lemma and_elim_r: A/\B -> B.
Proof.
  intros H. destruct H as [HA HB]. apply HB.
Qed.



(* disjunction *)

Definition or := forall X:Prop, (A -> X) -> (B -> X) -> X.
Infix "\/" := or.

Lemma or_intro_l: A -> A\/B.
  intros HA. left. apply HA.
Qed.

Lemma or_elim: forall C:Prop, A \/ B -> (A -> C) -> (B -> C) -> C.
Proof.
  intros C HOR HAC HBC. destruct HOR.
    apply (HAC H).
    apply (HBC H).
Qed.


(* falsity *)

Definition False := forall Y:Prop, Y.

Lemma false_elim: False -> A.
Proof.
  unfold False. intros. apply (H A).
Qed.

End s.

基本上，我写下了合取、析取、真假的排除和引入法则。我不确定是否正确地做事，但我认为事情应该这样工作。现在我想定义存在量化，但我不知道如何进行。有人有什么建议吗？

【问题讨论】：

一个小评论：假，and，or 已经是 Coq 的条款。您可能希望使用 other 来轻松区分您的构造和 Coq 的构造。
您还没有证明析取和合取定义的引入和消除原则。你已经证明了 Coq 的定义。您需要将您的符号放在 type_scope 中以覆盖 Coq。

标签： logic coq impredicativetypes

【解决方案1】：

存在量化只是合取的概括，其中对的第二个分量的类型取决于第一个分量的值。当没有依赖时，它们是等价的：

Goal forall P1 P2 : Prop, (exists _ : P1, P2) <-> P1 /\ P2.
Proof. split. intros [H1 H2]. eauto. intros [H1 H2]. eauto. Qed.

Coq'Art 从第 130 页开始有一个关于不可预测性的部分。

Definition ex (T1 : Type) (P1 : T1 -> Prop) : Prop :=
  forall P2 : Prop, (forall x1, P1 x1 -> P2) -> P2.

Notation "'exists' x1 .. x2 , P1" :=
  (ex (fun x1 => .. (ex (fun x2 => P1)) ..))
  (at level 200, x1 binder, right associativity,
  format "'[' 'exists' '/ ' x1 .. x2 , '/ ' P1 ']'") : type_scope.

含意定义的问题（除非我弄错了）是没有依赖消除。可以证明

forall (A : Type) (P : A -> Prop) (Q : Prop),
  (forall x : A, P x -> Q) -> (exists x, P x) -> Q,

但不是

 forall (A : Type) (P : A -> Prop) (Q : (exists x, P x) -> Prop),
   (forall (x : A) (H : P x), Q (ex_intro P x H)) ->
   forall H : exists x, P x, Q H

【讨论】：