Equivalence of bar recursors in the theory of functionals of finite type

DOI10.1007/BF01620763zbMath0665.03042MaRDI QIDQ1115867

Marc Bezem

Publication date: 1988

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

deduction theorembar recursionextensionality rule

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15)

Related Items

The equivalence of bar recursion and open recursion

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• Ein starker Normalisationssatz für die bar-rekursiven Funktionale