scientific article; zbMATH DE number 1303435

Publication date 11 October 1999

deductive systems many-valued logic Post logic reduction calculus rewriting systems sequent calculus

Abstract deductive systems (03B22) Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Grammars and rewriting systems (68Q42)

Review text

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].

Recommendations

Cited in

(2)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4250044)