eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2011-08-31
233
247
10.4230/LIPIcs.CSL.2011.233
article
System T and the Product of Selection Functions
Escardo, Martin
Oliva, Paulo
Powell, Thomas
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol012-csl2011/LIPIcs.CSL.2011.233/LIPIcs.CSL.2011.233.pdf
primitive recursion
product of selection functions
finite choice
dialectica interpretation