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

Petr Pudlak deb at pudlak.name
Thu Nov 11 06:43:58 EST 2010

Thanks Dan, the book is really interesting, all parts of it. It looks 
like I'll read the whole book.

   Best regards,

On Wed, Nov 10, 2010 at 05:21:16PM -0500, Dan Doel wrote:
>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
>Haskell-Cafe mailing list
>Haskell-Cafe at haskell.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20101111/c17b75d9/attachment.bin

More information about the Haskell-Cafe mailing list