[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,
Petr
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
>http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- 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