[Agda] termination proofs

Peter Hancock hancock at spamcop.net
Mon Sep 24 22:30:43 CEST 2012

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.


More information about the Agda mailing list