Normal form theorem of natural deduction for modal logic S4 (Proof theoretical study of the structure of logic and computation)
Yuuki Andou · Institutional Repositories DataBase (IRDB) · 2009
Gentzen's Hauptsatz [2], which has been stated in the systems of sequent calculi, was reconstructed by Prawitz [5] as normalization theorem in the systems of natural deduction.Conceming the modal logic S4, Prawitz introduced three formulations in natural deduction, and noticed that the third one enjoys normalization theorem.Later, Medeiros [3] mentioned that Prawitz's proof does not work, and gave a new proof of normalization theorem with another formulation of S4 in natural deduction.But her proof also contains gaps, as we have seen in our previous technical report [1].In this paper, we prove the normal form theorem of natural deduction for S4 in the formulation of Medeiros.Notice that it is not the normalization theorem of the system in a narrow sense.It means that we can show the existence of a normal derivation for any given derivation, but we do not define non-trivial normalization procedure $in$ the system.Our proof depends on the cut-elimination theorem of sequent calculus for S4 proved by Ohnishi and Matsumoto [4].First, we recall the formulation of Medeiros, and give the definition of the maximal formula, the redex of a derivation.Second, we define the transformation of a given cut-free derivation in sequent calculus for S4 to a normal derivation in natural deduction for the same logic. The system NS4In [3], Medeiros introduced a new formalization of the system in natural deduction for classical propo- sitional modal logic $S4$ , called NS4.It has $\wedge,$ $\vee,$ $\supset,$ $\perp$ , ロ as logical constants, and the inference rules for introduction and elimination of $\wedge,$ $\vee,$ $\supset$ are defined as usual.The rules for introduction and elimination of the modal operator a are defined as below.