Bar recursion and products of selection functions

DOI10.1017/JSL.2014.82MaRDI QIDQ5251356zbMATH OpenOpenAlexFDO

Authors Martín Escardo, Paulo Oliva

Publication date 20 May 2015

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.7046

zbMATH Keywords

selection functiongeneralised quantifierT-definabilitymodified bar recursionspector bar recursion

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Higher-type and set recursion theory (03D65) Relative consistency and interpretations (03F25) Recursive equivalence types of sets and structures, isols (03D50)

Abstract: We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of "skewed" selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products.

Recommendations

• On Spector's bar recursion
• Bar recursion over finite partial functions
• System T and the product of selection functions
• Modified bar recursion
• The equivalence of bar recursion and open recursion

Cites work

• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Modified bar recursion
• On Spector's bar recursion
• Selection functions, bar recursion and backward induction
• Sequential games and optimal strategies
• The equivalence of bar recursion and open recursion
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(12)

• Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice
• The equivalence of bar recursion and open recursion
• Modified bar recursion
• Higher-order games with dependent types
• System T and the product of selection functions
• scientific article; zbMATH DE number 7297814 (Why is no real title available?)
• On Spector's bar recursion
• Validating Brouwer's continuity principle for numbers using named exceptions
• Selection functions, bar recursion and backward induction
• The Herbrand functional interpretation of the double negation shift
• Bar recursion is not computable via iteration
• Bar recursion over finite partial functions

This page was built for publication: Bar recursion and products of selection functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5251356)