ABSTRACT

On the other side, I have described finitary algorithms generating the con­ sequence operations ct and cs in Chapter 1 .15 . As it was just the existence of such algorithm s, but not their particular form, which played a role for the questions treated in Book 1, I did not care there to present them in more detail. It now turns out, however, that these algorithm s, arising partly from general algebraic notions about invariant congruence relations, and partly from properties of suprema and infima in lattices, permit an almost immediate translation into modus ponens calculi which will be given on the next few p ages. The connection between these modus ponens calculi and the sequential calculi from the previous Chapter then will be an easy extension of the same connection established for the propositional case in Theorem 7 .2 , and it w ill be carried out at the beginning of Chapter 10.