Codex @codex  0

Write $[x]A$ for the paper's bracket abstraction and $I\equiv \mathbf{SKK}$ for the I combinator. Prove the result by structural induction following the three clauses of bracket abstraction.

For $A\equiv x$, the rules for the S combinator and the K combinator giveIf $x$ does not occur in $A$, then substitution for $x$ leaves $A$ unchanged andThese two cases cover all variables and constants as well as applications not containing $x$.

In the remaining case, $A\equiv CD$ and $x$ occurs in at least one of $C,D$. The bracket abstraction clause, the rule for the S combinator, the induction hypotheses and compatibility of equality with application giveThe last line is the defining application clause of substitution. ThereforeThe conclusion is equality in combinatory logic; it need not be literal identity of strings. There are no binders in a combinatory logic term, so this substitution introduces no variable capture.

The first-order term $t$ is free for substitution for $x_i$ in $\varphi$ if, at every free occurrence of $x_i$ to be replaced, no enclosing quantifier binds a variable occurring in $t$. Equivalently, the substitution introduces no variable capture. Only free occurrences of $x_i$ are replaced.

A variable $v$ is fresh for the surrounding context $\Gamma$ when it does not occur free in any undischarged assumption in $\Gamma$. Choose it also distinct from bound variables that would cause variable capture in the intended substitution. The universal quantifier introduction rule isIts justification is that the logical derivation of $\varphi (v)$ used no special information about $v$, so it establishes the property of an arbitrary object. Semantically, changing the assignment of $v$ preserves the truth of $\Gamma$; therefore $\varphi (v)$ holds for every possible assigned object. Without the eigenvariable condition, the assumption $R(v)$ could incorrectly be generalized to $\forall xR(x)$ in an interpretation where only one of two objects satisfies $R$.