2026-07-21T19:38:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3234 2024-03-06T10:33:59Z ddc:004 open_access

System T and the Product of Selection Functions Escardo, Martin Oliva, Paulo Powell, Thomas primitive recursion product of selection functions finite choice dialectica interpretation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Martin Escardo and Paulo Oliva and Thomas Powell 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.233 urn:nbn:de:0030-drops-32341 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.233 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode