Anita Wasilewska

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.

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.