Extended bar induction in applicative theories
type: Item
instance of: scholarly article
title: Extended bar induction in applicative theories
zbMATH Open document ID: 0717.03024
DOI: 10.1016/0168-0072(90)90047-6
author: Gerard R. Renardel de Lavalette
published in: Annals of Pure and Applied Logic
publication date: 1990-01-01T00:00:00Z
review text: This paper presents several important results of constructive mathematics on a meta-level. A sketch of the type-free theory with total application TAPP, which is an extension of APP, is given. The author shows that \(TAPP+EAC\) (extended axiom of choice) is conservative over HA (Heyting arithmetic) by using the method of forcing on a monoid, and that the same holds for \(TAPP+EAC\) with inductive definition. The author presents a novel proof of the theorem that \(ML_ 0\) (Martin-Löf's type theory without universes) is conservative over HA. The author studies the principle of extended bar induction (EBI), especially the arithmetical extended bar induction of type zero \(EBI^ a_ 0\). Extending TAPP and EL to \(TAPP^*\) and \(EL^*\) with sequence variables, the author proves that \(TAPP^*+EBI^ a_ 0\) and \(EL^*+EBI^ a_ 0\) both are arithmetically equivalent with \(ID_ 1\) (HA with non-iterated inductive definitions).
reviewed by: Fangmin Song
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 4181326
zbMATH Keywords: total applicative theory
zbMATH Keywords: intuitionistic arithmetic
zbMATH Keywords: constructive mathematics
zbMATH Keywords: type-free theory with total application
zbMATH Keywords: TAPP
zbMATH Keywords: extended axiom of choice
zbMATH Keywords: Heyting arithmetic
zbMATH Keywords: forcing on a monoid
zbMATH Keywords: inductive definition
zbMATH Keywords: Martin-Löf's type theory without universes
zbMATH Keywords: extended bar induction
MaRDI profile type: Publication
full work available at URL: 0168-0072(90)90047-6
OpenAlex ID: W2085036336
cites work: Goodman's theorem and beyond
cites work: Q3679172
cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
cites work: Q3029009
cites work: Q4128540
cites work: Q3882452
cites work: The faithfulness of the interpretation of arithmetic in the theory of constructions
cites work: The theory of the Gödel functionals
cites work: Relativized realizability in intuitionistic arithmetic of all finite types
cites work: Proof-theoretical analysis: Weak systems of functions and classes
cites work: Sheaf models for choice sequences
cites work: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
cites work: Q5343325
cites work: Formal systems for some branches of intuitionistic analysis
cites work: Constructive mathematics and computer programming
cites work: Q5519134
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q3887457
cites work: On the syntax of Martin-Löf's type theories
cites work: Constructivism in mathematics. An introduction. Volume I
description: scientific article; zbMATH DE number 4181326