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

We use the algebraic theory of programs as in Blikle [2], Mazurkiewicz [5] in order to show that the difference between programs with and without recursion is of the same kind as that between cut free Gentzen type formalizations of predicate and prepositional logics.