[Haskell-cafe] Gödel's System T
Dan Doel
dan.doel at gmail.com
Wed Nov 10 17:21:16 EST 2010
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
More information about the Haskell-Cafe
mailing list