The machinery of consistency proofs (Q1124588)

The author claims in effect that the essence of a consistency proof for a second-order system \b{S} is a primitive recursive procedure transforming any proof P in \b{S} of a closed sequent into an omega-derivation of the same sequent using second-order comprehension and enriched by derivations in \b{S} of all occurring sequents in such a way that the enrichment of the last sequent is P. Some additional conditions seem to be required (and in fact assured by the results mentioned in the paper under review) since the canonical (proof search) tree \(T_ s\) for a sequent s is already primitive recursive, well-founded if s is true in all (Henkin) omega-models, and \(T_ s\) true can be enriched by finite derivations using cuts with suitable easily derivable sequents. Most obvious amendments would be: (1) to restrict comprehension to the form allowed in the original system \b{S}; (2) to strengthen well-foundedness condition to enrichment by suitable ordinal notations, and (3) to forbid using the cut rule to connect \b{S}-proofs of adjacent sequents, requiring (Gentzen-Takeuti- type) finite reductions instead. The comparison with the Munich school approach (especially of the author's projections and elevations with collapsing functions) would probably make understanding easier.