What axioms can be added to $S,K$ combinator algebra without making it collapse into triviality?

Question

My understanding is that if you start with the free magma on two generators (call them $S$ and $K$) and then take a quotient with respect to the usual $S$ and $K$ equivalence rules ($Sfgx = fx(gx)$ and $Kxy = x$), you get the usual $S,K$ combinator algebra. (I think there may be something I don't get about $\eta$ equivalence and incompleteness with respect to $\lambda$-calculus, but that's another story.) What happens when you add other axioms that don't ordinarily belong, such as commutativity, associativity (perhaps limited), right inverse, things like $K^n = I = SKK$ or $S^n = I$ for large $n$, and so on? Are there any interesting systems like this on two generators, especially finite ones, that have nontrivial models? I can't visualize this and I'm not sure I even know how to think about the question.

Answer 1

Partial answer:

Commutativity: $\forall x \forall y (x y = y x)$

Let $K_2$ be an SK term such that $K_2 x y = y$. Then \begin{align} K K_2 &= K_2 K \\ K K_2 x &= K_2 K x \\ K_2 &= x & \text{(trivial theory)} \end{align}

Left-invertibility: $\forall x \exists y (y x = I)$

Always true: Let $y = K I$.

Right-invertibility: $\forall x \exists y (x y = I)$

\begin{align} K K^{-1} &= I \\ K K^{-1} x &= I x \\ K^{-1} &= x & \text{(trivial theory)} \end{align}

Associativity: $\forall x \forall y \forall z ((x y) z = x (y z))$

\begin{align} K K x &= K (K x) \\ K &= K (K x) \\ K y z &= K (K x) y z \\ y &= K x z \\ y &= x & \text{(trivial theory)} \end{align}

Note, however, that $I$ is not really a right-identity. Perhaps you meant cancellativity?

Right-cancellativity: $\forall f \forall g \forall x (f x = g x \rightarrow f = g)$

\begin{align} K K K &= I K \\ K K &= I \\ K K x &= I x \\ K &= x & \text{(trivial theory)} \end{align}

Left-cancellativity: $\forall f \forall x \forall y (f x = f y \rightarrow x = y)$

\begin{align} z &= z \\ (K z) x &= (K z) y \\ x &= y \end{align}

Suppose $I = K^n = K K^{n-1}$ for some $n > 0$, i.e. associating to the right. Then

\begin{align} I &= K K^{n-1} \\ I x &= K K^{n-1} x \\ x &= K^{n-1} & \text{(trivial theory)} \end{align}

Suppose $I = K^n = K^{n-1} K$ for some $n > 0$, i.e. associating to the left. Then note that

\begin{align} K^n &= \begin{cases} K & n \equiv 1 \mod 2 \\ K K & n \equiv 0 \mod 2 \end{cases} \end{align}

Case 1: \begin{align} I &= K^n \\ I &= K \\ I x y &= K x y \\ x y &= x \\ I y &= I \\ y &= I & \text{(trivial theory)} \end{align}

Case 2: \begin{align} I &= K^n \\ I &= K K \\ I x &= K K x \\ x &= K & \text{(trivial theory)} \end{align}

Answer 2

In general, the answer is essentially negative, because of Böhm's separability theorem. This a fundamental result in the theory of the $\lambda$-calculus and combinatory logic. For an informal but accurate account of Böhm's theorem, see here. For a more technically detailed and systematic account, see Barendregt's The Lambda Calculus. Its Syntax and Semantics (in particular, Chapters 4 and 10), or Hindley and Seldin's Lambda-Calculus and Combinators. An Introduction (in particular, Chapter 3).

I assume some familiarity with the $\lambda$-calculus and combinatory logic. Let us see first what happens in the $\lambda$-calculus, and then the corresponding results in combinatory logic.

In the $\lambda$-calculus, (a consequence of) Böhm's theorem says two $\lambda$-terms in $\beta$-normal form "behave in the same way" (operational equivalence) if and only if they are written in the same way (syntactic equivalence), apart for some expansions corresponding to the so-called $\eta$-equivalence of $\lambda$-terms (which is easily decidable). From that it easily follows that, for normalizing $\lambda$-terms, any non-trivial equivalence cannot equates more then $\beta\eta$. More precisely (Corollary 10.4.3 in Barendregt's textbook):

1. Let $M$ and $N$ be two distinct $\beta\eta$-normal forms. If you add the equivalence $M = N$ to $\beta$-congruence (the equivalence generated by $\beta$-reduction), then you can equate any pair of $\lambda$-terms.

In combinatory logic (generated by the combinators $S$ and $K$), the statement becomes (see Corollary 3.10.1 in Hindley and Seldin's textbook)

2. Let $M$ and $N$ be two distinct combinators in strong normal forms. If you add the equivalence $M = N$ to weak equivalence (the equivalence generated by usual reduction in combinatory logic), then you can equate any pair of combinators.

So, in combinatory logic, adding axioms that do not belong to the usual theory of combinatory logic (expressed by weak equivalence) and that equate two different strong normal forms, makes collapse the theory to the trivial inconsistency (everybody is equal to everybody). This is the case for associativity, commutativity, right-invertibility, and so on. I guess it is very hard to find an axiom that equates something of interest without being in the hypothesis above (and hence without collapsing everything).