[Haskell-cafe] Gödel's System T

[Dan Doel]

On Wednesday 10 November 2010 1:42:00 pm Petr Pudlak wrote:
> I was reading the paper "Total Functional Programming" [1]. I
> encountered an interesting note on p. 759 that primitive recursion in a
> higher-order language allows defining much larger set of function than
> classical primitive recursion (which, for example, cannot define
> Ackermann's function). And that this is studied in in Gödel's System T.
> It also states that this larger set of primitive functions includes all
> functions whose totality can be proved in first order logic.
> 
> I was searching the Internet but I couldn't find a resource (a paper, a
> book) that would explain this in detail, give proofs etc. I'd be happy
> if someone could give me some directions.

Girard's book, Proofs and Types, has some stuff on System T. A translation is 
freely available:

  http://www.paultaylor.eu/stable/Proofs+Types.html

Skimming, it looks like he gives an argument that T can represent all 
functions that are provably total in Peano arithmetic.

The rest of the book is also excellent.

-- Dan