On the intuitionistic strength of monotone inductive definitions

Sergei Tupailo


In his 2002 PhD thesis M. Moellerfeld has shown that the second-order mu-calculus, a theory axiomatizing least fixed points of positively defined monotone operators, when based on classical logic, has the strength of Pi1_2 comprehension axiom, which is the current limit of ordinal analysis. His methods are based on Generalized Recursion Theory, and as such are not amenable to intuitionistic reasoning. However, the $\mu$-calculus presented very little problems for the Goedel-Gentzen-Kolmogorov double-negation translation, so we prove that the intuitionistic theory is proof-theoretically equally strong. Further interpretation of the intuitionistic mu-calculus in the system T_0^i+UMID of Explicit Mathematics provides a first breakthrough into intuitionistic strength of monotone inductive definitions in those theories, showing that one should expect that this strength is as big as the classical one. This question was posed by S. Feferman in 1982, but up to now virtually nothing was known in this area. On the classical side, it came as a surprise when M. Rathjen proved in a series of papers of 1996-2002 that the strength is essentially that of Pi1_2-CA. Our work determines the exact strength of the intuitionistic T_0^i(restr.)+UMID_N. The complete paper is available at http://www.cs.ioc.ee/~sergei/Mypapers/mumid.ps .
Thursday 2nd October 2003, 14:00
Robert Recorde Room
Department of Computer Science