如何解决没有在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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。