A lambda proof of the P − W theorem

Sachio Hirokawa, Yuichi Komori, Misao Nagayama

Abstract

The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B′ = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is affirmative. The first to prove this was E.P. Martin by a semantical method.

In this paper, we give the first proof of Martin’s theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin’s Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λx.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

1 Introduction.

The logical system P-W is an implicational non-commutative intuitionistic logic

defined by axiom schemes

B = (b → c) → (a → b) → a → c,
B′ = (a → b) → (b → c) → a → c,
I = a → a,

with the rules of modus ponens and substitution. Martin’s theorem states the

following:

• If α → β and β → α are provable in P-W, then α = β.

The truth of Martin’s theorem had been an open problem, known as the “P-W

problem” for more than twenty years, since Belnap had originally asked it. Fi-

nally E.P. Martin solved it affirmatively by showing the statement below using

a semantical argument [9]. Powers showed the equivalence between this state-

ment and the original one [11] by essentially obtaining the theory of combinators

generated from B, B′ and I.

• No formula with form α → α is provable in P-W without using the axiom I .

Martin’s theorem means that the logic defined by B and B′ is “progressive” in the sense that a deduction from an assumption α does not return to the start point itself. The deduction creates something new and does not yield the tautology α → α, which would be a “logical nonsense”(cf. Fine and Martin [4]).

Since Martin’s solution was a semantical proof, finding a syntactic proof of the problem attracted some researchers. A syntactic proof in sequent calculus was obtained by the third author originally in June of 1993 ([10]) and the second author in August of 1993 ([7]). Also there have been several attempts to obtain a syntactic proof based on simply typed λ-calculus, where, by means of the Curry-Howard isomorphism, proofs are identified with λ-terms according to the “formulas-as-types” or “terms-as-proofs” correspondence^{1} .

P. Trigg introduced, in [5], a notion of hereditary right-maximality for the combinators generated from B, B′ and I. This notion accommodates a restricted exchange rule introduced by B and B′, where we can exchange the position of the first two arguments but not the position of the third ones. This establishes, via the Curry-Howard isomorphism, the correspondence between proofs in the Hilbert-style formal system and the hereditary right-maximal BB′I-combinators.

The first author adapted this notion to linear λ-terms, where each variable contained in them occurs exactly once. This established, via the Curry-Howard isomorphism, the correspondence between P-W proofs in natural deduction style and hereditary right-maximal linear (HRML) λ-terms [6]. Furthermore, he showed in [6] that the statement below is equivalent to Martin’s theorem.

• Any HRML λ-term of type α → α is βη-reducible to λx.x .

The purpose of the present paper is to prove this theorem. Based on the transformations between P-W proofs in the Hilbert-style formal system and those in the natural deduction style system, we can define transformations between closed linear λ-terms and closed BB′I-combinators in both directions, whose composition is the identity up to βη-equality: a translation of a linear λ-term to a BB′I-combinator is obtained from an abstraction algorithm of basic combinators; in the other direction, a translation of a BB′I-combinator to a linear λ-term is obtained by the replacement of the combinators B, B′ and I by the λ-terms λxyz.x(yz), λxyz.y(xz), and λx.x. In the proof of the main theorem, we use two important properties of a β-reduction with respect to λxyz.x(yz) or λxyz.y(xz): namely, they preserve any subterm of form P (QR), and never create a new η-redex.

1When R. Meyer visited Japan in 1991, he told the first author that he believed in a clear solution to the problem using λ-calculus.

In Section 2, we give definitions and theorems contained in [6], with some sketches of proofs, in order to make the paper self-contained.

In Section 3, we prove the main theorem (Theorem 3).

In Section 4, we derive, directly from the main theorem, Martin’s theorem (Theorem 4) and the other statements due to Powers and Dwyer (Theorems ??, 6).

2 Preliminaries.

We consider B, B′ and I as atomic combinators with the following reduction rules.

\begin{matrix}Bxyz & ▷ & x(yz) \\ B′xyz & ▷ & y(xz) \\ Ix & ▷ & x \end{matrix}

The set Λ(BB′I) is defined as the smallest set containing every variable, the constants B, B′ and I, closed under application and abstraction. Thus the terms in Λ(BB′I) will be mixed combinatory and λ-terms. We mean by a term an element in the set Λ(BB′I).

