Long D-normal Form Yields Uniqueness of Proofs

Sachio Hirokawa & Makoto Tatsuta

There have been much interest in the conditions for uniqueness of normal form proofs in intuitionistic logic. [Tatsuta99] introduced a notion of D-normal form proof and showed that D-normal form proof is unique for any implicational formula. But this result means the uniqueness of D-normal form proof. There may be some other normal form proof which is not D-normal. We show that D-normality yields the uniqueness of proofs as long as the long-normal form proofs are concerned.

For a formula, core(A) is the rightmost variable in A. A normal form proof is D-normal if core(A) ≠ core(B) for any initial sequent Γ, A, B ⊢ A.

Theorem If a formula A has a long D-normal form proof , then long normal form of A is unique.

[Hirokawa93] S. Hirokawa, Principal types of BCK-λ-terms, Theoretical Computer Science 107, 253–276, 1993 [Tatsuta93] M. Tatsuta, Uniqueness of normal form proofs of minimal formulas, Journal of Symbolic Logic 58 (3), 789–799, 1993 [Tatsuta99] M. Tatsuta, Uniqueness of D-normal Proofs, Asian Logic Conference, Jun 7–10, 1999

Addresses Sachio Hirokawa: Computing and Communications Center, Kyushu University, Fukuoka 812-8581, Japan

E-mail: hirokawa@cc.kyushu-u.ac.jp

Makoto Tatsuta: Department of Mathematics, Kyoto University, Kyoto 606-8502, Japan

E-mail: tatsuta@kusm.kyoto-u.ac.jp