Extending Models of Second Order Predicate Logic to Models of Second Order Dependent Type Theory

. We describe a method for constructing a model of second order dependent type theory out of a model of classical second order predicate logic. Apart from the construction being of interest by itself, this also suggests a way of proving the completeness of the formulasas -types embedding from second order predicate logic to second order dependent type theory. Under this embedding, formulas are interpreted as types, and derivability (of a formaula) in the logic should correspond to inhabitation (i.e. the associated type being nonempty) in the type system. This correspondence works in one way (called soundness): if a formula is derivable, then the associated type is inhabited (there is a term of that type). It's an open problem whether the correspondence works in the other direction (called completeness): if the type associated with formula ' is inhabited, then ' is derivable. The completeness is proved if any model M of second order logic can faithfully be extended to a model S(M) of s..