The machinery of consistency proofs (Q1124588)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The machinery of consistency proofs |
scientific article |
Statements
The machinery of consistency proofs (English)
0 references
1989
0 references
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.
0 references
proof theory
0 references
enrichment of sequent
0 references
consistency proof
0 references
second-order system
0 references
primitive recursive procedure
0 references
closed sequent
0 references
omega-derivation
0 references
second-order comprehension
0 references
0 references
0 references
0 references
0 references