[Agda] termination proofs

[Peter Hancock]

On 24/09/2012 20:55, Altenkirch Thorsten wrote:

> We are far beyond Arithmetic. I am sure Anton can give a better answer but
> I'd suspect that inductive-recursive definitions give you Pi_1^2-CA.

No.  It doesn't line up very tidily with second order arithmetic.
(According to Maichael Rathjen, it corresponds
to some weird fragment to do with a certain kind of "beta-model reflection" or something like that.
In any case, umpteen light years below Pi12CA.)
  
> Are there natural functions which are not provable total in such a theory?

Yes, if you mean ones with a short definition, as understandable as a
normalisation proof for such a theory.

Hank