On the Degeneracy of Σ-Types in Presence of Computational Classical Logic

摘要

We show that a minimal dependent type theory based on Σ-types and equality is degenerated in presence of computational classical logic. By computational classical logic is meant a classical logic derived from a control operator equipped with reduction rules similar to the ones of Felleisen's C or Parigot's μ operators. As a consequence, formalisms such as Martin-Loef's type theory or the (Set-predicative variant of the) Calculus of Inductive Constructions are inconsistent in presence of computational classical logic. Besides, an analysis of the role of the η-rule for control operators through a set-theoretic model of computational classical logic is given.