A subsystem of classical analysis proper to Takeuti's reduction method for \(\Pi ^ 1_ 1\)-analysis (Q1087871)

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.