Non-existent Statman's double fixed point combinator does not exist, indeed (Q1368379)

Corrado Böhm pointed out the role of the combinator \({\mathbf S}{\mathbf I}\) in the theory of fixed point combinators [see \textit{H. Barendregt}: The lambda calculus. Its syntax and semantics. Rev. ed. (1984; Zbl 0551.03007), 6.5.3]. In particular, any fixed point combinator \(Y\) must satisfy \(Y={\mathbf S}{\mathbf I}Y\) (and conversely). Note that \({\mathbf S}{\mathbf I}\) reduces to the normal form \(\lambda vw.w(vw)\) that we shall denote by \(\delta\). Now, let \(Y\) be a fixed point combinator. \(Y({\mathbf S}{\mathbf I})\) is still a fixed piont combinator; for any given term \(M\), we have \(Y({\mathbf S}{\mathbf I})M={\mathbf S}{\mathbf I}(Y({\mathbf S}{\mathbf I}))M=M(Y({\mathbf S}{\mathbf I})M)\). So, \textit{R. Statman} [see Theor. Comput. Sci. 121, 441-448 (1993; Zbl 0795.03022), Problem 1(a)] has considered the very natural problem: 1.1 Problem (\(\lambda\beta\)-calculus). Is there a fixed point combinator \(Y\) such that \(Y=Y({\mathbf S}{\mathbf I})\)? (This problem is also stated as Problem 52 in the problem list of \textit{N. Dershowitz}, \textit{J. P. Jouannaud}, and \textit{J. W. Klop} [Lect. Notes Comput. Sci. 690, 468-487 (1993)].) Observe that we are asking for a simultaneous solution of the equation system \[ x={\mathbf S}{\mathbf I}x,\qquad x=x({\mathbf S}{\mathbf I}).\tag{1.2} \] So, it seems natural to call such a solution, if any, a double fixed point combinator. As is clear from the title of Statman's paper, he conjectured that the above-mentioned problem has a negative answer. In the present paper, we solve Problem 1.1 by showing that indeed no double fixed point combinator exists in the \(\lambda\beta\)-calculus. We end the paper with a few general remarks relating the given solution with some of the ideas involved in Statman's paper.