Completeness and Cut-elimination in the Intuitionistic Theory of Types.

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et. al. and the basis for the Prolog programming language. Our approach, extending techniques of Takahashi and Andrews and tableaux machinery of Fitting, Smullyan, Nerode and Shore, is to prove a completeness theorem for the cut-free fragment and show semantically that cut is a derived rule. This allows us to generalize a result of Takahashi and Schutte on extending partial truth valuations in impredicative systems. We extend Andrews' notion of Hintikka sets to intuitionistic higher-order logic in a way that also defines tableau-provability for intuitionistic type theory. In addition to giving a completeness theorem without using cut we then show, using cut, how to establish completeness of more conventional term models. These models give a declarative semantics for the logic underlying the Prolog programming. language. [ABSTRACT FROM AUTHOR]