[Haskell-cafe] Gödel's System T
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.
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" . 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
>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.
>Haskell-Cafe mailing list
>Haskell-Cafe at haskell.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
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