Monotone inductive definitions in a constructive theory of functions and classes
type: Item
instance of: scholarly article
title: Monotone inductive definitions in a constructive theory of functions and classes
zbMATH Open document ID: 0665.03037
DOI: 10.1016/0168-0072(89)90019-5
author: S. Takahashi
published in: Annals of Pure and Applied Logic
publication date: 1989-01-01T00:00:00Z
review text: A constructive theory of functions and classes, \(T_ 0\), has been developed by \textit{S. Feferman} [Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)]. In a constructive framework, functions are given by algorithmic rules of construction and classes are given by defining properties. In the language of \(T_ 0\) we are able to formulate the least fixed point principle for monotone inductive definitions (MID) as: every monotone operation f on classes to classes has a least fixed point. The question due to \textit{S. Feferman} [The L. E. J. Brouwer Centen. Symp., Proc. Conf., Noordwijkerhout/Holl. 1981, Stud. Logic Found. Math. 110, 77-89 (1982; Zbl 0525.03037)] of the strength of \(T_ 0+M\) and some related questions are prime concern of this paper. Main results are: the consistency of \(T_ 0+MID\) (through constructing the corresponding model in set-theoretic sense) and the proof-theoretical equivalence between a subsystem \(EM_ 0+J+MID\) of \(T_ 0+MID\) and \(\Pi^ 1_ 1-CA\). This equivalence can be obtained by a careful examination of the analogous model construction for \(EM_ 0+J+MID\). The proof-theoretic strength of \(T_ 0+MID\) still remains open. Note that in any model of \(T_ 0\) the cardinality of the collection of classes is the same as the cardinality of the universal class \(V=\{x| x=x\}\) of all entities. So, it does not seem to be possible to use for MID the least fixed point theorem in ZF. There is a similarity with the ordinary Myhill and Shepherdson theorem that every monotone recursive transformation of the indexes of r.e. sets is described by a \(\Sigma^+\)-formula and has a least fixed point. However, in \(T_ 0\) classes are unlike r.e. sets, because they are closed under complementation operation. Hence, some additional ideas are used. The paper is selfcontained and clearly written.
Mathematics Subject Classification ID: 03D70
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 03D75
zbMATH DE Number: 4087655
zbMATH Keywords: proof-theoretic strength
zbMATH Keywords: combinators
zbMATH Keywords: constructive theory of functions and classes
zbMATH Keywords: least fixed point principle
zbMATH Keywords: monotone inductive definitions
reviewed by: Vladimir Yu. Sazonov
MaRDI profile type: Publication
full work available at URL: 0168-0072(89)90019-5
OpenAlex ID: W2035074687
cites work: Q4128540
cites work: Q3882452
cites work: Q3039340
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q4146722
cites work: Q3041187
cites work: Abstract First Order Computability. I
cites work: Effective operations on partial recursive functions
cites work: Q5573961
Wikidata QID: Q127207371
Recommended article: Monotone inductive definitions in explicit mathematics
Recommended article: Q4447153
Recommended article: Q3699688
Recommended article: Q4793037
Recommended article: Q3197877
Recommended article: A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE
Recommended article: Q5435636
Recommended article: Explicit mathematics with the monotone fixed point principle
Recommended article: La théorie intuitionniste des types : sémantique des preuves et théorie des constructions
Recommended article: On Tarski’s fixed point theorem
description: scientific article; zbMATH DE number 4087655