Abstract

We use here the notions and results from algebraic theory of programs in order to give a new proof of the decidability theorem for Suszko logic SCI (Theorem 3).We generalize the method used in the proof of that theorem in order to prove a more general fact that any prepositional logic which admits a cut-free Gentzen type formalization is decidable (Theorem 6).