1
$\begingroup$

I am new to combinatory logic, and I am interested in its relationship to first-order logic. In particular, I am wondering if there is a universal translation of first-order logic to combinatory logic with the usual combinators S, K, B, C, I, together with Schonkinfel's combinator U (which stands for disjoint class: UPQ=$\neg\exists x(Px\wedge Qx)$). For instance, given a sentence $\forall y\exists x(Ny\supset (Px\wedge Gxy))$, its translation in CL is $UN\mathrm{B}(UP)(\mathrm{C}G)$ (this example is taken from https://plato.stanford.edu/entries/logic-combinatory/). Is there a universal procedure for translating first-order formulas (and is there a way of translating combinators into first-order formulas)? On this note, I am also curious if the combinator U can be defined in terms of S and K.

Many thanks in advance.

$\endgroup$
  • $\begingroup$ This is the first time I hear of this connection, but as far as I can see, your question is already answered positively in your link. $\endgroup$ – Emil Jeřábek Jul 4 '18 at 10:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.