Extended bar induction in applicative theories

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50)

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