[FOM] Gödel's functional interpretation

[William Tait]

On May 30, 2011, at 10:40 AM, William Tait wrote:
> The algorithm in this case is the one which, applied to a closed numerical term of Gödel's theory T, computes it---i.e. carries out a certain sequence of reductions via the explicit and primitive recursive definitions. The statement that this algorithm terminates with a numeral in each case implies (in PRA) consistency of T and so of PA.

Sorry: The second sentence should read

The statement that this algorithm terminates with a numeral in each case and that the result of reducing a constant numerical equation s=t should always be of the form n=n implies (in PRA) consistency of T and so of PA.


Bill Tait