2. Condensed Detachment, Principal Types, and Unification

In this section, we summarize some basic definitions and facts about condensed detachment, principal types, and the unification algorithm, which will help to introduce the new rule of inference and the new typing scheme in the section to follow.

2.1 Propositional logic and condensed detachment

In order to facilitate the comparison between condensed detachment and principal types, the considered propositional formulas will be purely implicational. To be more precise, propositional formulas are defined by the simple grammar rule:

(1) \begin{align*} \varphi ::= p\, |\, (\varphi \rightarrow \varphi) \end{align*}

where p ranges over a countable infinite set of propositional variables.

We call the formula $\alpha'$ an alphabetic variant of the formula $\alpha$ if, in order to obtain $\alpha'$ , all or some variables in $\alpha$ have been substituted by variables distinct from each other and distinct from any variables in $\alpha$ which have not been replaced. ^{Footnote 3} A substitution $\sigma$ is called a unifier of the formulas $\alpha$ and $\beta$ if $\sigma(\alpha) = \sigma(\beta)$ . A unifier $\sigma$ of $\alpha$ and $\beta$ is called most general if $\sigma'(\alpha)$ is a substitution instance of $\sigma(\alpha)$ for every other unifier $\sigma'$ of $\alpha$ and $\beta$ . In this case, we call $\sigma(\alpha)$ the most general unification of $\alpha$ and $\beta$ .

The rule $\mathbf{D}$ (condensed detachment) can then be given as:

(D)

where $\gamma'$ is an alphabetic variant of $\gamma$ which has no common variables with $\alpha$ , and where $\sigma$ is a most general unifier of $\alpha$ and $\gamma'$ for which no new variable in $\sigma(\alpha)$ occurs in $\beta$ . ^{Footnote 4} If rule $\mathbf{D}$ can be applied to $\alpha \rightarrow \beta$ and $\gamma$ , we write ${\mathbf{D}(\alpha \rightarrow \beta, \gamma) = \sigma(\beta)}$ . ^{Footnote 5}

As an example for an application of rule $\mathbf{D}$ , let the major premise ${\alpha \rightarrow \beta}$ be ${(a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c))}$ , and let the minor premise $\gamma$ be the formula ${p \rightarrow p}$ . As $\alpha$ and $\gamma$ share no common variables, we can immediately proceed with their actual unification, which is realized by the most general unifier ${\sigma = \left\lbrace a\leadsto(b \rightarrow c), p\leadsto(b \rightarrow c) \right\rbrace}$ . Thus, the resulting formula $\sigma(\beta)$ is ${((b \rightarrow c) \rightarrow b) \rightarrow ((b \rightarrow c) \rightarrow c)}$ .

The representation of the just mentioned formulas as binary trees leads to the picture in Fig. 1, in which the original trees $\alpha$ and $\gamma$ successfully try to grow into the same overall shape or structure. Note how the subtree $\beta$ follows the same “growing rules” as $\alpha$ and $\gamma$ do. Finally, variables in inner nodes will have to be replaced by the implication operator.

Figure 1. Rule $\mathbf{D}$ applied to the major premise $\alpha \rightarrow \beta = (a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c))$ and the minor premise $\gamma = {p \rightarrow p}$ , both represented as binary trees. The resulting formula is $\sigma(\beta) = ((b \rightarrow c) \rightarrow b) \rightarrow ((b \rightarrow c) \rightarrow c)$ .

2.2 Combinatory logic and principal types

Terms of combinatory logic (CL-terms) are built according to the following production rule:

(2) \begin{align*} \varphi ::= \mathsf{S}\, |\, \mathsf{K}\, |\, (\varphi\, \varphi), \end{align*}

the third option being called an application. Example CL-terms are $\mathsf{S}$ , $(\mathsf{K}\mathsf{S})$ , and $((\mathsf{K}\mathsf{K})(\mathsf{K}\mathsf{S}))$ , the last one of which is usually simply written as $\mathsf{K}\mathsf{K}(\mathsf{K}\mathsf{S})$ following an association to the left.

