The exercise I'm dealing with asks me to show that by adding $S = K$ to the usual reduction rules for the SKI-calculus, one obtains an inconsistent equivalence. This must be done without using Böhm's theorem.
Now, I've found two terms (not combinators) $M$ and $N$ with the following properties:
- $M = x$
- $N = y$
- $M$ can be obtained from $N$ by replacing one or more occurrences of $S$ with $K$
From the rule $S = K$ we thereby get that $M = N$, and hence that $x = y$. Which means that any term can be proved equal to any other.
Do you think such an answer could work? Actually, Böhm's theorem (as shown in the book I am studying) establishes that, for distinct combinators $G$ and $H$, there is a combinator $D$ such that $DxyG = x$ and $DxyH = y$. So, I feel it would have been more appropriate to find a combinator $D$ such that $Dx_1x_2S = x_i$ and $Dx_1x_2K = x_j$ with $i, j = 1, 2$ and $i \neq j$. But I have HUGE problems in finding combinators, so I have only found terms respectively reducing to one of the variables, and obtainable one from another by replacing $S$ with $K$ or viceversa.