Uniqueness of normal proofs of minimal formulas

Makoto Tatsuta

Research Institute of Electrical Communication, Tohoku University, 2-1-1 Katahira, Sendai 980, JAPAN e-mail: tatsuta@riec.tohoku.ac.jp

Abstract

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the followings: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.

1 Introduction

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. The minimality was defined first in [5]. [5] proposed the following 2 problems:

1. Is a βη-normal proof of a minimal formula in BCK logic unique?

2. Is a βη-normal proof of a minimal formula in NJ unique?

The first problem has been solved already. For BCK logic, it has been proved that a β-normal proof of a minimal formula is unique [3]. This result brought the following rich results in BCK logic [6]:

• In BCK logic, the structure of all the normal proofs of a formula A is determined by all the minimal formulas which are smaller than the formula A.

• Especially, the number of normal proofs of a formula is always finite in BCK logic.

Therefore the second problem for NJ case is very interesting. Moreover the following problem for NK case is also interesting.

3. Is a βη-normal proof of a minimal formula in NK unique?

In this paper, we attack the problems for NJ case and NK case. The answers are only partially positive and negative in general.

The depth |A| of a formula A is defined as |α| = 0 for a variable α and |A → B| = max(|A| + 1, |B|). Since a formula of small depth has simple structure, we expect a minimal formula of small depth has the unique normal proof. We prove that this holds for a minimal formula of depth 2 for NJ case.

On the other hand, we found counterexamples of formula of large depth for the problems for both NJ and NK cases. Since the counterexample we found first was so large, it is interesting to find the limitation of the depth.

Some procedures of reducing the depth of a formula preserving provability are known. Moreover some procedure also preserves equivalence of proofs [7]. In this paper, we present one of such procedures and prove that it preserves the minimality of a formula and equivalence of proofs. By this procedure, we get counterexamples of depth 3 for both NJ and NK cases.

Combining these results, we get a classification of minimal formulas having the unique normal proof by the depth of formulas.

Note that the classification by the number of variables occurring in a formula is already known: If the number of each variable occurring in a formula A is 1 or 2, then a normal proof of A is unique. In this paper, we try to classify minimal formulas having the unique normal proof by the depth of a formula.

Section 2 gives basic definitions and proposes the uniqueness problems. In Section 3, we prove the uniqueness for a formula of depth 2. Section 4 presents counterexamples for the uniqueness problems. In Section 5, we give a procedure for reducing the depth of a formula and counterexamples of a formula of depth 3.

2 Problems

In this section, we give basic definitions and problems to solve.

Definition 2.1. (Formula)

1. α is a formula if α is a propositional variable.

2. A → B is a formula if A and B are formulas.

Notation 2.2.

We use α, β, … for propositional variables and A, B, … for formulas.

We suppose that → is right associative.

Definition 2.3. (Implicational logic NJ and NK)

We use only the formulas defined above, called implicational formulas. We use the natural deduction style [8]. Intuitionistic implicational logic NJ has no axioms and has only the following two inference rules.

{(l) \atop A} ; ⋮ . ; B ; A → B (→I)(l)  \begin{matrix}A → B & A \\ B \end{matrix} (→E)

Classical implicational logic NK is defined as NJ + (((A → B) → A) → A), that is, a theory NJ having the Pierce’s formulas as axioms.

Definition 2.4. (Identity of proofs)

For proofs π_{1}, π_{2}, we write π_{1} ≡ π_{2} if π_{1} and π_{2} are syntactically identical modulo renaming of discharging labels.

Definition 2.5.

For a formula A and a sequence Γ of formulas, Γ ⊢NJ A denotes that A has a proof of NJ under the assumption of formulas in Γ. Γ ⊢NK A denotes that A has a proof of NK under the assumption of formulas in Γ.

We write simply Γ ⊢ A omitting NJ and NK if it is clear from the context. If Γ is empty, we write simply ⊢ A.

Definition 2.6. (Normalization of a proof, β-normal proof, η-normal proof) A β-redex of a proof is the following form:

\begin{matrix}{⋮ . π \atop B} ; A → B (→I) & ⋮ . ; A \\ B \end{matrix} (→E)

A β-contraction replaces the above β-redex with the following form in a proof:

{⋮ . π \atop B}

