Thumbnail
Access Restriction
Open

Author Escardó, Martín ♦ Oliva, Paulo
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Bar Recursion Product Selection Function ♦ Iterated Product ♦ Skewed Selection Function ♦ Full Classical Analysis Pa Ca ♦ Different Binary Product ♦ Ha Acn Dns ♦ Dependent Binary Product ♦ Modified Realizability ♦ Simple Product ♦ Pa Ca ♦ Dialectica Interpretation ♦ Quantifier-free Calculus ♦ So-called Dialectica Interpretation ♦ Bar Recursion ♦ Modified Bar Recursion ♦ Spector Bar Recursion ♦ Selection Function ♦ Negative Translation ♦ Full Classical Analysis
Abstract 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. §1. Introduction. Gödel’s [13] so-called dialectica interpretation reduces the consistency of Peano arithmetic to the consistency of the quantifier-free calculus of functionals T. In order to extend Gödel’s interpretation to full classical analysis PA ω + CA, Spector [19] made use of the fact that PA ω + CA can be embedded, via the negative translation, into HA ω + ACN + DNS. Here PA ω
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article