Extended bar induction in applicative theories (Q753810)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Extended bar induction in applicative theories |
scientific article |
Statements
Extended bar induction in applicative theories (English)
0 references
1990
0 references
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).
0 references
total applicative theory
0 references
intuitionistic arithmetic
0 references
constructive mathematics
0 references
type-free theory with total application
0 references
TAPP
0 references
extended axiom of choice
0 references
Heyting arithmetic
0 references
forcing on a monoid
0 references
inductive definition
0 references
Martin-Löf's type theory without universes
0 references
extended bar induction
0 references
0 references
0 references