Extended bar induction in applicative theories
From MaRDI portal
Publication:753810
DOI10.1016/0168-0072(90)90047-6zbMath0717.03024OpenAlexW2085036336MaRDI QIDQ753810
Gerard R. Renardel de Lavalette
Publication date: 1990
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0168-0072(90)90047-6
constructive mathematicsHeyting arithmeticintuitionistic arithmeticinductive definitionextended axiom of choiceextended bar inductionforcing on a monoidMartin-Löf's type theory without universesTAPPtotal applicative theorytype-free theory with total application
Related Items (4)
Totality in applicative theories ⋮ Extensional realizability ⋮ Arithmetical conservation results ⋮ On Goodman realizability
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Sheaf models for choice sequences
- Proof-theoretical analysis: Weak systems of functions and classes
- On the syntax of Martin-Löf's type theories
- Goodman's theorem and beyond
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Constructivism in mathematics. An introduction. Volume I
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Constructive mathematics and computer programming
- The theory of the Gödel functionals
- Relativized realizability in intuitionistic arithmetic of all finite types
- The faithfulness of the interpretation of arithmetic in the theory of constructions
- Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
- Formal systems for some branches of intuitionistic analysis
This page was built for publication: Extended bar induction in applicative theories
