A Direct Computational Interpretation of Second-Order Arithmetic via Update Recursion

EasyChair Preprint 8768

Abstract

Second-order arithmetic has two kinds of computational interpretations: via Spector's bar recursion of via Girard's polymorphic lambda-calculus. Bar recursion interprets the negative translation of the axiom of choice which, combined with an interpretation of the negative translation of the excluded middle, gives a computational interpretation of the negative translation of the axiom scheme of specification. It is then possible to instantiate universally quantified sets with arbitrary formulas (second-order elimination). On the other hand, polymorphic lambda-calculus interprets directly second-order elimination by means of polymorphic types. The present work aims at bridging the gap between these two interpretations by interpreting directly second-order elimination through update recursion, which is a variant of bar recursion.

Keyphrases: bar recursion, polymorphism, realizability, second-order arithmetic

@booklet{EasyChair:8768,
  author    = {Valentin Blot},
  title     = {A Direct Computational Interpretation of Second-Order Arithmetic via Update Recursion},
  howpublished = {EasyChair Preprint 8768},
  year      = {EasyChair, 2022}}