Two rules of weak reduction ^{Footnote 6} can be applied to CL-terms, and while the actual terms can be interpreted as algorithms, it is the reduction rules which bring in the dynamics of the computation. These rules are

(3)

(4)

where the metavariables x, y, and z represent arbitrary CL-terms. Applying these rules, an example reduction leading to what is called an unreducible normal form might look as follows:

The reader should note that we could also have chosen a different reduction path, which, nevertheless, would have led to the same normal form, a property of combinatory logic known as the Church–Rosser property:

\begin{align*} \mathsf{K}(\mathsf{S}\mathsf{K}\mathsf{S}\mathsf{S})\mathsf{K} \rhd \mathsf{S}\mathsf{K}\mathsf{S}\mathsf{S} \rhd \mathsf{K}\mathsf{S}(\mathsf{S}\mathsf{S}) \rhd \mathsf{S} \end{align*}

In typed combinatory logic, principal types can be assigned to certain CL-terms. These types follow the building law given by production rule (1), that is, every type can be interpreted as an implicational proposition. Two axioms assign the principal types ${(a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c))}$ and ${a \rightarrow (b \rightarrow a)}$ (or any other alphabetic variant) to the CL-terms $\mathsf{S}$ and $\mathsf{K}$ , respectively. If two CL-terms M and N with principal types ${\varphi \rightarrow \psi}$ and $\vartheta$ are given, the principal type ${\mathbf{D}(\varphi \rightarrow \psi, \vartheta)}$ , if it exists, is assigned to the application $(M\, N)$ . Otherwise, $(M\, N)$ is regarded as not typable. The typing scheme is summarized in Fig. 2.

Figure 2. Assigning principal types to terms in CL.

As an example, the tree in Fig. 3 assigns the principal type ${(a \rightarrow a)}$ to the CL-term $\mathsf{S}\mathsf{K}\mathsf{K}$ .

Figure 3. A tree assigning the principal type ${(a \rightarrow a)}$ to the CL-term $\mathsf{S}\mathsf{K}\mathsf{K}$ , using two applications of rule (pt). The substitution in the first step is $\left\lbrace a \!\leadsto\! p, b\!\leadsto\! q, c\!\leadsto\! p\right\rbrace$ and in the second step $\left\lbrace p \!\leadsto\! a, q\!\leadsto\! (b \rightarrow a)\right\rbrace $ .

2.3 The unification algorithm

Without going into two many details, we now present a version of the unification algorithm which is based on a variant given in Russell and Norvig (Reference Russell and Norvig2010) and which, in our case, computes a most general unifier of two implicational propositional formulas $\alpha$ and $\beta$ . Basically, Algorithm 1 considers four cases: if $\alpha$ and $\beta$ are equal, the substitution built up so far is returned. If one of the formulas is a variable, the two formulas are passed on to Algorithm 2, unify-var, which unifies the variable with the second formula. Otherwise, the left and right parts of $\alpha$ and $\beta$ , that is, their antecedent and consequent, are recursively unified.

Two things are worth noting about this algorithm. First, unification is “nearly” symmetrical in $\alpha$ and $\beta$ , the only difference between $\alpha$ and $\beta$ which breaks the symmetry being that the test if $\alpha$ is a variable comes before the test if $\beta$ is a variable. Thus, in certain cases, unify $(\alpha, \beta)$ may lead to a result different from the one returned by unify $(\beta, \alpha)$ . ^{Footnote 7} However, it can be shown that the resulting unified formulas are always alphabetic variants of each other. Second, the algorithm is apparently far from being trivial: as Peter Norvig notes (Norvig Reference Norvig1991), many textbooks in the 1980s presented ^{Footnote 8} versions of the algorithm which, for example, failed to unify the formulas ${(a \rightarrow (b \rightarrow a)) \rightarrow (b \rightarrow (a\rightarrow b))}$ and ${p \rightarrow p}$ due to a missing dereferencing clause when unifying variables (lines 3/4 in Algorithm 2).

Algorithm 1 unify(α, β, σ)

Algorithm 2 unify-var(var, β, σ)

3. Pattern Matching, Pattern Detachment, and Pattern Typing

As mentioned in the Introduction, we now shift the focus to the unidirectional sibling of the unification algorithm, which is known as pattern matching. Pattern matching regards one of the given formulas as a fixed and unchangable pattern to which the other formula has to be matched using appropriate variable substitutions. ^{Footnote 9} This asymmetry is reflected in Algorithm 3 (match) by the difference between the clause in lines 5/6 on the one hand and the clause in lines 7/8 on the other hand: if $\beta$ is a variable but $\alpha$ is not, the matching is doomed to fail because $\beta$ is not allowed to grow. Furthermore, Algorithm 4 (match-var) fails if a variable var has to be substituted by an expression $\beta$ , but the substitution built so far already contains a binding ${\left\langle var \!\leadsto\! \gamma\right\rangle}$ for which $\beta \neq \gamma$ holds. In this case, there is no possibility to unify $\beta$ and $\gamma$ .

Algorithm 3 match(α, β, σ)

Algorithm 4 match-var(var, β, σ)

While pattern matching is a widely used technique in Artificial Intelligence and related fields, it does not play an apparent role when it comes to logical rules of inference in propositional logic or to type inference in combinatory logic. In what follows, we take a closer look at the consequences of replacing the unification algorithm by pattern matching as the underlying mechanism of these kinds of inferences. To start with, we define an inference rule $\mathbf{P}$ (pattern detachment) as follows:

(P) \begin{align*} \frac{\alpha \rightarrow \beta \qquad \gamma}{\sigma(\beta)} \end{align*}

Here, if it exists, $\sigma$ is the substitution for which $\sigma(\alpha) = \gamma'$ holds, where $\gamma'$ is an alphabetic variant of $\gamma$ which does not share any variables with $\beta$ . ^{Footnote 10} In this case, we write ${\mathbf{P}(\alpha \rightarrow \beta, \gamma) = \sigma(\beta})$ , otherwise ${\mathbf{P}(\alpha \rightarrow \beta, \gamma)}$ remains undefined. The reader should note that if ${\mathbf{P}(\alpha \rightarrow \beta, \gamma)}$ is defined, then also ${\mathbf{D}(\alpha \rightarrow \beta, \gamma)}$ (condensed detachment) is defined and ${\mathbf{P}(\alpha \rightarrow \beta, \gamma)} = {\mathbf{D}(\alpha \rightarrow \beta, \gamma)}$ holds.

An example of pattern detachment is shown in Fig. 4, where the formulas ${(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a \rightarrow c))}$ and ${(p \rightarrow q) \rightarrow (p \rightarrow q)}$ , both represented as binary trees, lead to the result ${p \rightarrow ((p \rightarrow q) \rightarrow q)}$ , the (most general) unifier being the substitution ${\sigma = \left\lbrace a \leadsto (p \rightarrow q), b \leadsto p, c \leadsto q \right\rbrace }$ .

Figure 4. Rule $\mathbf{P}$ applied to the major premise $\alpha \rightarrow \beta = (a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a \rightarrow c))$ and the minor premise $\gamma = {(p \rightarrow q) \rightarrow (p \rightarrow q)}$ , both represented as binary trees. The resulting formula is $\sigma(\beta) = p \rightarrow ((p \rightarrow q) \rightarrow q)$ . Note that the minor premise $\gamma$ remains in its fixed shape.

When it comes to typed combinatory logic, the notion of pattern typing can be defined exactly as in Fig. 2, the third rule (pt) being replaced by the following rule

If ${\mathbf{P}(\varphi \rightarrow \psi, \vartheta)}$ is not defined, then the CL-term (M N) is not pattern typable. If a CL-term Q is pattern typable, we use the notation ptt(Q) for its pattern type.

As an example for pattern typing, we refer the reader back to Fig. 3, where we simply replace the annotation (pt) by (ptt), stressing the fact that in this example both applications of rule (ptt) regard the type of the combinator $\mathsf{K}$ (the minor premise) as a fixed pattern, to which the antecedent of the types of the combinators $\mathsf{S}$ and $\mathsf{S}\mathsf{K}$ have to be matched. The example demonstrates that every pattern type also is a principal type of its CL-term.

4. Pattern Types and Weak Reduction

It is a widely known fact that weak reduction is capable to change the principal type of a CL-term. To be more precise, if $\varphi$ is the principal type of a CL-term M which weakly reduces to N (i.e., $M \rhd N$ ), then N has a principal type $\psi$ of which $\varphi$ is a substitution instance. ^{Footnote 11} As an example, consider the CL-term $\mathsf{S}\mathsf{K}\mathsf{S}\mathsf{I}$ (where $\mathsf{I}$ abbreviates the term $\mathsf{S}\mathsf{K}\mathsf{K}$ ). This term reduces to $\mathsf{K}\mathsf{I}(\mathsf{S}\mathsf{I})$ . But while the former term has the principal type ${(a \rightarrow b) \rightarrow (a \rightarrow b)}$ , the latter has the principal type ${a \rightarrow a}$ . If we consider CL-terms as programs and a reduction step as part of a computation, then the possible change of the program’s principal type during a computation may well disturb our picture of a type as a way to characterize the input and output of the computation. At this very point, it should be remarkable to note that the pattern type of a CL-term never changes when the term is reduced.

Similar arguments lead us to the structure of the types of y and z, and finally to the pattern type of $\mathsf{S} xyz$ :

As $\mathsf{S} xyz$ reduces to xz(yz), we can now construct the pattern type of the reduct, taking into consideration the appropriate structures of the types of x, y, and z. As we can see, the deduction results in the same pattern type as before:

In case 2, M is the CL-term $\mathsf{K} xy$ , with x and y again denoting CL-terms. For $\mathsf{K} xy$ to be pattern typable, x and y may now have arbitrary pattern types, which we denote as $\sigma_1(a)$ and $\sigma_2(b)$ , respectively. Here, we stipulate that

$\sigma_1$ does not replace any other variables than a,

$\sigma_1(a)$ does not contain the variable b,

$\sigma_2$ does not replace any other variables than b,

which, for example, implies that $\sigma_1(b) = b$ , a fact which is used in the following deduction:

Due to the stipulations concerning the substitutions $\sigma_1$ and $\sigma_2$ , the resulting pattern type is equal to $\sigma_1(a)$ , which is the pattern type of x, which in turn is the reduct of $\mathsf{K} xy$ .

In case 3, M contains one of the redexes $\mathsf{S} xyz$ and $\mathsf{K} xy$ as a proper subterm, which is reduced to obtain the term N. Using structural induction, this case can easily be reduced to the first two cases.

As every pattern type is also a principal type, Theorem 1 identifies a large class of CL-terms which do not change their principal type when being reduced.

At this point, the question may arise how “natural” Theorem 1 is, or, to put it the other way round, one may wonder if the unchanged types in the above proof are just a mere coincidence. A look at other combinators presents a somewhat diffuse picture at first sight: while the combinators $\mathsf{B}$ and $\mathsf{W}$ with reduction rules $\mathsf{B} xyz \rhd x(yz)$ and $\mathsf{W} xy \rhd xyy$ , respectively, preserve pattern types, the combinator $\mathsf{C}$ with reduction rule $\mathsf{C} xyz \rhd xzy$ and pattern type ${(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a \rightarrow c))}$ reveals a somewhat different behavior. Again, we can first determine the types of the terms x, y, and z as follows:

Trying to pattern type the redex xzy then leads to the insight that a pattern type might not exist if $\sigma_3$ is a substitution that modifies the type ${\sigma_2 \circ \sigma_1(b \rightarrow c)}$ :

