No label defined (Q4250044)

The reduction calculus approach, introduced by the author for classical predicate calculi in ``Cut free formalization of logic with finitely many variables. I'' [Computer science logic. 8th workshop, CSL '94, Lect. Notes Comput. Sci. 933, 136-150 (1995)] is extended to \(m\)-valued predicate Post logics. It is shown that a Hilbert-style deduction calculus \({\mathbf {PL}}_m\), which formalizes the \(m\)-valued Post logic, can be embedded in a 2-valued deduction calculus \({\mathbf L}_m^*\) such that for a formula \(A\), \({\mathbf {PL}}_m \vdash A\) iff \({\mathbf L}_m^* \vdash {\mathbf D}_{m-1}A\) (\({\mathbf D}_{m-1}A\): representative of \(A\) for the embedding). Gentzen's method applied to \({\mathbf L}_m^*\) yields an equivalent cut free sequent calculus \({\mathbf {SL}}_m^{\dagger}\) in Schütte-Rasiowa-Sikorski-Tait form. Since in the case of the restricted predicate calculus \({\mathbf L}_{m,n}^*\), with a finite number \(n\) of distinct variables, this approach does not work, the author presents a cut free formalization in the form of a rewriting system, the so-called reduction system \({\mathbf {RL}}_{m,n}^{\dagger}\). It is shown that a formula \(A\) is derivable in \({\mathbf {RL}}_{m,n}^{\dagger}\) ( \( A\overset{*}\longrightarrow \text{top}\)) iff \({\mathbf L}_{m,n}^* \vdash A\). For the entire collection see [Zbl 0910.00016].