This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.

Programming practice suggests a notion of general iteration corresponding to the while-do construct. This leads to new characterizations of general computable unary functions usable in computer science.