[FOM] Fwd: invitation to comment

[William Tait]

In 

> So in this respect, Gödel's proof of Con_{PA} in the Dialectica paper  is superior to Gentzen's, for it begins with nothing more than the mere acceptance of the finite types based on the natural numbers. For once we simply admit these, the theory T is given: finite iteration applied to operations on domains D that are k-tuples of finite types is given.

please read "Cartesian products of some k finite types" for  " k-tuples of finite types".

Bill Tait