Strong stability and the incompleteness of stable models for λ-calculus Original Research Article

We prove that the class of stable models is incomplete with respect to pure λ-calculus. More precisely, we show that no stable model has the same theory as the strongly stable version of Parkʹs model. This incompleteness proof can be adapted to the continuous case, giving an incompleteness proof for this case which is much simpler than the original proof by Honsell and Ronchi della Rocca. Moreover, we isolate a very simple finite set, View the MathML source, of equations and inequations, which has neither a stable nor a continuous model, and which is included in View the MathML source and in View the MathML source, the contextual theory induced by the set of essentially λI-closed terms. Finally, using an approximation theorem suitable for a large class of models (in particular stable and strongly stable non-sensible models like View the MathML source and View the MathML source), we prove that View the MathML source and View the MathML source are included in View the MathML source, giving an operational meaning to the equality in these models.