Martin—Lof类型论中不普和的推广和有究类型的可定义性

摘要

本文推广了不交和运算且给出ｎ个类型不交和的规则借助于它，证明了有穷类型的封闭性和分离性，讨论有究类型的可定义性，证明Ｎｋ可由Ｎ１和ｋ个类型不交和而定义以及Ｎｋ可由Ｎｋ＋１定义。