As an example, we can now consider the term $\mathsf{C}\mathsf{T}\mathsf{I}\mathsf{K}$ with pattern type ${(a \rightarrow (b \rightarrow a))}$ , where $\mathsf{T}$ abbreviates the term $\mathsf{C}(\mathsf{S}\mathsf{K}(\mathsf{S}\mathsf{K}))$ with pattern type ${(a \rightarrow ((a \rightarrow b) \rightarrow b))}$ . It is now easy to see that the reduct $\mathsf{T}\mathsf{K}\mathsf{I}$ is not pattern typable. ^{Footnote 12}

The following theorem characterizes exactly those combinators which guarantee that reduction does preserve pattern types. If M is a combination of terms taken from the set $\left\lbrace x_1, \dots, x_n \right\rbrace$ , index(M) denotes the greatest x-index occuring within M. For example, $index(x_1 x_3 (x_2 x_3)) = 3$ .

Before we move on to the Theorem’s proof, two examples may help to clarify the central point. First, the just regarded combinator $\mathsf{C}$ with reduction rule $\mathsf{C} x_1 x_2 x_3 \rhd x_1 x_3 x_2$ violates the subterm condition in the term $((x_1 x_3) x_2)$ because $index{(x_1 x_3)} > index{(x_2)}$ . Second, the combinator $\mathsf{B}'$ with reduction rule $\mathsf{B}'x_1 x_2 x_3 \rhd x_2(x_1 x_3)$ does indeed guarantee the preservation of pattern types, as can now immediately be read off the indices of the structure $(x_2(x_1 x_3))$ . We now proceed to the proof of Theorem 2.

In the second step, we now consider subterms (MN) of Q with $\underbrace{index(M)}_{=: k} \leq \underbrace{index(N)}_{=: l}$ . By structural induction, we can show that (MN) has pattern type ${\sigma_l \dots \sigma_1(\psi)}$ for some type $\psi$ . As the base case, we consider the subterm $(x_k x_l)$ for two variables $x_k: \sigma_k \dots \sigma_1(\varphi_k)$ and $x_l: \sigma_l \dots \sigma_1(\varphi_l)$ . As $k \leq l$ holds by the assumption of the theorem, we get $(x_k x_l): \sigma_l \dots \sigma_1(\psi)$ . For the induction step, we consider two terms M and N, which, by the induction hypothesis, have pattern types $\sigma_k \dots \sigma_1(\varphi_M)$ and $\sigma_l \dots \sigma_1(\varphi_N)$ , respectively. Again, $k \leq l$ holds, and we conclude that the term (MN) has pattern type $\sigma_l \dots \sigma_1(\psi)$ . In the case of the complete term Q, this is exactly the type of the term $Px_1 \dots x_n$ .

5. The Pattern Model of Untyped Combinatory Logic

Theorem 1 of the preceding section now gives rise to a model of untyped combinatory logic which can be regarded as a simplification of the Fool’s model (Meyer et al. Reference Meyer, Bunder and Powers1991). To start with, we define the notion of a combinatory reduction algebra.

Definition 1 . A combinatory reduction algebra is an algebraic structure ${(\mathcal{A}, \leq, \bullet, s, k)}$ where $\mathcal{A}$ (the domain) is a nonempty set, $\leq$ is a partial order on $\mathcal{A}$ , $\bullet\! : \mathcal{A} \times \mathcal{A} \rightarrow \mathcal{A}$ is a binary operation on $\mathcal{A}$ , and s and k are two distinct elements of $\mathcal{A}$ , and where the following stipulations hold for all $x,y,z \in \mathcal{A}$ :

(5)

(6)

(7)

(8)

Next, we interpret CL-terms (the set of which we denote by $\mathbb{T}$ ) by means of the elements of a combinatory reduction algebra.

