An intuitionistic fixed point theory
type: Item
instance of: scholarly article
title: An intuitionistic fixed point theory
zbMATH Open document ID: 0903.03034
author: Wilfried Buchholz
published in: Archive for Mathematical Logic
publication date: 1998-12-14T00:00:00Z
review text: In the paper under review the author shows that the theory \(\widehat{ID} ^i_1\) is conservative over Heyting Arithmetic, \(HA\), w.r.t. almost negative formulas. \(\widehat{ID}^i_1\) is the extension of \(HA\) obtained by adding new predicate constants \(P_\Phi\) for every strongly positive formula \(\Phi (X,x)\) containing just free the individual variable \(x\) and the unary predicate variable \(X\), and the new axioms \((FP_\Phi)\) \(\forall x(\Phi(P_\Phi, x) \leftrightarrow P_\Phi x).\) Almost negative formulas (of the language \({\mathcal L}_0\) of number theory with function symbols for all recursive functions) do not contain \(\vee\) and contain \(\exists\) only for equations between terms [cf. \textit{A. S. Troelstra}, Metamathematical investigation of intuitionistic arithmetic and analysis (Lect. Notes Math. 344) (1973; Zbl 0275.02025), 3.2.9]. Strongly positive formulas are built up by atomic formulas of \({\mathcal L}_0\) and the unary predicate symbol \(P\) using the logical symbols \(\wedge, \vee, \exists, \forall.\) In \S 1, Theorem 1 is proved, namely that in \(HA + CT_0\) \((FP_\Phi)\) is provable, \(CT_0\) being Church's thesis (cf. Troelstra (loc. cit.)). As was shown in the introduction, Theorem 1 and material from Troelstra (loc. cit.) give Theorem 2, the above conservativity result. But this is not the whole story. The author assures that Theorem 2 can be generalized to: Theorem \(2'\). If \(\prec\) is a primitive recursive binary relation and \(TI (\prec \upharpoonright)\) the schema of transfinite induction over all proper initial segments of \(\prec\), then \(\widehat{ID}^i_1+TI(\prec \upharpoonright)\) is conservative over \(HA + TI(\prec \upharpoonright)\) w.r.t. almost negative formulas. This has interesting consequences for proof theory. Cut elimination and thus ordinal analysis of a semi-formal theory \(Th\) (also classical) can be formalized in \(\widehat{ID}^i_1+TI(\prec \upharpoonright).\) The definition of a derivability predicate \…
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 1156507
zbMATH Keywords: inductive definitions
zbMATH Keywords: extension of Heyting arithmetic
zbMATH Keywords: conservative extension
zbMATH Keywords: fixed point axiom
zbMATH Keywords: almost negative formulas
zbMATH Keywords: strongly positive formula
zbMATH Keywords: transfinite induction
zbMATH Keywords: proof theory
zbMATH Keywords: semi-formal theory
zbMATH Keywords: derivability predicate
zbMATH Keywords: Gödel translation
reviewed by: Helmut Pfeiffer
MaRDI profile type: Publication
full work available at URL: s001530050079
OpenAlex ID: W1987795668
DOI: 10.1007/S001530050079
Recommended article: Intuitionistic fixed point theories over set theories
Recommended article: Intuitionistic fixed point theories over Heyting arithmetic
Recommended article: An intensional fixed point theory over first order arithmetic
Recommended article: Intuitionistic fixed point logic
Recommended article: Fixed point theorems in constructive mathematics
Recommended article: Q3466577
Recommended article: Q4623093
Recommended article: On the Strength of the Uniform Fixed Point Principle in Intuitionistic Explicit Mathematics
Recommended article: Intuitionistic Fixed Point Theories for Strictly Positive Operators
Recommended article: Q3782439
description: scientific article; zbMATH DE number 1156507