Fixed point theories and dependent choice
type: Item
instance of: scholarly article
title: Fixed point theories and dependent choice
zbMATH Open document ID: 0956.03051
author: Gerhard Jäger
author: Thomas Strahm
published in: Archive for Mathematical Logic
publication date: 2001-03-13T00:00:00Z
review text: ATR is Friedman's famous system of second-order arithmetic for arithmetical transfinite recursion; \(\text{ATR}_0\) is ATR with induction on the natural numbers restricted to sets of natural numbers; \((\Sigma^1_1\text{-DC})\) is the usual schema of dependent choice for \(\Sigma^1_1\) formulas. With \(\widehat{\text{ID}}_\alpha\) we denote the first-order system for \(\alpha\) times iterated fixed points generated by positive arithmetic operator forms; \(\widehat{\text{ID}}_{<\beta}\) denotes the union of the theories \(\widehat{\text{ID}}_\alpha\) for \(\alpha<\beta\). In this paper we establish the proof-theoretic equivalence of (i) ATR and \(\widehat{\text{ID}}_\omega\), (ii) \(\text{ATR}_0 + (\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\omega^\omega}\), and (iii) \(\text{ATR} +(\Sigma^1_1\text{-DC})\) and \(\widehat{\text{ID}}_{<\varepsilon_0}\).
reviewed by: Thomas Strahm
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 1547900
zbMATH Keywords: second-order arithmetic
zbMATH Keywords: arithmetical transfinite recursion
zbMATH Keywords: dependent choice
zbMATH Keywords: fixed points
MaRDI profile type: Publication
full work available at URL: s001530050161
OpenAlex ID: W2010039716
DOI: 10.1007/S001530050161
description: scientific article; zbMATH DE number 1547900