Definition 2. A model of untyped combinatory logic is a pair $(\mathfrak{A}, \mathfrak{I})$ where ${\mathfrak{A} = (\mathcal{A}, \leq, \bullet, s, k)}$ is a combinatory reduction algebra, and ${\mathfrak{I}\!: \mathbb{T} \rightarrow \mathcal{A}}$ is a mapping for which the following equalities hold:

(9)

(10)

(11)

In order to introduce the new model, which we will call the pattern model, we first identify propositional formulas which are alphabetic variants of each other. To this end, we use the notation $\left\lbrace \varphi \right\rbrace_\alpha$ to denote the set of all formulas which are alphabetic variants of $\varphi$ . These kind of sets actually form the domain of the pattern model.

Definition 3. The pattern model is the pair $(\mathfrak{P}, \mathfrak{I})$ , where

(12)

(13)

(14)

(15)

(16)

(17)

(18)

A few remarks should be appropriate at this point.

• As defined in (13), the domain $\mathcal{P}$ of $\mathfrak{P}$ can simply be regarded as the set of implicational propositional formulas modulo alphabetic variation. $\mathcal{P}$ thus consists of equivalence classes of formulas which have the same “logical power.” ^{Footnote 14}

• If x and y are elements of the domain $\mathcal{P}$ , $x \subseteq y$ only holds if $x = y$ or $x = \emptyset$ .

• As defined in (15), $x = \emptyset$ or $y = \emptyset$ immediately lead to the fact that $x \bullet y = \emptyset$ . This corresponds to the fact that any CL-term, which has an pattern-untypable subterm, is itself pattern-untypable.

• If both $x \neq \emptyset$ and $y \neq \emptyset$ , then $x \bullet y$ is the result of (possibly) applying rule $\mathbf{P}$ (pattern detachment) to two representatives of the sets x and y, finally collecting the alphabetic variants of the result. ^{Footnote 15}

• Concerning the role of the empty set $\emptyset$ , computer experiments have been able to show that 310,210 out of 397,242 terms – with a maximum of eight applications – are indeed pattern typable and are thus not represented by the empty set.

For stipulation (5), we consider two cases. In the first case, the expression $s \bullet x \bullet y \bullet z$ is equal to the empty set. In this case, set inclusion is trivially fulfilled. Otherwise, one can successfully apply rule $\mathbf{P}$ three times to representatives of the sets s, x, y, and z, yielding a nonempty set of alphabetic variants of a formula $\vartheta$ . But now Theorem 1 guarantees that the expression $x \bullet z \bullet (y \bullet z)$ leads to exactly the same result. Again, set inclusion holds.

For stipulation (7), we also consider two cases. In the first case, $x \subseteq y$ holds because x is the empty set. But in this case, the expression $z \bullet x$ is also equal to the empty set, and thus $z \bullet x \subseteq z \bullet y$ is fulfilled. In the second case, $x \subseteq y$ holds because x and y are equal. But then $z \bullet x$ and $z \bullet y$ are also equal.

In the next step, we show that the interpretaion $\mathfrak{I}$ does indeed give rise to a model. As equalities (9) and (10) obviously hold, we can concentrate on equality (11). This time, we consider three cases. In case 1, at least one of the CL-terms P and Q is not pattern typable. This implies that the application (PQ) is not pattern typable, either. Thus, both sides of the equation evaluate to the empty set. In case 2, both P and Q are pattern typable, but the application (PQ) is not. Again, both sides of the equation yield the empty set, the right-hand side because the sets $\mathfrak{I}(P)$ and $\mathfrak{I}(Q)$ do not contain any formula to which rule $\mathbf{P}$ can be applied. In the third case, P, Q, and (PQ) are pattern typable. Thus, the term $\mathfrak{I}(P) \bullet \mathfrak{I}(Q)$ evaluates exactly to the set of alphabetic variants of the pattern type of the application (PQ).

