2010-9-11

Coq的核心是基于归纳定义的构造演算,而这一切都是建立在直觉主义逻辑之上的。
有些问题是很有趣的,比如无限小。我在大学里学数学分析的时候,课本的定理和定义中并没有提及无限小。总是说对于任意大于0的整数epsilon,怎样怎样怎样。通过牛顿之后的很多数学家的一起努力,终于在微积分的表述中消除了无限小。而数学直觉主义则更保守,它不承认逻辑的排中率。所以数学直觉主义者不能用真值表的方式来证明那些基本的逻辑命题。Coq产生的是构造性的证明,我所难以理解,看不懂的。假设存在对于命题P的证明,并且有P->Q的证明,那么我们就证明了Q?
Coq中很强调类型。所有的对象必须有一个类型。不能说“对于所有的x,命题P成立",而要说"对于所有属于T类型的x,命题P成立"。
顺便google了一下,找到了一个对选择公理讨论的很到位的网页:http://www.math.vanderbilt.edu/~schectex/ccc/choice.html
Coq这套东西太别扭了,我不知道继续学下去有什么意义

此博客中的热门博文

在windows下使用llvm+clang

少写代码,多读别人写的代码

tensorflow distributed runtime初窥