Arithmetical Fragment of Martin-Loef's Type Theories with Weak Sigma-Elimination

摘要

The author discusses the logical and the arithmetical fragments of Martin-Lof's type theories with a weak version of the Sigma elimination rule. The principal result of this paper is that the weak, intensional version of ML is conservative over Intuitionistic Finite Type Arithmetic HA(sup omega).