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 <00724-0@swan.cl.cam.ac.uk>; Thu, 14 May 1992 12:08:29 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10181;
          Thu, 14 May 92 04:00:35 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from mailgate.ericsson.se by ted.cs.uidaho.edu (16.6/1.34) id AA10177;
          Thu, 14 May 92 04:00:28 -0700
Received: from brazil.ericsson.se 
          by mailgate.ericsson.se (4.1/SMI-4.1-MAILGATE1.10) id AA28353;
          Thu, 14 May 92 13:00:52 +0200
Received: from timor14.brazilyp ([130.100.180.16]) 
          by brazil.ericsson.se (4.1/SMI-4.1) id AA17295;
          Thu, 14 May 92 13:00:21 +0200
Date: Thu, 14 May 92 13:00:21 +0200
From: etxhsan@se.ericsson.brazil (Herbert Sander TAL VL6018 12160)
Message-Id: <9205141100.AA17295@brazil.ericsson.se>
To: toal@edu.ucla.cs, Andy.Gordon@uk.ac.cam.cl
Subject: Re: Ackermann's function
Cc: info-hol@edu.uidaho.cs.ted



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?


Herbert