On certain normalizable natural deduction formulations of some propositional intermediate logics (Q1117920)

Transformations of Gentzen-type formulations for some intermediate propositional logics into natural deduction systems are studied. Author considers intermediate logics \(\Delta\) (M), \(S_{\omega}\), \(S_ n\), where \(\Delta (M)\rightleftharpoons H+((p\to A)\to p)\to p\) and A is any formula provable in an abitrary propositional logic M and p is a propositional variable not contained in A; \(S_{\omega}\rightleftharpoons H+(A\to B)\vee (B\to A)\); \(S_ n\rightleftharpoons S_{\omega}+A_ n\), \(A_ 1\rightleftharpoons ((p_ 1\to p_ 0)\to p_ 1)\to p_ 1\), \(A_ n\rightleftharpoons ((p_ n\to A_{n-1})\to p_ n)\to p_ n\). The Gentzen-type formulation \(G\Delta\) (M) for \(\Delta\) (M) was obtained by Hosoi (1974), \(GS_ n\) for \(S_ n\) was found by Sonobe (1975), system \(GS'_{\omega}\) for \(S_{\omega}\) is constructed in this paper. The author finds a transformation of GL, where \(L=\Delta (M)\), \(S_{\omega}\), \(S_ n\), into the corresponding natural deduction systems NL. Author constructs the mapping f from the class of proofs in a cut-free sequent calculus into the class of derivations of the corresponding natural deduction system. The following results are obtained: 1) \(\Gamma\) \(\vdash \Delta\) is provable in GL iff \(\Gamma \vdash_{NL}\Delta\). 2) If the proof d of the sequent \(\Gamma\) \(\vdash \Delta\) in GL is without applications of the cut rule, then f(d) is a normal derivation in NL. 3) If \(\Gamma \vdash_{NL}\Delta\) by a derivation d in NL, then there exists a normal derivation \(d'\) in NL by which \(\Gamma \vdash_{NL}\Delta\). 4) There is an effective procedure reducing all derivations in NL into a normal derivation.