The variables and the constants B, B′ and I are said to be atomic. A term is closed iff it contains no free variables. A term is a BB′I-term iff it contains no λ’s. A term is a λ-term iff it does not contain B, B′ nor I. We denote the set of free variables in M by F V (M).

Definition 1 (Definition 2. Hirokawa [6]) Let x_{0}, x_{1}, ⋯, x_{n} be a sequence of distinct variables and M be a term. The index of M with respect to x_{0}, x_{1}, ⋯, x_{n} is defined by idx(M, x_{0}x_{1} ⋯ x_{n})

= \{ \begin{matrix}max\{i | 0 ≤ i ≤ n, x_{i} ∈ F V (M)\} + 1 & if x_{i} ∈ F V (M) for some i = 0, ⋯, n, \\ 0 & otherwise. \end{matrix}

Definition 2 (Definition 3. Hirokawa [6]) The set HRM(x_{0}x_{1} ⋯ x_{n}) of hereditary right-maximal terms with respect to x_{0}x_{1}, ⋯, x_{n} is defined as follows.

(1) Every variable and the constants B, B′, I are in HRM(x_{0}x_{1} ⋯ x_{n}).

(2) If M, N ∈ HRM(x_{0}x_{1} ⋯ x_{n}) and idx(M, x_{0}x_{1} ⋯ x_{n}) ≤ idx(N, x_{0}x_{1} ⋯ x_{n}) then (MN) ∈ HRM(x_{0}x_{1} ⋯ x_{n}).

(3) If M ∈ HRM(x_{0}x_{1} ⋯ x_{n}x_{n+1}) and x_{n+1} ın F V (M) then λx_{n+1}.M ∈ HRM (x_{0}x_{1} ⋯ x_{n}).

Definition 3 (Definition 4. Hirokawa [6]) A closed λ-term λx_{0}x_{1} ⋯ x_{n}.M is said to be hereditary right-maximal iff F V (M) = {x_{0}, x_{1}, ⋯, x_{n}} and M ∈ HRM(x_{0}x_{1} ⋯ x_{n}).

We note that when xM_{1} ⋯ M_{m} ∈ HRM(x_{0}x_{1} ⋯ x_{n}), we have

idx(x, x_{0}x_{1} ⋯ x_{m}) ≤ idx(M_{1}, x_{0}x_{1} ⋯ x_{m}) ≤ ⋯ ≤ idx(M_{m}, x_{0}x_{1} ⋯ x_{m}).

Definition 4 (Definition 5. Hirokawa [6]) The set of linear terms is defined by induction thus:

(1) every variable and the constants B, B′, I are linear,

(2) (MN) is linear if M, N are linear and F V (M) ∩ F V (N) is empty.

(3) (λx.M) is linear if M is linear and x occurs free in M.

The set of closed hereditary right-maximal linear λ-terms is denoted by HRML.

Based on the transformations between the P-W proofs in the Hilbert-style system and those in the natural deduction style system, we can define transformations between closed linear λ-terms and closed BB′I-combinators in both directions, whose composition is the identity up to the βη-equality. Firstly, we define a transformation from a closed HRML linear λ-term M to a closed BB′I-combinator M^{+}.

Definition 5 (Definition 6. Hirokawa [6]) Let x_{0}x_{1}, ⋯, x_{n}, x_{n+1} be a sequence of distinct variables (n ≥ −1), M be a linear BB′I-term in HRM(x_{0}x_{1} ⋯ x_{n}x_{n+1}) and x_{n+1} ∈ F V (M). Then we define a linear term λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.M as follows.

λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.x_{n+1} = I λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.P x_{n+1} = P

λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.P Q = \{ \begin{matrix}BP (λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.Q) & if idx(P, x_{0}x_{1} ⋯ x_{n}) ≤ idx(Q, x_{0}x_{1} ⋯ x_{n}) \\ B′(λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.Q)P & if idx(P, x_{0}x_{1} ⋯ x_{n}) > idx(Q, x_{0}x_{1} ⋯ x_{n}) \end{matrix}

Definition 6 (Definition 7. Hirokawa [6]) Let x_{0}, x_{1}, ⋯, x_{n} be a sequence of distinct variables and X ∈ Λ(BB′I) be a linear term in HRM(x_{0}x_{1} ⋯ x_{n}). Then we define a linear BB′I-term (x_{0}x_{1} ⋯ x_{n}; X)^{∗} in HRM(x_{0}x_{1} ⋯ x_{n}) as follows.

(x_{0}x_{1} ⋯ x_{n}; X)^{∗} = X if X is atomic.
(x_{0}x_{1} ⋯ x_{n}; P Q)^{∗} = (x_{0}x_{1} ⋯ x_{n}; P)^{∗}(x_{0}x_{1} ⋯ x_{n}; Q)^{∗}
(x_{0}x_{1} ⋯ x_{n}; λy.R)^{∗} = λ_{y}^{x_{0}x_{1}···x_{n}}.(x_{0}x_{1} ⋯ x_{n}y; R)^{∗}

These definitions are well-defined [6]. Under the Curry-Howard isomorphism, a BB′I-term (x_{0}x_{1} ⋯ x_{n}; X)^{∗} represents a Hilbert-style proof with types of x_{0}, x_{1}, ⋯, x_{n} as hypotheses ordered in this way. In particular, for a closed λterm M, it can be shown that F V ((; M)^{∗}) = F V (M) = ∅, that is, (; M)^{∗} is a closed BB′I-term [6].

Definition 7 (Definition 8. Hirokawa [6]) Given a closed HRML λ-term M, we define M^{+} as (; M)^{∗}.

Now we define a transformation from a closed BB′I-combinator M to a closed HRML linear λ-term M^{⋄}:

Definition 8 (Definition 9. Hirokawa [6]) Given a term M ∈ Λ(BB′I), a closed λ-term M^{⋄} is defined inductively by x^{⋄} = x, B^{⋄} = λxyz.x(yz), B′^{⋄} = λxyz.y(xz), I^{⋄} = λx.x, (P Q)^{⋄} = (P^{⋄}Q^{⋄}) and (λx.R)^{⋄} = λx.R^{⋄}.

Theorem 1 (Theorem 2. Hirokawa [6]) For a closed HRML λ-term M, M^{+⋄} =^{βη} M.

Proof. We can prove (x_{0}x_{1} ⋯ x_{n}; M)^{∗⋄} =^{βη} M^{⋄} by induction on M. By letting n = −1, we obtain the theorem.

Theorem 2 (Theorem 3. Hirokawa [6]) For a closed HRML λ-term M in βnormal form, (1),(2) and (3) are equivalent.

1. M ⟶^{η} ⟶ λx.x.

2. M^{+} contains an I.

3. The η-normal form of M does not contain a subterm of the form P (QR).

Proof. (1) ⇒ (2): We can prove that for any term P and Q, if P ⟶^{η} ⟶ Q then (x_{0}x_{1} ⋯ x_{n}; P)^{∗} = (x_{0}x_{1} ⋯ x_{n}; Q)^{∗}, by induction on the length of the ηreduction. Thus M ⟶^{η} ⟶ λx.x implies that M^{+} = (; M)^{∗} = (; λx.x)^{∗} = λ_{x}.x = I.

(2) ⇒ (1): Let M = λx_{0} ⋯ x_{n}.xM_{0} ⋯ M_{m} (n ≥ 0). Then

M^{+} = λ_{x_{0}}λ_{x_{1}}^{x_{0}} ⋯ λ_{x_{n}}^{x_{0}x_{1}···x_{n−1}}. (x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗}.

Now we can prove that for a β-normal form linear λ-term N in HRM(x_{0}x_{1} ⋯ x_{n}) satisfying F V (N) ⊆ {x_{0}x_{1}, ⋯, x_{n}} that if N is not an abstraction, then (x_{0}x_{1} ⋯ x_{n}; N)^{∗} does not contain an I, by induction on N. Hence (x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗} does not contain an I. Let i be the first i such that an I occurs as the result of the abstraction λ_{x_{i}}^{x_{0}x_{1}···x_{i−1}}.X where

X = λ_{x_{i+1}}^{x_{0}x_{1}···x_{i}} ⋯ λ_{x_{n}}^{x_{0}x_{1}···x_{n−1}}. (x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗}.

We can show that for a linear combinator X in HRM(x_{0}x_{1} ⋯ x_{n}x_{n+1}) not containing λ and I, if x_{n+1} ∈ F V (X) and λ_{x_{n+1}}^{x_{0}x_{1}···x_{n}}.X contains an I then X = x_{n+1} by induction on X. Hence we have X = x_{i}. On the other hand, we have F V (X) = {x_{0}, x_{1}, ⋯, x_{i}}. Therefore i = 1 and we have

λ_{x_{1}}^{x_{0}}λ_{x_{2}}^{x_{0}x_{1}} ⋯ λ_{x_{n}}^{x_{0}x_{1}···x_{n−1}}.(x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗} = x_{0}.

Note that x_{0}x_{1} is the unique term that yields x_{0} as the result of abstraction λ_{x_{1}}^{x_{0}}. Thus we have

λ_{x_{2}}^{x_{0}x_{1}}λ_{x_{3}}^{x_{0}x_{1}x_{2}} ⋯ λ_{x_{n}}^{x_{0}x_{1}···x_{n−1}}.(x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗} = x_{0}x_{1}.

Similarly we have

λ_{x_{3}}^{x_{0}x_{1}x_{2}} ⋯ λ_{x_{n}}^{x_{0}x_{1}···x_{n−1}}.(x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗} = x_{0}x_{1}x_{2}.

Continuing this argument, we have

(x_{0} ⋯ x_{n}; xM_{0} ⋯ M_{m})^{∗} = x_{0}x_{1}x_{2} ⋯ x_{n}.

On the other hand, we have

(x_{0} ⋯ x_{n}; xM_{1} ⋯ M_{m})^{∗} = x(x_{0}x_{1} ⋯ x_{n}; M_{0})^{∗} ⋯ (x_{0}x_{1} ⋯ x_{n}; M_{m})^{∗}.

Thus we have x = x_{0}, m = n − 1 and (x_{0}x_{1} ⋯ x_{n}; M_{i})^{∗} = x_{i+1} for each 0 ≤ i ≤ n − 1. It follows that

M = λx_{0}x_{1} ⋯ x_{n}.x_{0}M_{0} ⋯ M_{n−1} ⟶^{η} ⟶ λx_{0}x_{1} ⋯ x_{n}.x_{0}x_{1} ⋯ x_{n} ⟶^{η} ⟶ λx_{0}.x_{0}.

Finally we can prove that for a linear λ-term M in β-normal form contained

in HRM(x_{0}x_{1} ⋯ x_{n}), if (x_{0}x_{1} ⋯ x_{n}; M)^{∗} = x_{i} then M ⟶^{η} ⟶ x_{i} by induction on

M, from which the claim holds.

(3) ⇒ (1): Let M be a β-normal form linear λ-term in HRM(x_{0}x_{1} ⋯ x_{n}) such that F V (M) = {x_{0}, x_{1}, ⋯, x_{n}} and the η-normal form of M does not contain any subterm of the form P (QR). We can prove by induction on the number of λ’s of M, that M ⟶^{η} ⟶ x_{0}x_{1} ⋯ x_{n}.

3 Proof of the main theorem.

Now we prove the main theorem of this paper, without using Martin’s Theorem.

Theorem 3 (Main theorem.) If a closed hereditary right-maximal linear λterm has type α → α, then it is βη-reducible to λx.x.

Proof. Let M be a closed HRML λ-term of the type α → α. We prove the theorem by induction on the size | α | of the type α, which is the total number of occurrences of type variables in α. Since M is linear, M has a βη-normal form M′. Base Step. α = a is a type variable. Since M′ is closed, M′ has the form M′ = λx.N and the type assignment for M′ : a → a has the following form.

x : a ; ⋮ . ; N : a ; λx.N : a → a

Since a is a type variable, N is not a λ-abstraction. Since F V (N) = {x}, N = xN_{1} ⋯ N_{m}. Since the predicate of x : a is a type variable, we have m = 0. Hence N = x. Thus we have M ⟶^{βη} ⟶ M′ = λx.x.

Induction Step. Let M′ = λx_{0}x_{1} ⋯ x_{n}.x_{k}M_{1} ⋯ M_{m} be the βη-normal form of M. Then the type assignment for M′ : α → α has the following form.

\begin{matrix}x_{k} : \overbrace{ξ_{1} → ⋯ → ξ_{m} → γ}^{α_{k}} & M_{1} : ξ_{1} & ⋯ & M_{m} : ξ_{m} \\ x_{k}M_{1} ⋯ M_{m} : γ \end{matrix} ; λx_{0}x_{1} ⋯ x_{n}.x_{k}M_{1} ⋯ M_{m} : α → \underbrace{α_{1} → ⋯ → α_{n} → γ}_{α}

Here α_{k} = ξ_{1} → ⋯ → ξ_{m} → γ and α = α_{1} → ⋯ → α_{n} → γ. Case 1. m = 0. Then M′ = λx_{0}x_{1} ⋯ x_{n}.x_{k}. Since M′ is closed and linear, it follows that n = k = 0. Hence M′ = λx_{0}.x_{0} and Theorem holds. Case 2. m ≠ 0. Subcase 2.1 n = 0. Then k = 0 and M′ = λx_{0}.x_{0}M_{1} ⋯ M_{m}. Since M′ is closed and linear, M_{1}, ⋯, M_{m} are closed λ-terms. Therefore idx(M_{1}, x_{0}) = ⋯ = idx(M_{m}, x_{0}) = 0. On the other hand, we have 1 = idx(x_{0}, x_{0}) ≤ idx(M_{1}, x_{0}) ≤ ⋯ ≤ idx(M_{m}, x_{0}) by the hereditary right-maximality of M′. A contradiction. Therefore this subcase does not happen. Subcase 2.2 n ≠ 0. Subcase 2.2.1 k = 0. Then α_{k} = α. Therefore

ξ_{1} → ⋯ → ξ_{m} → γ = α_{1} → ⋯ → α_{n} → γ.

Hence m = n and ξ_{i} = α_{i}(i = 1, ⋯, n). By the right-maximality of M′, we have 1 = idx(x_{0}, x⃗) ≤ idx(M_{1}, x⃗) ≤ ⋯ ≤ idx(M_{m}, x⃗), where x⃗ is x_{0}x_{1} ⋯ x_{n}. Since 1 ≤ idx(M_{i}, x⃗), the index is attained by a variable in x_{0}, x_{1}, ⋯, x_{n} and M_{i} contains such a free variable. Since M′ is linear, each variable occurs exactly once. Thus we have idx(M_{1}, x⃗) < ⋯ < idx(M_{n}, x⃗). Therefore F V (M_{i}) = {x_{i}}(i = 1, ⋯, n). Thus we have λx_{i}.M_{i} : α_{i} → α_{i}. By induction hypothesis for α_{i}, we have λx_{i}.M_{i} ⟶^{βη} ⟶ λx_{i}.x_{i}. Since M′ is in βη-normal form, so is M_{i}. Therefore M_{i} = x_{i}. Thus we have M′ = λx_{0}x_{1} ⋯ x_{n}.x_{0}x_{1} ⋯ x_{n}. This contradicts that M′ is in η-normal form. Thus this subcase does not happen. Subcase 2.2.2 k ≠ 0. Since M′ is linear, x_{0} occurs in some M_{j}. Subcase 2.2.2.1 F V (M_{j}) = {x_{0}}. Then idx(M_{j}, x_{0}x_{1} ⋯ x_{n}) = 1. This contradicts k + 1 = idx(x_{k}, x⃗) ≤ idx(M_{1}, x⃗) ≤ ⋯ ≤ idx(M_{j}, x⃗). Therefore this subcase does not happen. Subcase 2.2.2.2 F V (M_{j}) ⊃ {x_{0}}. Let F V (M_{j}) = {x_{0}, x_{j_{1}}, ⋯, x_{j_{q}}} with 0 < j_{1} < ⋯ < j_{q}, 1 ≤ q. Let Y = λx_{0}x_{j_{1}} ⋯ x_{j_{q}}.M_{j}. Then Y is a closed HRML λ-term and has the following type assignment.

{M_{j} : ξ_{j} \atop Y = λx_{0}x_{j_{1}} ⋯ x_{j_{q}}.M_{j} : α → \underbrace{α_{j_{1}} → ⋯ → α_{j_{q}} → ξ_{j}}_{δ}}

Here δ = α_{j_{1}} → ⋯ → α_{j_{q}} → ξ_{j}. Then we see that | δ |<| α | as follows. Since α_{k} = ξ_{1} → ⋯ → ξ_{j} → ⋯ → ξ_{m} → γ, ξ_{j} is a proper subtype of α_{k}. Therefore

| δ |=| α_{j_{1}} | + ⋯ + | α_{j_{q}} | + | ξ_{j} |<| α_{j_{1}} | + ⋯ + | α_{j_{q}} | + | α_{k} | .

Since M′ is linear, x_{k} occurs exactly once. Therefore x_{j_{1}}, ⋯, x_{j_{q}}, x_{k} are distinct variables among x_{1}, ⋯, x_{n}. Hence

| α_{j_{1}} | + ⋯ + | α_{j_{q}} | + | α_{k} | ≤| α_{1} | + ⋯ + | α_{n} |
<| α_{1} | + ⋯ + | α_{n} | + | γ |
<| α | .

Therefore | δ |<| α |. Subcase 2.2.2.2.1 M_{j} does not contain a subterm of the form P (QR). Then Y = λx_{0}.x_{0} by Theorem 2. This contradicts that q ≥ 1. Thus this subcase does not happen. Subcase 2.2.2.2.2 M_{j} contains a subterm of the form P (QR). Then Y = λx_{0}x_{j_{1}} ⋯ x_{j_{q}}.M_{j} contains P (QR), and is a closed HRML λ-term in β-normal form. Let X = λyx_{1} ⋯ x_{n}.x_{k}M_{1} ⋯ (yx_{j_{1}} ⋯ x_{j_{q}}) ⋯ M_{m}. Then X contains a subterm of the form P (QR), and is a closed HRML λ-term in β-normal form and has the following type assignment.

\begin{matrix}x_{k} : ξ_{1} → ⋯ → ξ_{m} → γ & ⋯ & \begin{aligned}y : δ & x_{j_{1}} : α_{j_{1}} & ⋯ & x_{j_{q}} : α_{j_{q}} \\ & yx_{j_{1}} ⋯ x_{j_{q}} : ξ_{j} \end{aligned} & ⋯ & M_{m} : ξ_{m} \\ x_{k}M_{1} ⋯ (yx_{j_{1}} ⋯ x_{j_{q}}) ⋯ M_{m} : γ \end{matrix} ; X = λyx_{0} ⋯ x_{n}.x_{k}M_{1} ⋯ (yx_{j_{1}} ⋯ x_{j_{q}}) ⋯ M_{m} : δ → \underbrace{α_{1} → ⋯ → α_{n} → γ}_{α}

By Theorem 2, X^{+} and Y^{+} consist only of B and B′. Let Z be λx.Y (Xx). This is a closed HRML λ-term of type δ → δ. Moreover, Z^{+} consists only of B and B′. Since Z^{+⋄} consists only of B^{⋄} and B^{′⋄}, it is in η-normal form and contains a subterm of the form P (QR). Now we use two important properties of β-reductions with respect to B^{⋄} = λxyz.x(yz) and B^{′⋄} = λxyz.y(xz): namely, they preserve any subterm of form P (QR), and never create a new η-redex. Therefore Z^{+⋄} −̸→^{βη} ⟶ λx.x. Hence by Theorem 1, Z −̸→^{βη} ⟶ λx.x, which, however, contradicts to the induction hypothesis ^{2}. Thus this subcase does not happen.

4 Proof of Martin’s Theorem by λ-calculus.

Now we prove Martin’s theorem as a corollary to Theorem 3.

Theorem 4 (Martin and Meyer [9] ) If both α → β and β → α are provable in P-W, then α = β.

Proof. Under the assumption that formulas α → β and β → α are provable in P-W, we choose closed HRML λ-terms M and N in β-normal form of type α → β and β → α, respectively. If neither M^{+} nor N^{+} contains I, by defining Z as λx.N(Mx) of type β → β, we obtain a contradiction to Theorem 3 by exactly following the argument in Subcase 2.2.2.2.2. Therefore either M^{+} or N^{+} contains an I, hence by Theorem 2, α = β holds.

Now we directly derive, from Theorem 3, the statement due to Powers, known as being equivalent to Martin’s theorem.

Theorem 5 No formula of the form α → α is provable in P-W without I.

Proof. Under the assumption that formula α → α is provable in P-W, there exists a BB′-combinator X of type α → α. Therefore a closed HRML λ-term X^{⋄} has type α → α, and, by Theorem 3, X^{⋄} ⟶^{βη} ⟶ λx.x. However, since X^{⋄} is made of B^{⋄} = λxyz.x(yz) and B^{′⋄} = λxyz.y(xz), a subterm of the form P (QR) remains after any reduction. A contradiction. Therefore α → α is not provable in P-W without I.

Finally, we directly derive, from Theorem 3, the statement due to Powers and Dwyer, known as being equivalent to Martin’s theorem.

Theorem 6 α → β is provable in P-W without I iff α → β is provable in P-W and α ≠ β.

Proof. The only-if-part is immediate from Theorem 5. So, it suffices to prove the if-part. Under the assumption that formula α → β is provable in P-W and α ≠ β we choose a closed HRML λ-term M in β-normal form such that M : α → β. If the translated BB′I-combinator M^{+} contains an I, then Mηarrowλx.x by Theorem 2. This contradicts α ≠ β. Therefore M^{+} does not contain I. Thus M^{+} is made of B and B′. Therefore α → β is provable in P-W without I.

2We can obtain a contradiction also by the characterization theorem for λη-invertibility (Barendregt [2], Dezani [3]) as follows: Since X is linear and contains P (QR), X is not a finite hereditary permutation. Thus X is not λη-invertible. Hence in particular, Z = λx.Y (Xx)

⟶^{βη} ⟶λx.x. But Z is of type δ → δ, which contradicts to the induction hypothesis.

Acknowledgements

The authors are deeply indebted to R. Meyer, M. Dezani and R. Hindley for their encouragement on this subject, and for careful reading of the earlier versions of the manuscript.

References

[1] A.R. Anderson and N.D. Belnap Jr., Entailment, vol. 1, Princeton University Press, Princeton, N.J., 1975.

[2] H. Barendregt, The Lambda Calculus, Second Edition, North-Holland, Amsterdam, 1984.

[3] M. Dezani-Ciancaglini, Characterization of normal forms possessing inverse in the λ-β-η calculus, Theoretical Computer Science, vol. 2 (1976) pp.323– 337.

[4] K. Fine and E. P. Martin, Progressive Logic – the conjunction case, manuscript, October 13, 1994.

[5] P. Trigg, J.R. Hindley and M.W. Bunder, Combinatory abstraction using B,B’ and friends, Theoretical Computer Science, vol. 135 (1994) pp. 405-422.

[6] S. Hirokawa, The proof of α → α in P-W, Journal of Symbolic Logic, vol. 61 (1996) pp.195–221.

[7] Y. Komori, Syntactic Investigations into BI Logic and BB’I Logic, Studia Logica, vol. 53 (1994) pp. 397–416.

[8] A. Kron, A constructive proof of a theorem in relevant logic, Zeitschr. f. math. Logik und Grundlagen d. Math., vol. 31 (1985) pp.423 – 430.

[9] E.P. Martin and R.K. Meyer, Solution to the P-W problem, Journal of Symbolic Logic. vol. 47 (1982) pp.867–887.

[10] M. Nagayama, Normalization theorem for P-W, Bulletin of the Section of Logic vol. 28 (1999) pp.83-85.

[11] L. Powers, On P-W, The Relevance Logic Newsletter, vol.1 (1976), pp.131-142.

Sachio Hirokawa  Yuichi Komori  Misao Nagayama
Computer Center  Department of Mathematics Department of Mathematics
Kyushu University Faculty of Science Tokyo Woman’s Christian
Chiba University  University
Hakozaki 6-10-1 Yayoi-cho 1-33, Inage-ku Zempuku-ji 2-6-1, Suginami
Fukuoka 812-8581, JAPAN Chiba 263-8522, JAPAN  Tokyo 167-8585, JAPAN
hirokawa@cc.kyushu-u.ac.jp komori@math.s.chiba-u.ac.jp misao@twcu.ac.jp

Footnote. 1. When R. Meyer visited Japan in 1991, he told the first author that he had been believing in clear solution to the problem using λ-calculus.

2.We can obtain a contradiction also by the characterization theorem for ληinvertibility (Barendregt [2], Dezani [3]) as follows: Since X is linear and contains P (QR), X is not a finite hereditary permutation. Thus X is not ληinvertible. Hence in particular, Z = λx.Y (Xx) −̸→^{βη} ⟶λx.x. But Z is of type δ → δ, which contradicts to the induction hypothesis.