[FOM] Gödel's functional interpretation

[Añon Barfod]

It would be interesting to hear what's Voevodsy's take on Gödel's
functional interpretation.

There's a proof theoretic discussion of the method in:

Feferman: "Gödel's functional dialectica interpretation", Handbook of
proof theory.

On May 21, 2011, at 3:26 PM, Vladimir Voevodsky wrote:

There is Gentzen's "proof" of consistency of PA. I looked through it
in the book by Takeuti who describes all the related definitions in
finitary terms. What the proof requires however is that certain
algorithm ("normalization" of the ordinals < epsilon ) always
terminates. This follows from the part of set theory which guarantees
the existence of epsilon but does not follow from anything else.

It is very typical, that the consistency issues are related to the
termination for different algorithms and in this case it is a very
explicit combinatorial algorithm but there is no mathematical proof
that it terminates.

Vladimir.