If we get a proof π_{2} from a proof π_{1} by a β-contraction, we write π_{1} ▷_{1β} π_{2}. If we get a proof π_{2} from a proof π_{1} by a finite sequence of β-contractions, we say that π_{1} reduces to π_{2} by β-reduction and it is denoted by π_{1} ▷_{β} π_{2}. If a proof π does not have any β-redex, π is called β-normal.

An η-redex of a proof is the following form:

\begin{matrix}\begin{matrix}{⋮ . π \atop A → B} & {(l) \atop A} \\ B \end{matrix} & (→E) \\ A → B \end{matrix} ; (→I)(l)

An η-contraction replaces the above η-redex with the following form in a proof:

{⋮ . π \atop A → B}

If we get a proof π_{2} from a proof π_{1} by an η-contraction, we write π_{1} ▷_{1η} π_{2}. If we get a proof π_{2} from a proof π_{1} by a finite sequence of η-contractions, we say that π_{1} reduces to π_{2} by η-reduction and it is denoted by π_{1} ▷_{η} π_{2}. If a proof π does not have any η-redex, π is called η-normal.

A proof π is a βη-normal proof if π is a β-normal proof and an η-normal proof.

=_{βη} is defined from ▷_{β} and ▷_{η} in a usual way [1].

Definition 2.7. (Substitution)

For formulas A, B, we write A ≡ B if A and B are syntactically identical.

A substitution maps propositional variables to formulas. For a substitution θ, a formula A and a proof π, Aθ and πθ represent A and π respectively where propositional variables are replaced by the corresponding formulas to which θ map the propositional variables.

For formulas A, B, we write A ≤ B or B ≥ A to denote that there exists a substitution θ such that Aθ ≡ B. We write A < B or B > A to denote that A ≤ B holds but B ≤ A does not hold.

For proofs π_{1}, π_{2}, we write π_{1} ≤ π_{2} or π_{2} ≥ π_{1} to denote that there exists a substitution θ such that π_{1}θ ≡ π_{2}. We write π_{1} < π_{2} or π_{2} > π_{1} to denote that π_{1} ≤ π_{2} holds but π_{2} ≤ π_{1} does not hold.

Note that the relation ≤ for formulas and proofs is a preorder.

Definition 2.8. (Minimal formula)

A formula A is a minimal formula of NJ if the following conditions hold.

1. ⊢NJ A.

2. For any formula B, if ⊢NJ B and B ≤ A, then B ≥ A.

A formula A is a minimal formula of NK if the following conditions hold.

1. ⊢NK A.

2. For any formula B, if ⊢NK B and B ≤ A, then B ≥ A.

Problem 2.9.

If a formula A is minimal of NJ and has βη-normal proofs π_{1} and π_{2} in NJ, then does π_{1} ≡ π_{2} hold?

Problem 2.10.

If a formula A is an minimal formula of NK and has βη-normal proofs π_{1} and π_{2} in NK, then does π_{1} ≡ π_{2} hold?

Problem 2.9 was proposed first in [5].

Notation 2.11.

We use notations of type theory for simplicity by Curry-Howard isomorphism [4] and identify the corresponding notations. Especially a proof π of A_{1},…, A_{n} ⊢ A corresponds to a term t such that x_{1} : A_{1},…, x_{n} : A_{n} ⊢ t : A and we identify π with t. In this paper, we suppose that each variable x of a term has a fixed type. We write x^{A} when we show the type A of the variable x explicitly.

3 Minimal formulas of depth 2

In this section, we prove that the answer to the problem given in Section 2 is positive for a formula of depth 2.

Definition 3.1. (Depth of a formula)

We define the depth |A| of a formula A as follows:

|α| = 0,

|A → B| = max(|A| + 1, |B|).

Theorem 3.2.

In NJ, if A is a minimal formula and |A| ≤ 2, A has the unique β-normal proof.

Definition 3.3.

For a formula A, we define the variable core(A) as follows:

1. core(α) = α.

2. If core(B) = α, then core(A → B) = α.

For a sequence Γ of formulas, |Γ| is defined as the maximum of |A_{1}|,…, |A_{n}| where Γ ≡ A_{1},…, A_{n}.

For a term t, head(t) is defined as x where t ≡ xt_{1} … t_{n}, x is a variable and t_{1},…, t_{n} are terms. For terms u,v, u ∈ v denotes that a term u is a subterm of a term v. For sequences Γ, Γ′ of formulas, formulas A, A′, (Γ, A) ≤ (Γ′, A′) denotes that there exists

some substitution σ such that σ substitutes a formula for a variable and Γσ ≡ Γ′ and Aσ ≡ A′. (Γ, A) < (Γ′, A′) denotes that (Γ, A) ≤ (Γ′, A′) and (Γ, A) ≱ (Γ′, A′). For a sequence Γ of formulas and a formula A, (Γ, A) is minimal iff (Γ, A) is minimal in all the (Γ′, A′) such that Γ′ ⊢ A′ holds with respect to the substitution relation ≤.

Let Γ ≡ x_{1} : A_{1},…, x_{n} : A_{n}. Then Γ̃ denotes A_{1},…, A_{n}. A core of Γ means core(A_{i}) (1 ≤ i ≤ n). |Γ| denotes |Γ̃|.

For a term t, |t| denotes the length of a term t. A term t is called λ-free if t does not include λ-abstractions.

Remark 3.4.

(1) If (Γ̃, A) is minimal and Γ ⊢ t : A, then a principal typing-scheme Γ |⊢ t : A holds [2].

(2) Assume that a principal typing-scheme Γ |⊢ t : A holds for any t whenever Γ ⊢ t : A. Then (Γ̃, A) is minimal.

(3) (Γ̃, A) is not necessarily minimal even if a principal typing-scheme Γ |⊢ t : A holds for some t. A counterexample is |⊢ λxy.x(xy) : (α → α) → (α → α).

Lemma 3.5.

If Γ ⊢ t : A, |Γ| ≤ 1, t is λ-free, x^{B} ∈ t and |B| = 1, then one of the following (1) and (2) holds.

(1) x ≡ head(t).

(2) There is a subterm u of t such that x ≡ head(u) and Γ ⊢ u : core(B).

Proof 3.6.

By induction on t. □

Lemma 3.7.

If Γ ⊢ t : A, t is β-normal, |Γ| ≤ 1 and |A| = 0, then t is λ-free.

Proof 3.8.

By induction on t. □

Proposition 3.9.

Suppose that (Γ̃, A) is minimal, |Γ| ≤ 1 and |A| = 0. Then each core of Γ is distinct, that is, if x^{B} : B and x^{C} : C are in Γ and B ≢ C, then core(B) ≢ core(C).

Proof 3.10.

There exists a β-normal term t such that Γ |⊢ t : A. By Lemma 3.7, t is λ-free. Assume that x^{B} : B, x^{C} : C, B ≢ C, core(B) ≡ core(C).

The case that x^{B} ∉ t and the case that x^{C} ∉ t are easy and we omit them here.

Suppose that x^{B} ∈ t and x^{C} ∈ t.

If |B| = 1, by Lemma 3.5 and |A| = 0, we have u such that u ∈ t, head(u) ≡ x. If |B| = 0, Γ ⊢ x^{B} : core(B). Therefore for any B there exists u such that u ∈ t, head(u) ≡ x^{B} and Γ ⊢ u : core(B). Let u_{1},…, u_{n} be all the u satisfying these conditions.

In the same manner, there exists v such that v ∈ t, head(v) ≡ x^{C} and Γ ⊢ v : core(C). Let v_{1},…, v_{m} be all the v satisfying these conditions.

There exists a minimal term of u_{1},…, u_{n}, v_{1},…, v_{m} with respect to the subterm relation ∈. We suppose that it is u satisfying the former conditions. (We omit the case that it is v satisfying the latter conditions.) By Lemma 3.5, x^{C} ∉ u if x^{C} ≢ u.

For a λ-free term w, we define a function f as follows:

• f(x^{D}) ≡ x^{D} for any D.

• f(xw_{1} … w_{n}) ≡ u if Γ ⊢ xw_{1} … w_{n} : core(B).

• f(xw_{1} … w_{n}) ≡ xf(w_{1}) … f(w_{n}) otherwise.

Let t′ be f(t). We can prove that x^{C} ∉ f(w) for any λ-free term w by induction on w by using Lemma 3.5. Hence x^{C} ∉ t′. Choose a fresh variable α. We get Γ′ by replacing x^{C} : C in Γ by x^{α} : α. Then Γ′ ⊢ t′ : A. Since (Γ′, A) < (Γ, A), it contradicts with the minimality of (Γ̃, A). □

Lemma 3.11.

Γ ⊢ t_{1} : A, Γ ⊢ t_{2} : A, t_{1} and t_{2} are λ-free and each core of Γ is distinct, then t_{1} ≡ t_{2}.

Proof 3.12.

Induction on |t_{1}| + |t_{2}|. □

Theorem 3.13.

If (Γ̃, A) is minimal, Γ ⊢ t_{1} : A, Γ ⊢ t_{2} : A, t_{1} and t_{2} are β-normal, |Γ| ≤ 1 and |A| = 0, then t_{1} ≡ t_{2}.

Proof 3.14.

By Lemma 3.7, t_{1} and t_{2} are λ-free. By Proposition 3.9, each core of Γ is distinct. By Lemma 3.11, t_{1} ≡ t_{2}. □

Lemma 3.15.

If (Γ̃, A) is minimal, Γ ⊢ t : A, t is β-normal, |Γ| ≤ 1 and |A| ≤ 2, then there exists a term u and a variable α such that t ≡ λx_{1} … x_{n}.u and Γ, x_{1} : A_{1},…, x_{n} : A_{n} ⊢ u : α.

Proof 3.16.

Γ |⊢ t : A holds. We prove the claim by induction on |t|.

The case that |t| = 0 and the case that |t| > 0, t ≡ λx^{B}.t_{1} are easy and we omit these cases. We suppose that |t| > 0, t ≡ t′t′′.

Since t is β-normal, we have t ≡ x^{A_{1}→...A_{n}→A}t_{1} … t_{n} and Γ ⊢ t_{i} : A_{i} (1 ≤ i ≤ n) for some n ≥ 1. Since A_{1} →… A_{n} → A is in Γ̃, |A_{1} →… A_{n} → A| = 1, |A_{i}| = 0 (1 ≤ i ≤ n) and |A| ≤ 1 hold. If |A| = 0, the claim holds by putting u ≡ t. Suppose that |A| = 1.

By Lemma 3.7, t_{i} (1 ≤ i ≤ n) is λ-free. Therefore t is λ-free. Let B ≡ A_{1} →… → A_{n} → A. Let u_{1},…, u_{m} be all the subterms u of t such that x^{B} ≡ head(u) and Γ ⊢ u : core(B). Let v be a minimal term of t, u_{1},…, u_{m} with respect to the subterm relation ∈.

We omit the case that v ≡ t here. We suppose that v ≡ u_{i} for some i.

Suppose A ≡ A_{n+1}→… A_{l}→β. Then v ≡ x^{B}v_{1} … v_{l}. Moreover x^{B} ∉ v_{i} by Lemma 3.5. Choose a fresh variable α and get Γ′ by replacing x^{B} : B in Γ by x^{A_{1}→...→A_{n}→α} : A_{1} →…→A_{n} →α. Then Γ′ ⊢ x^{A_{1}→...→A_{n}→α}v_{1} … v_{n} : α and (Γ̃′, α) < (Γ̃, A) hold. This contradicts with the minimality of (Γ̃, A). □

Proof 3.17. (Proof of Theorem 3.2)

Suppose that π and π′ are β-normal proofs of A.

|⊢ π : A and |⊢ π′ : A hold. Since A is minimal, |A| ≤ 2, π and π′ are β-normal, by Lemma 3.15, π ≡ λx_{1} … x_{n}.u, Γ ⊢ u : α, π′ ≡ λx_{1} … x_{n}.v and Γ ⊢ v : α hold for some variable α where Γ ≡ x_{1} : A_{1},…, x_{n} : A_{n}. From |A| ≤ 2, we get |Γ| ≤ 1. Since A is minimal, (Γ̃, α) is minimal. Since u and v are β-normal, by Theorem 3.13, u ≡ v holds. Therefore π ≡ π′ holds. □

4 Counterexamples

In this section, we present general answers to the problems given in Section 2. The answers are negative for both NJ an NK cases.

Theorem 4.1.

The claim of Problem 2.9 does not hold. That is, there is a counterexample A which is a minimal formula of NJ and has more than 1 βη-normal proofs in NJ.

Proof 4.2.

The following proofs π_{1} and π_{2} are counterexamples to the claim of Problem 2.9. The formula proved by π_{1} and π_{2} is a minimal formula. The minimality of this formula was checked by machine with a Lisp program. This formula has distinct βη-normal proofs π_{1} and π_{2}.

In the proofs π_{1} and π_{2}, we use A, B, …, X, Y to denote propositional variables.

The proof π_{1} is

\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}\begin{matrix}{⋮ . Π_{1} \atop H → I} & {⋮ . Π_{2} \atop H} \\ I \end{matrix} ; (((K → A) → B) → X) → I & (6) \\ (A → F) → (((K → A) → B) → X) → I \end{matrix} & (7) \\ (((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I \end{matrix} & (8) \\ L → (((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I \end{matrix} ; (9) ; K → L → (((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I & (10) \\ (A → T) → K → L → (((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I \end{matrix} (11) ; {(((T → B) → X) → F → Y) → (A → T) → K → L \atop →(((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I} ; (12) ; {(((L → A) → Y) → H → I) → (((T → B) → X) → F → Y) → (A → T) → K → L \atop →(((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I.} ; (13)

The subproof Π_{1} is

\begin{aligned}(13) ; {((L → A) → Y) \atop →H → I} & \begin{matrix}\begin{aligned}(12) ; {((T → B) → X) \atop →F → Y} & \begin{matrix}{(6) \atop ((K → A) → B) → X} & \begin{aligned}{(2) \atop T → B} & & \begin{matrix}{(11) \atop A → T} & {⋮ . Σ_{1} \atop A} \\ T \end{matrix} \\ & B \end{aligned} ; (K → A) → B ; (1) \\ X \end{matrix} ; (T → B) → X ; (2) \\ & F → Y \end{aligned} & \begin{aligned}{(7) \atop A → F} & & \begin{matrix}{(3) \atop L → A} & {(9) \atop L} \\ A \end{matrix} \\ & F \end{aligned} \\ Y \end{matrix} ; (L → A) → Y ; (3) \\ & H → I. \end{aligned}

The subproof Σ_{1} is

\begin{matrix}{(1) \atop K → A} & {(10) \atop K} \\ A. \end{matrix}

The subproof Π_{2} is

\begin{aligned}{(8) \atop ((F → B) → X) → H} & \begin{matrix}{(6) \atop ((K → A) → B) → X} & \begin{aligned}{(5) \atop F → B} & \begin{aligned}{(7) \atop A → F} & & \begin{matrix}{(4) \atop K → A} & {(10) \atop K} \\ A \end{matrix} \\ & F \end{aligned} \\ & B \end{aligned} ; (K → A) → B ; (4) \\ X \end{matrix} ; (F → B) → X ; (5) \\ & H. \end{aligned}

The proof π_{2} is the same as the proof π_{1} except that π_{2} includes a subproof Σ_{2} instead of Σ_{1}. The subproof Σ_{2} is

\begin{matrix}{(3) \atop L → A} & {(9) \atop L} \\ A. \end{matrix}

□

The next problem is Problem 1.5 proposed in Komori’s paper [5].

Problem 4.3. (Komori)

For a minimal formula A, βη-normal terms t_{1} and t_{2}, if ⊢ t_{1} : A and ⊢ t_{2} : A are type-schemes [2], then t_{1} and t_{2} are syntactically identical.

Theorem 4.4.

The claim of Problem 4.3 does not hold.

Proof 4.5.

We construct βη-normal terms t_{1} and t_{2} corresponding to proofs π_{1} and π_{2} in Proof 4.2 respectively.

Distinct terms t_{1} and t_{2} are βη-normal terms and both have the same type (((L → A) → Y) → H → I) → (((T → B) → X) → F → Y) → (A → T) → K → L →(((F → B) → X) → H) → (A → F) → (((K → A) → B) → X) → I

which is a minimal formula where A, B, …, X, Y denote type variables.

The term t_{1} is λmlkjihgf.m(λc.l(λb.f(λa.b(k(aj))))(g(ci)))(h(λe.f(λd.e(g(dj))))).

The term t_{2} is λmlkjihgf.m(λc.l(λb.f(λa.b(k(ci))))(g(ci)))(h(λe.f(λd.e(g(dj))))).

Note that a subproof Σ_{1} corresponds to a term aj in t_{1} and a subproof Σ_{2} corresponds to a term ci in t_{2}. □

Remark 4.6.

Minc found another counterexample:

((((A → B) → A) → A) → B) → B where A and B denote propositional variables. Our counterexample was found independently.

Note that our counterexample has just 2 βη-normal proofs, but on the other hand Minc’s counterexample has infinite βη-normal proofs.

Theorem 4.7.

The claim of Problem 2.10 does not hold. That is, there is a counterexample A which is a minimal formula of NK and has more than 1 βη-normal proofs in NK.

Proof 4.8.

The same formula of Proof 4.2 is also a counterexample of this theorem. The formula is also minimal in NK. The minimality of the formula in NK was also checked by machine with a Lisp program. The formula has distinct βη-normal proofs. □

Remark 4.9.

This result is independent of a formalization of NK. In this paper we give it by NJ + (((A → B) → A) → A), but for other formalizations of NK Theorem 4.7 holds also.

Minc’s counterexample in Remark 4.6 is not a counterexample of this claim because the formula is not minimal in NK, since

((((A → C) → A) → A) → B) → B < ((((A → B) → A) → A) → B) → B and ⊢NK ((((A → C) → A) → A) → B) → B hold.

5 Minimal formulas of depth 3

In this section, we search smaller counterexamples. We present counterexamples of depth 3 for both NJ and NK cases.

Combined with Theorem 3.2 in Section 3, it gives a classification of minimal formulas having the unique normal proof by the depth of a formula. That is, a minimal formula of depth less than 3 always has the unique normal proof, but on the other hand for any n ≥ 3 there exists a minimal formula A of depth n such that A does not have the unique normal proof.

Theorem 5.1.

(1) In NJ, there exists a minimal formula A of depth 3 such that a βη-normal proof of A is not unique.

(2) In NK, there exists a minimal formula A of depth 3 such that a βη-normal proof of A is not unique.

We prove this theorem by using a procedure of reducing the depth of a formula.

Definition 5.2.

Suppose that a formula A is ((A_{11}^{1} → A_{12}^{1} →… → α_{1}^{1}) → (A_{21}^{1} → A_{22}^{1} →… → α_{2}^{1}) →… → α_{1}) → ((A_{11}^{2} → A_{12}^{2} →… → α_{1}^{2}) → (A_{21}^{2} → A_{22}^{2} →… → α_{2}^{2}) →… → α_{2}) → →… → α

and |A| ≥ 4.

We define P_{1}(A) as follows: Let A_{1} be the leftmost occurrence A_{jk}^{i} such that |A_{jk}^{i}| = |A| − 3. Choose a fresh variable p. Let Ã(p) be A such where A_{1} is replaced by p. We define

P_{1}(A) ≡ (p → A_{1}) → Ã(p). For a formula A, #A denotes the number of occurrences A_{jk}^{i} such that |A_{jk}^{i}| = |A| − 3. We use

the lexical order for (n, m) ∈ N × N here. We define a formula P_{0}(A) by induction on (|A|, #A) as follows:

• If |A| ≤ 3, then P_{0}(A) ≡ A.

• If |A| > 3, then P_{0}(A) ≡ P_{0}(P_{1}(A)).

Note that if |A| > 3, then (|P_{1}(A)|, #P_{1}(A)) < (|A|, #A) holds.

Proposition 5.3.

(1) |P_{0}(A)| ≤ 3.

(2) ⊢ A iff ⊢ P_{0}(A) in both NJ and NK.

Proof 5.4.

(1) Clear by definition.

(2) It is sufficient to show that ⊢ A iff ⊢ P_{1}(A).

The only if part: ⊢ A → P_{1}(A) holds since the occurrence p is negative in Ã(p).

The if part: Let π be a proof of P_{1}(A). We get π′ by replacing all the occurrences of p in π by A_{1}. Then π′ is a proof of (A_{1} → A_{1}) → A. Therefore ⊢ A holds. □

Theorem 5.5.

• If a formula A is minimal in NJ, P_{0}(A) is minimal in NJ.

• If a formula A is minimal in NK, P_{0}(A) is minimal in NK.

Proof 5.6.

The proofs are the same for both NJ case and NK case. It is sufficient to show that if A is minimal, then P_{1}(A) is minimal.

Assume that A is minimal and P_{1}(A) is not minimal. We have formulas C(α) and D such that a variable α occurs once in C(α) and ⊢ C(α), C(D) ≡ P_{1}(A) and |D| > 0 hold. Then C(D) ≡ (p^{1} → A_{1}) → Ã(p) holds where p^{1} denotes the occurrence of p. We classify cases by which part of C(D) D occupies.

The case that D covers p^{1}. Since |D| > 0 and C(α) ≢ α from ⊢ C(α), we have C(α) ≡ α→Ã(p). Let π be a proof of C(α) and β be a fresh variable. We get π′ by replacing all the occurrences of α in π by β → β. Then π′ is a proof of (β → β) → Ã(p). Therefore ⊢ Ã(p) holds. Since Ã(A_{1}) ≡ A, Ã(p) < A. This contradicts with the minimality of A.

We omit the case that D does not cover p^{1}, for almost the same discussion proves this case. □

Remark 5.7.

This theorem shows that the procedure P_{1} or P_{0} of reducing the depth of a formula preserves the minimality of a formula.

This property depends on the definition of the procedure. If we define P_{2}(A) ≡ (p → A_{1}) → (A_{1} → p) → Ã(p), then P_{2} does not preserve the minimality. For example, let A ≡ (((α → β) → β) → γ) → α → γ, then A is minimal but P_{2}(A) is not minimal.

Definition 5.8. (Transformation of a proof)

Suppose that |A| ≥ 4 and π is a proof of a formula A. We define a proof P_{1}(π) of P_{1}(A) as follows:

P_{1} is defined by using P_{+}^{A(p)} and P_{−}^{A(p)}. Fix a propositional variable p and a term variable f. Suppose that a variable p occurs at most

once in a formula A(p). We define P_{+}^{A(p)} and P_{−}^{A(p)} by induction on the construction of A(p) as follows:

We use type theoretical notations here. That is, we treat proofs, P_{+}^{A(p)} and P_{−}^{A(p)} as terms. P_{+}^{A(p)} and P_{−}^{A(p)} are defined to have the following property:

• If p occurs positively in A(p), f : p → A_{1} ⊢ P_{+}^{A(p)} : A(p) → A(A_{1}).

• If p occurs negatively in A(p), f : p → A_{1} ⊢ P_{−}^{A(p)} : A(A_{1}) → A(p).

We define P_{+}^{A(p)} and P_{−}^{A(p)}:

1. A(p) ≡ p.

P_{+}^{p} ≡ f.

We do not have P_{−}^{p}.

2. A(p) ≡ α where a variable α is not p.

P_{+}^{α} ≡ λx^{α}.x, P_{−}^{α} ≡ λx^{α}.x.

3. A(p) ≡ B(p) → C(p).

P_{+}^{B(p)→C(p)} ≡ λx^{B(p)→C(p)}y^{B(A_{1})}.P_{+}^{C(p)}(x(P_{−}^{B(p)}y)),

P_{−}^{B(p)→C(p)} ≡ λx^{B(A_{1})→C(A_{1})}y^{B(p)}.P_{−}^{C(p)}(x(P_{+}^{B(p)}y)).

Finally we define P_{1}(π) ≡ λf^{p→A_{1}}.P_{−}^{Ã(p)}(π).

Proposition 5.9.

If π is a proof of A, P_{1}(π) is a proof of P_{1}(A).

Proof 5.10.

Since f : p→A_{1} ⊢ P_{−}^{Ã(p)} : A→Ã(p), if ⊢ t : A holds, then ⊢ λf^{p→A_{1}}.P_{−}^{Ã(p)}(t) : (p→A_{1})→Ã(p) holds. Therefore ⊢ P_{1}(π) : P_{1}(A). □

Proposition 5.11.

Let σ be a substitution [p := A_{1}, f := λx^{A_{1}}.x].

(1) (P_{+}^{A(p)}σ)x^{A(A_{1})} =_{βη} x^{A(A_{1})}.

(2) (P_{−}^{A(p)}σ)x^{A(A_{1})} =_{βη} x^{A(A_{1})}.

Proof 5.12.

These claims (1) and (2) are proved simultaneously by induction on the construction of A(p). □

Theorem 5.13.

If P_{1}(π) =_{βη} P_{1}(π′), then π =_{βη} π′ holds.

Proof 5.14.

Assume that P_{1}(π) =_{βη} P_{1}(π′). Then λf^{p→A_{1}}.P_{−}^{Ã(p)}(π) =_{βη} λf^{p→A_{1}}.P_{−}^{Ã(p)}(π′). Apply the both sides to a variable f^{p→A_{1}}. Let σ be a substitution [p := A_{1}, f := λx^{A_{1}}.x] and apply σ to the both sides. Since p and f do not occur in π and π′, we have (P_{−}^{Ã(p)}σ)(π) =_{βη} (P_{−}^{Ã(p)}σ)(π′). Therefore by Proposition 5.11 π =_{βη} π′ holds. □

Remark 5.15.

This theorem shows that the transformation P_{1} of a proof preserves equivalence of proofs.

[7] gave very similar notions of P_{1}(A) for a formula A, P_{1}(π) for a proof π, the preservation of equivalence of proofs by P_{1}. These notions of this paper are based on those of his paper, but this paper gives a precise definition P_{1}, though his paper omitted a precise definition of a procedure. The precise definition of the procedure is important for our purpose, since, as discussed in Remark 5.7, the preservation of minimality by a procedure depends on a subtle point of the definition of the procedure. Note also that [7] made mistakes in the proof of the preservation of equivalence of proofs.

Proof 5.16. (Proof of Theorem 5.1)

By applying the procedure P_{1} to the counterexamples of Proof 4.2 and Remark 4.6, we get new counterexamples of depth 3.

(1) By applying P_{1} to the counterexample of Proof 4.2, we get the first counterexample of depth 3:

(S → (K → A)) → (R → (F → B)) → (Q → (T → B)) → (P → (L → A)) →

((P → Y) → H → I) → ((Q → X) → F → Y) → (A → T) → K → L →
((R → X) → H) → (A → F) → ((S → B) → X) → I

where A, B,…, P, Q, R, S, X, Y denote propositional variables.

By applying P_{1} to the counterexample of Remark 4.6, we get the second counterexample of depth 3:

(P → (A → B) → A) → ((P → A) → B) → B where A, B and P denote propositional variables.

They are both counterexamples of depth 3 for NJ case.

(2) The first counterexample of depth 3 in (1) is also a counterexamples of depth 3 for NK case. □

Acknowledgements

I am grateful to Prof. Yuichi Komori for proposing the problems. I would like to thank Prof. Masahiko Sato, Prof. Sachio Hirokawa and Mr. Yukiyoshi Kameyama for valuable discussions and suggestions. I also wish to express thanks to Prof. Nobuo Yoneda, Prof. Hayao Nakahara, Dr. Yoshiki Kinoshita, Dr. Hiroyuki Sato and Mr. Makoto Matsumoto for careful comments.

References

[1] Barendregt, H.P. : The Lambda Calculus: Its Syntax and Semantics (North-Holland, Amsterdam, 1984).

[2] J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ-Calculus (Cambridge University Press, Cambridge, 1986).

[3] S. Hirokawa, Principal types of BCK-lambda terms, to appear in Theoretical Computer Science.

[4] W.A. Howard, The Formulae-as-Types Notion of Construction, in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, London, 1980).

[5] Y. Komori, BCK Algebras and Lambda Calculus, in: Proceedings of the 10th Symposium on Semigroups (Josai Univ., Sakado, 1987) pp. 5 – 11.

[6] Y. Komori and S. Hirokawa, The number of proofs for a BCK-formula, to appear in Journal of Symbolic Logic.

[7] S.V. Solov’ev, Preservation of Equivalence of Derivations under Reduction of Depth of Formulas, English translation from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya matematicheskogo Instituta im. V.A. Steklova AN SSSR, Vol. 8 (1979) pp. 197–207.

[8] A. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, in: Lecture Notes in Mathematics 344 (Springer, Berlin, 1973).