Re: [Haskell-cafe] Gödel's System T
aaronngray.lists at gmail.com
Thu Nov 11 11:04:07 EST 2010
On 11 November 2010 11:43, Petr Pudlak <deb at pudlak.name> wrote:
> Thanks Dan, the book is really interesting, all parts of it. It looks like
> I'll read the whole book.
Watch out for the decidability issue though :-
> 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" . 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
>> freely available:
>> 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
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.10 (GNU/Linux)
> -----END PGP SIGNATURE-----
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe