Monotone Inductive Definitions in Explicit Mathematics
Rathjen, Michael
J. Symbolic Logic, Tome 61 (1996) no. 1, p. 125-146 / Harvested from Project Euclid
The context for this paper is Feferman's theory of explicit mathematics, $\mathbf{T_0}$. We address a problem that was posed in [6]. Let $\mathbf{MID}$ be the principle stating that any monotone operation on classifications has a least fixed point. The main objective of this paper is to show that $\mathbf{T_0} + \mathbf{MID}$, when based on classical logic, also proves the existence of non-monotone inductive definitions that arise from arbitrary extensional operations on classifications. From the latter we deduce that $\mathbf{MID}$, when adjoined to classical $\mathbf{T_0}$, leads to a much stronger theory than $\mathbf{T_0}$.
Publié le : 1996-03-14
Classification: 
@article{1183744930,
     author = {Rathjen, Michael},
     title = {Monotone Inductive Definitions in Explicit Mathematics},
     journal = {J. Symbolic Logic},
     volume = {61},
     number = {1},
     year = {1996},
     pages = { 125-146},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744930}
}
Rathjen, Michael. Monotone Inductive Definitions in Explicit Mathematics. J. Symbolic Logic, Tome 61 (1996) no. 1, pp.  125-146. http://gdmltest.u-ga.fr/item/1183744930/