On the definability of functionals in G\"odel's theory T

TL;DR

This paper investigates the definability of higher-type functionals in G"odel's theory T, showing that under certain restrictions, these functionals can be encoded as epsilon_0-recursive functions, extending known results about numerical functions.

Contribution

It extends the understanding of definability in G"odel's theory T to higher-type functionals, demonstrating their encoding as epsilon_0-recursive functions under specific conditions.

Findings

Functionals of arbitrary type in T can be encoded as epsilon_0-recursive functions when restricted to pure closed normal forms.

The result generalizes the known characterization of numerical functions definable in T.

Provides a bridge between higher-type functionals and classical recursion theory.

Abstract

Godel's theory T can be understood as a theory of the simply-typed lambda calculus that is extended to include the constant 0, the successor function S, and the operator R_tau for primitive recursion on objects of type tau. It is known that the functions from non-negative integers to non-negative integers that can be defined in this theory are exactly the <epsilon_0-recursive functions of non-negative integers. As an extension of this result, we show that when the domain and codomain are restricted to pure closed normal forms, the functionals of arbitrary type that are definable in T can be encoded as <epsilon_0-recursive functions.