在Martin－Lof类型论中添加判断的新形式

下载PDF

导出

摘要木文对于添加于Ｍａｒｔｉｎ－Ｌｏｆ类型论的四种新形式判断给出完整的描述．首先列出这些新判断形式的一般规则，然后证明带一个前提的假设判断可由这些新型判断替代，最后，重新作出笛卡儿积的消去和相等性规则使它们有与其他类型相同的式样而且证明新旧规则是等价的．

作者宋方敏

机构地区南京大学数学系

出处《数学年刊（A辑）》 CSCD 北大核心 1994年第2期177-184,共8页 Chinese Annals of Mathematics

关键词类型论判断范畴 M-L类型论

1宋方敏.Martin-Lf类型论中不交和的推广和有穷类型的可定义性[J].数学年刊（A辑）,1994,1(4):472-477.
2夏伟洪,汤建钢.具有左R-模结构的类型及其范畴逻辑模型[J].数学的实践与认识,2015,45(23):260-270. 被引量：5
3张锦文.A Hierarchy of Axiom Systems for Set Theory[J].Chinese Quarterly Journal of Mathematics,1989,4(3).
4罗海东.普通物理中的微元法[J].科技信息,2012(32):140-140. 被引量：2
5李勇,孙广.微元法在普通物理中的应用探微[J].科技信息,2009(3):219-220. 被引量：1
6郭亮.电磁学中的微元法探析[J].阴山学刊（自然科学版）,2007,21(2):52-54.
7宋方敏.直觉主义类型论中否定构造的研究[J].南京大学学报（自然科学版）,1991,27(2):203-208.
8赵院娥,乔淑莉.悖论及其对数学发展的影响[J].延安大学学报（自然科学版）,2004,23(1):21-25. 被引量：5
9王兆军.重指数族与推广的准似然函数间的关系[J].南开大学学报（自然科学版）,1995,28(4):78-81.
10王玮.省略内聚集（英文）[J].南京大学学报（数学半年刊）,2013,30(1):40-47.

数学年刊（A辑）

1994年第2期

浏览历史

内容加载中请稍等...