直觉主义类型论中否定构造的研究

STUDIES OF THE NEGATION IN THE INTUITIONISTIC TYPE THEORY

本文详细讨论直觉主义类型论中的否定构造,首先列出它的规则,然后证明一些有关否定的性质,最后证明对于直觉主义命题演算的可证命题在直觉主义类型论中可直接构造出其证明。

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.