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

摘要

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