The absence and the presence of fixed point combinators (Q807612)

The paper grew out of an (unsuccessful) attempt to prove a conjecture of Smullyan concerning failure of the fixed-point property (f.p.p.) for the combinators in the language \(\{\) M,B\(\}\), where \(Mx=xx\), \(Bxyz=x(yz)\). The absence of the f.p.p. is established instead for many sets of similar combinators. Choice of these sets was made with the help of a theorem- proving program for the logic with equality. This program (together with a special incomplete strategy) turned out to be efficient for finding a fixed-point combinator when it exists in the considered fragment. So its failure to produce such a combinator after long run was considered to be an indication of its absence, and the analysis of the search space helped to prove it.