Uniqueness of normal proofs in implicational intuitionistic logic (Q1288178)

This paper includes the excellent result on the uniqueness of normal proofs in implicational intuitionistic logic. All previous results are covered with the result. A minimal theorem in a logic \(L\) is an \(L\)-theorem which is not a nontrivial substitution instance of another \(L\)-theorem. The reviewer [in: Proc. 10th Symp. on Semigroups, Sakado/Jap. 1986, 5-11 (1987)] raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system \(NJ\). Two sufficient conditions for a minimal implicational intuitionistic theorem \(A\) to have a unique \(\beta\)-normal proof in \(NJ\) have been obtained. One of them requires \(A\) to be provable in BCK; it follows from a series of results (Hirokawa, 1993; Jaskowski, 1963; Kashima, 1997). The other needs \(A\) to be of depth \(\leq 2\); it was proved by \textit{M. Tatsuta} [J. Symb. Log. 58, No. 3, 789-799 (1993; Zbl 0791.03004)]. The author gives a sufficient condition for a minimal implicational theorem in intuitionistic logic to have a unique normal proof in the natural deduction system \(NJ\). The result is that a minimal implicational intuitionistic theorem \(A\) has a unique \(\beta\)-normal proof in \(NJ\) whenever \(A\) is provable without ``non-prime contraction''. The non-prime contraction rule in \(NJ\) is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. The result covers the two conditions mentioned above.