A subsystem of classical analysis proper to Takeuti's reduction method for \(\Pi ^ 1_ 1\)-analysis (Q1087871)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A subsystem of classical analysis proper to Takeuti's reduction method for \(\Pi ^ 1_ 1\)-analysis |
scientific article |
Statements
A subsystem of classical analysis proper to Takeuti's reduction method for \(\Pi ^ 1_ 1\)-analysis (English)
0 references
1985
0 references
The author proposes a subsystem of classical analysis called AII (Axiom of Instantiation \(\forall \phi F(\phi)\supset F(V)\) with the Isolated formulae \(\forall \phi F(\phi))\) which is proved to be consistent following some methods of G. Gentzen and G. Takeuti. This result, together with related work by the author concerning derivability of transfinite induction in the system AII complements the proof of consistency of Takeuti's \((\Pi^ 1_ 1-CA)+(BI).\) The reader should be aware of some minor misprints, especially in the use of commas.
0 references
consistency proofs
0 references
subsystem of classical analysis
0 references
AII
0 references
Axiom of Instantiation
0 references
Isolated formulae
0 references