Easiness in graph models (Q2368937): Difference between revisions

We generalize Baeten and Boerboom's method of forcing to show that there is a fixed sequence \((u_k)_{k\in\omega}\) of closed (untyped) \(\lambda\)-terms satisfying the following properties: (a) For any countable sequence \((g_k)_{k\in\omega}\) of Scott continuous functions (of arbitrary arity) on the power set of an arbitrary countable set, there is a graph model such that \((\lambda x.xx)(\lambda x.xx)u_k\) represents \(g_k\) in the model. (b) For any countable sequence \((t_k)_{k\in\omega}\) of closed \(\lambda\)-terms there is a graph model that satisfies \((\lambda x.xx)(\lambda x.xx)u_k=t_k\) for all \(k\). We apply these two results, which are corollaries of a unique theorem, to prove the existence of (1) a finitely axiomatized \(\lambda\)-theory \({\mathcal L}\) such that the interval lattice constituted by the \(\lambda\)-theories extending \({\mathcal L}\) is distributive; (2) a continuum of pairwise inconsistent graph theories (\(=\lambda\)-theories that can be realized as theories of graph models); (3) a congruence distributive variety of combinatory algebras (lambda abstraction algebras, respectively).