Non-strictly positive fixed points for classical natural deduction

Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions. ers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new result. y, the relation to Parigot’s strictly positive inductive definition of his set of reducibility candidates and to his notion of generalized reducibility candidates is explained.