Implementing the `Fool's model' of combinatory logic

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Review text

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.

Recommendations

Cites work

Cited in

(6)

This page was built for publication: Implementing the `Fool's model' of combinatory logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1181718)