We conclude this section with a short comparison between the pattern model and the Fool’s model. Details about the latter can be found in Meyer et al. (Reference Meyer, Bunder and Powers1991) and Bimbo (2011, Chapter 6). The Fool’s model can actually be obtained by simply changing Definition 3 as follows:

1. (1) Change the index $\alpha$ to an index s all the way through, where the notation $\left\lbrace \varphi \right\rbrace_s $ represents the set of all substitution instances of $\varphi$ .

2. (2) In (18), change “ptt” and “pattern typable” into “pt” and “principal-typable,” respectively.

The advantages of the pattern model over the Fool’s model now lie at hand: First, the former is based on the very natural domain consisting of propositional formulas (modulo the renaming of variables). Second, two arbitrary CL-terms P and Q with $P \rhd Q$ are always represented by the same object, thus supporting the idea that a computation is not supposed to change its input and output types while running.

6. Major versus Minor Premisses as Fixed Patterns

In this last section, we answer the question why we have decided to consider the minor premise as the fixed and unchangable pattern both in rule $\mathbf{P}$ and in rule (ptt). The main reason is that any proof which also allows for the consideration of the major premise as the fixed pattern can – under certain very “mild” conditions – be transformed into an equivalent proof which uses rule $\mathbf{P}$ only. To be more precise, we first define the following rule $\mathbf{P}'$ , which is applicable if and only if there is a substitution $\sigma$ for which $\sigma(\gamma) = \alpha$ holds:

(P′) \begin{align*} \frac{\alpha \rightarrow \beta \qquad \gamma}{\beta} \end{align*}

Using the notation $\mathbb{A} \vdash_{\mathbf{P}} \varphi$ ( $\mathbb{A} \vdash_{\mathbf{P},\mathbf{P}'} \varphi$ ) for the existence of a proof for $\varphi$ which is based on the axioms $\mathbb{A}$ and rule $\mathbf{P}$ (and rule $\mathbf{P}'$ , resp.), we can now state the following theorem.

We replace this passage by the following structure:

For this structure, we assume that b is a fresh variable with respect to $\alpha, \beta, \gamma$ , and the substitution $\sigma$ . $\sigma'$ is the substitution $\sigma$ , extended by the substitution $\left\lbrace b \!\leadsto\! \beta \right\rbrace $ , that is, ${\sigma' = \sigma \cup \left\lbrace b \!\leadsto\! \beta \right\rbrace }$ . As b does not occur in $\gamma$ , ${\sigma'(\gamma) = \sigma(\gamma)}$ holds.

We finish our considerations with some remarks and open questions concerning the interplay between rules $\mathbf{P}$ and $\mathbf{P}'$ in the presence of the two axioms $(a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c))$ and ${a \rightarrow (b \rightarrow a)}$ , which, on the one hand, form a basis for the implicational fragment of intuitionistic propositional logic, and, on the other hand, serve as types for combinatory logic based on the combinators $\mathsf{S}$ and $\mathsf{K}$ .

• It remains an open question whether the formula $a \rightarrow ((a \rightarrow b) \rightarrow a)$ , which plays such a crucial role in the elimination of rule $\mathbf{P}'$ , can be pattern-proved using the two just mentioned axioms. As computer experiments have shown, none of the CL-terms with less than eight combinators have pattern type $a \rightarrow ((a \rightarrow b) \rightarrow a)$ .

• If the formula $(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a \rightarrow c))$ , which is the principal type of the combinator $\mathsf{C}$ , is added as an axiom, the formula $a \rightarrow ((a \rightarrow b) \rightarrow a)$ can be pattern-proved. It is the pattern type of the CL-term $\mathsf{C} \mathsf{S} \mathsf{K}$ . It remains an open question whether the formula $(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a \rightarrow c))$ is a pattern type for the basis $\mathsf{S}$ and $\mathsf{K}$ . (Again, there is no CL-term with less than eight combinators which serves our purpose.)

• It also remains open whether the combination of rules $\mathbf{P}$ and $\mathbf{P}'$ can replace rule $\mathbf{D}$ , condensed detachment.