Implementing the `Fool's model' of combinatory logic (Q1181718)

The paper studies `Fool's models' of combinatory logic. A `fool's model' is a family of sets of propositional formulas, built with the implication symbol only, which is closed under condensed detachment of implicational calculus. Alternatively, it is a model of combinatory logic in set theory. `Fool's models' allow the investigation of properties of combinators. On the other hand, the correlation between implicational calculus and combinatory logic via the `fool's models' permits the application of methods of combinatory logic to theorem proving in implicational calculus. As a technical result, it is shown that the pure implicational calculus \(T\to\) consisting of the combinators \(B\), \(B'\), \(I\) and \(W\) is complete in the sense that all theorems can be generated by straightforward resolution with the condensed detachment rule. Furthermore, \(R\to\) is minimal among the systems with this property. An implementation of the `fool's model' ideas is presented in the last section. Some suggestions for exploiting it to do theorem proving in the implicational calculus are made.