Extended bar induction in applicative theories (Q753810)

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).