| 直觉主义类型论中否定构造的研究 |
| |
| 引用本文： | 宋方敏. 直觉主义类型论中否定构造的研究[J]. 南京大学学报(自然科学版), 1991, 27(2): 203-208 |
| |
| 作者姓名： | 宋方敏 |
| |
| 作者单位： | 南京大学数学系 |
| |
| 摘 要： |
|
| 关 键 词： | 类型论 直觉主义逻辑 否定 |
STUDIES OF THE NEGATION IN THE INTUITIONISTIC TYPE THEORY |
| |
| Song Fangmin. STUDIES OF THE NEGATION IN THE INTUITIONISTIC TYPE THEORY[J]. Journal of Nanjing University: Nat Sci Ed, 1991, 27(2): 203-208 |
| |
| Authors: | Song Fangmin |
| |
| Affiliation: | Department of Mathematics |
| |
| Abstract: | In this paper, the negation in ITT is studied. First, we write out the rules about it, and then prove its properties. We conclude that if a proposition A is provable in IPC, then there exists a term p such that p A is provable in ITT. |
| |
| Keywords: | type theory intuitionistic logic negation |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
