Weak completeness of type assignment in \(\lambda\)-calculus models: A generalization of Hindley's result (Q809993)

Given a \(\lambda\)-theory, \([[X]]^ D\) is an interpretation of a closed \(\lambda\)-term X of the theory in a model D and \([[]]_ v\) is an interpretation mapping type schemes into subsets of D. The \(\lambda\)- theory is said to be complete for a closed term X if \((\exists D)(\forall v)\{[[X]]^ D\in [[\alpha]]_ v\}\to \vdash \alpha X.\) This property is known to hold for some but not for all closed terms X. Hindley has suggested the following new notion: A \(\lambda\)-theory is said to be weakly complete if for all closed terms X, \((\forall D)[(\exists v)\{[[X]]^ D\in [[\alpha]]_ v\}\to (\exists M^*)([[M]]^ D=[[M^*]]^ D\wedge \vdash \alpha M^*)].\) The author proves that all \(\lambda\)-theories are weakly complete.