Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <09340-0@swan.cl.cam.ac.uk>; Fri, 15 May 1992 13:38:17 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03027;
          Fri, 15 May 92 05:17:33 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA03023;
          Fri, 15 May 92 05:17:27 -0700
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <08751-0@swan.cl.cam.ac.uk>;
          Fri, 15 May 1992 13:17:40 +0100
To: etxhsan@se.ericsson.brazil
Cc: Tom.Melham@uk.ac.cam.cl, info-hol@edu.uidaho.cs.ted
Subject: Recursive Functions in HOL
Date: Fri, 15 May 92 13:17:37 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.753:15.04.92.12.17.43"@cl.cam.ac.uk>


Regarding:

> Girard has shown that every function from natural numbers to natural numbers
> that can be proved total by using second-order aritmetic can be expressed in
> his polymorphic typed lambda calculus. (this includes not only primitive
> recursice functions but also Ackermann's function).
> 
> Does there exists a similar result for the HOL logic?

I'm not sure about that. But every general recursive function is representable
in the closely related Q_0^\infty system of Andrews. I'd be very surprised if
a similar result did not hold for HOL.

Tom