A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM

DOI10.1017/jsl.2017.33zbMath1406.03059arXiv1607.05237OpenAlexW2964235990MaRDI QIDQ4638975

Paulo Oliva, Silvia Steila

Publication date: 2 May 2018

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

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

zbMATH Keywords

logical relationsSpector's bar recursiongeneral bar recursionSchwichtenberg's closure theoremsystem \(\mathsf{T}\)

Mathematics Subject Classification ID

Structure of proofs (03F07) Functionals in proof theory (03F10)

Related Items (6)

Equivalence of bar induction and bar recursion for continuous functions with continuous moduli ⋮ Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions ⋮ Characterising Brouwer's continuity by bar recursion on moduli of continuity ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Higher order functions and Brouwer’s thesis

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Primitive recursion and the chain antichain principle
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• On bar recursion of types 0 and 1
• Ordinal analysis of simple cases of bar recursion
• On the No-Counterexample Interpretation
• An analysis of the Podelski–Rybalchenko termination theorem via bar recursion

This page was built for publication: A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM