This paper can be treated as a simplification of the Gentzen formalization of SCI-tautologies presented by A. Michaels in [1].

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.

We introduce here and investigate the notion of an alternative tree of decomposition. We show (Theorem 5) a general method of finding out all non-alternative trees of the alternative tree determined by a diagram of decomposition.