Abstract:
The problem of the cut-elimination for calculuses of general type is formulated as the problem of strict representability by means of Post canonical systems satisfying the additional requirement: each word can be a conclusion only of a finite member of applications of rules. Possibilities of elimination and of algorithmic elimination of cut-type rules are studied.