On the intuitionistic strength of monotone inductive definitions. (English) Zbl 1070.03040

Summary: We prove here that the intuitionistic theory \({\mathbf T}_0\!\!\upharpoonright \!\!+\,\, \mathbf{ UMID}_N\), or even \(\mathbf{EETJ}\!\!\upharpoonright\!\! +\,\, \mathbf{ UMID}_N\), of Explicit Mathematics has the strength of \(\Pi^1_2-\mathbf{CA}_0\). In Section 1 we give a double-negation translation for the classical second-order \(\mu\)-calculus, which was shown by M. Möllerfeld [Generalized inductive definitions. The \(\mu\)-calculus and \(\Pi^1_2\)-comprehension. Thesis. Münster: Univ. Münster (2002; Zbl 1050.03040)] to have the strength of \(\Pi^1_2-\mathbf{CA}_0\). In Section 2 we interpret the intuitionistic \(\mu\)-calculus in the theory \(\mathbf{EETJ}\!\!\upharpoonright +\,\, \mathbf{ UMID}_N\). The question about the strength of monotone inductive definitions in \(\mathbf T_0\) was asked by S. Feferman in 1982, and – assuming classical logic – was addressed by M. Rathjen.


03F50 Metamathematics of constructive systems
03D70 Inductive definability
03F35 Second- and higher-order arithmetic and fragments
03F55 Intuitionistic mathematics


Zbl 1050.03040
Full Text: DOI


[1] The L. E. J. Brouwer centenary symposium pp 77– (1982)
[2] Logic colloquium ’78 pp 159– (1979)
[3] DOI: 10.1007/BFb0062852
[4] DOI: 10.1016/S0168-0072(02)00065-9 · Zbl 1022.03045
[5] DOI: 10.1016/S0168-0072(96)00040-1 · Zbl 0877.03027
[6] DOI: 10.1016/0168-0072(89)90019-5 · Zbl 0665.03037
[7] Explicit mathematics with the monotone fixed point principle. II. Models 64 pp 517– (1999) · Zbl 0930.03093
[8] Explicit mathematics with the monotone fixed point principle 63 pp 509– (1998)
[9] Monotone inductive definitions in explicit mathematics 61 pp 125– (1996)
[10] Reflections on the foundations of mathematics: Essays in Honour of Solomon Feferman 15 pp 329– (2002) · Zbl 1001.00020
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.