Martin-Löf类型论中不交和的推广和有穷类型的可定义性

下载PDF

导出

摘要本文推广了不交和运算且给出n个类型不交和的规则,借助于它,证明了有穷类型的封闭性和分离性,讨论有穷类型的可定义性,证明N_(k)可由N_(1)和K个类型不交和而定义以及Nk可由N_(K+1)定义.

作者宋方敏

机构地区南京大学数学系

出处《数学年刊(A辑)》 CSCD 北大核心 1994年第4期472-477,共6页 Chinese Annals of Mathematics

关键词类型论不交和有穷类型的可定义性

1彭丽华,焦勇.自由随机变量和的凹Φ不等式[J].中国科学：数学,2015,45(5):683-694.
2宋方敏.在Martin－Lof类型论中添加判断的新形式[J].数学年刊（A辑）,1994,1(2):177-184.
3夏伟洪,汤建钢.具有左R-模结构的类型及其范畴逻辑模型[J].数学的实践与认识,2015,45(23):260-270. 被引量：6
4张锦文.A Hierarchy of Axiom Systems for Set Theory[J].Chinese Quarterly Journal of Mathematics,1989,4(3).
5章文捷,沈元隆.计算线形和环形连续k-out-of-n:F系统可靠性的新算法[J].通信学报,2000,21(8):79-84. 被引量：2
6宋方敏.直觉主义类型论中否定构造的研究[J].南京大学学报（自然科学版）,1991,27(2):203-208.
7赵院娥,乔淑莉.悖论及其对数学发展的影响[J].延安大学学报（自然科学版）,2004,23(1):21-25. 被引量：5
8张玉平.可定义的推导关系[J].中国科学（E辑）,1998,28(5):439-445.
9王菲,闫慧臻.网络可靠度的不交分解算法[J].大连轻工业学院学报,1999,18(4):351-356. 被引量：1
10王玮.省略内聚集（英文）[J].南京大学学报（数学半年刊）,2013,30(1):40-47.

数学年刊(A辑)

1994年第4期

浏览历史

内容加载中请稍等...