[FOM] Gödel's functional interpretation

[William Tait]

On May 29, 2011, at 3:27 PM, Añon Barfod wrote:

> 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:
>> 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.

The reference should be to Avigad and Feferman. 

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.

I do wish that Voevodsky would stop writing "there is no mathematical proof that it terminates", since that statement is, as numerous postings attest, literally ambiguous.  There are arguments for Con_{PA} or Con_{T} which most of is would accept as mathematical proofs; but we don't accept them as establishing the consistency of PA or T, resp.

Bill Tait