Proof theory for minimal quantum logic. I (Q1325718)

More than a decade ago, the author [J. Symb. Log. 45, 339-352 (1980; Zbl 0437.03034)] introduced \textit{G. Gentzen's} [Math. Z. 39, 176-210, 405-431 (1934; Zbl 0010.14501, Zbl 0010.14601)] sequential methods into the realm of quantum logic. The methods were elaborated by \textit{N. J. Cutland} and \textit{P. F. Gibbons} [Logique Anal., Nouv. Sér. 25, 221-248 (1982; Zbl 0518.03029)] to render a sequential system of minimal quantum logic which enjoys regularity and duality, but which fails to enjoy the so-called cut- elimination theorem. \textit{S. Tamura} [Kobe J. Math. 5, No. 1, 133-150 (1988; Zbl 0663.03050)] finally succeeded in giving a cut-free sequential system of minimal quantum logic, but his system enjoys cut-freeness in such an unreasonably distorted manner that his proof for the cut- elimination theorem appears more esoteric than it really is. This paper gives a more lucid sequential make-up of minimal quantum logic, and then establishes its two fundamental proof-theoretical properties, namely, the duality theorem and the cut-elimination theorem, though their proofs are relegated to a subsequent paper [Int. J. Theor. Phys. 33, 1443-1459 (1994)] due to severe limitations of space. The duality theorem is a conceptual distillation of Lemma 4 of Tamura's paper [loc. cit.]. The completeness theorem with respect to \textit{R. I. Goldblatt}'s [J. Philos. Log. 3, 19-35 (1974; Zbl 0278.02023)] semantics is also established.