On the Intuitionistic Strength of Monotone Inductive Definitions
by
Sergei Tupailo
University of Leeds, England

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 \Pi¹₂ 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₀ⁱ+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 \Pi¹₂-CA. Our work determines the exact strength of the intuitionistic T₀ⁱ(restr.)+UMID_N.

Date received: April 19, 2003