没有在coq

问题描述

我有兴趣尝试使用Coq构建集合论。我想定义一个类型sets而不指定其成员是什么，以及一个将两个集合映射到Prop的函数

Definition elem (s1 s1 : sets) : Prop.

然后我将集合论假设公理化，并将定理表示为（例如）

Theorem : ZFC -> (forall s : sets,~ elem s s).

但是，以上语法不起作用。这个想法可以在Coq中完成吗？在Coq中，有没有更好的方法可以实现这一目标？我对Coq并不陌生，因此如果有一种我不知道的明显方法，我深表歉意。

解决方法

您需要给定理起名字。为了假设事物，请使用Parameter和Axiom（从技术上讲，它们是同一件事，但您可以用来非正式地区分概念和事实）。

Parameter set : Type.
Parameter elem : set -> set -> Prop.

Axiom set_extensionality : forall x y,(forall z,elem z x <-> elem z y) -> x = y.
(* etc. *)

相比之下，Definition和Theorem用于定义和证明事物。假定ZFC公理，则可以证明集合不是其本身的元素。 Theorem命令首先采用一个定理名称（以后使用该定理名称）：

Theorem no_self_elem : forall x,~ elem x x.
Proof.
  (* tactics here. *)
Qed.