Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality (Q1283126)

An interpretation of Martin-Löf type theory is given which consists of a domain \(D\), a subdomain (of infinitary type expressions) \(S\) of \(D\) and a continuous map \(I\) sending elements of \(S\) to subdomains of \(D\) thus providing meaning for the elements of types. These data are all obtained as least fixpoints of appropriate domain equations. Thereafter, a totality predicate is defined on \(S\) and on each \(I(s)\) in such a way that all denotable elements are in fact total and the empty type has no total elements. This provides a domain-theoretic model of Martin-Löf type theory which is still faithful w.r.t.\ its logical interpretation. As applications some nonderivability results are given, most importantly the nonderivability of the statement that all type 2 functionals are continuous. The latter result is somewhat remarkable since the model does interpret functions as continuous maps. One should mention that in the meantime this line of work has been considerably advanced by \textit{U. Berger} [``Continuous functionals of dependent and transfinite types'', in: S. B. Cooper et al. (eds.), Models and computability. Invited papers from the Logic Colloquium '97, Leeds, UK, Lond. Math. Soc. Lect. Note Ser. 259, 1-22 (1999)] who establishes a Kleene-Kreisel style density theorem for total maps for a similar interpretation of Martin-Löf's type theory.