No Fixed-Point Combinator from B and M, Even up to beta-eta-Conversion

Status: preprint, not peer reviewed. This work was directed by the author and assisted by AI systems, which were used for proof development, the Lean formalization, drafting and review. The Lean proof is checked by the Lean kernel. The written proof has not been independently checked by a human. A fixed-point combinator is a closed term Y with Yx = x(Yx) for a fresh variable x. We prove that no applicative combination of B = λfgz.f(gz), M = λz.zz and I = λz.z is one, even up to βη-conversion; more generally, Yx ≠βη xq(Yx) for every such Y and every q ≥ 1, also when Y contains variables other than x. The question for B and M goes back to Smullyan and is Problem 4 of the TLCA list; at the weak equality of combinatory logic, where it is usually read, Imamura has recently given a negative answer in a preprint, and he asks for the answer at βη, which we give. The closed case is formalized in Lean 4, with no external library. Files: paper.pdf, its source paper.tex, and the Lean release min2_final5.tar.gz. To check the proof, unpack the archive and run bash scripts/check.sh.