On the intuitionistic strength of monotone inductive definitions

Tupailo, Sergei

Tupailo, Sergei

J. Symbolic Logic, Tome 69 (2004) no. 1, p. 790-798 / Harvested from Project Euclid

Résumé

We prove here that the intuitionistic theory T₀↾+UMID_N, or even EETJ↾+UMID_N, of Explicit Mathematics has the strength of Π₂¹-CA₀. In Section 1 we give a double-negation translation for the classical second-order μ-calculus, which was shown in [Moe02] to have the strength of Π₂¹-CA₀. In Section 2 we interpret the intuitionistic μ-calculus in the theory EETJ↾+UMID_N. The question about the strength of monotone inductive definitions in T₀ was asked by S. Feferman in 1982, and — assuming classical logic — was addressed by M. Rathjen.

Publié le : 2004-09-14
Classification:

@article{1096901767,
     author = {Tupailo, Sergei},
     title = {On the intuitionistic strength of monotone inductive definitions},
     journal = {J. Symbolic Logic},
     volume = {69},
     number = {1},
     year = {2004},
     pages = { 790-798},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1096901767}
}

Tupailo, Sergei. On the intuitionistic strength of monotone inductive definitions. J. Symbolic Logic, Tome 69 (2004) no. 1, pp.  790-798. http://gdmltest.u-ga.fr/item/1096901767/