System T and the product of selection functions

Martín Escardó, Paulo Oliva, Thomas Powell

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

We show that the finite product of selection functions (for all finite types) is primitive recursively equivalent to Goedel's higher-type recursor (for all finite types). The correspondence is shown to hold for similar restricted fragments of both systems: The recursor for type level n+1 is primitive recursively equivalent to the finite product of selection functions of type level n. Whereas the recursor directly interprets induction, we show that other classical arithmetical principles such as bounded collection and finite choice are more naturally interpreted via the product of selection functions.
Original languageEnglish
Title of host publicationComputer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011
Pages233-247
Number of pages15
DOIs
Publication statusPublished - 2011
Event25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL - Bergen, Norway
Duration: 12 Sep 201115 Sep 2011

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume12
ISSN (Print)1868-8969

Conference

Conference25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL
CountryNorway
CityBergen
Period12/09/1115/09/11

Keywords

  • Dialectica interpretation
  • Finite choice
  • Primitive recursion
  • Product of selection functions

ASJC Scopus subject areas

  • Software

Cite this

Escardó, M., Oliva, P., & Powell, T. (2011). System T and the product of selection functions. In Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011 (pp. 233-247). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 12). https://doi.org/10.4230/LIPIcs.CSL.2011.233