[Agda] Re: Logical meaning of nontermination

[Peter Hancock]

> So... after much deliberation, I do second Nils in his answer, even
> though I'm not sure he answered the right question. You can interpret
> a non-terminating proof of Q as a proof of (Q →⊥), but as Nils said,
> that gives you an inconsistent logic.

Maybe it's an almost totally red herring, but this reminds me of 
the usual way for proving completeness of eg classical predicate logic:  
If you have a non-terminating *search* for a proof of Q,
you use it to define a countermodel for Q. 

I'm not sure that "non-terminating proof" isn't an oxymoron.
What is non-terminating here?  Calculating the head normal form?
(I'm simply asking.)

If I could throw another red herring into the pot, I wonder what
people think of the idea of non-wellfounded proofs?  We might be
reasonably comfortable with non-wellfounded data-structures, but
I feel some reluctance to allow that *proofs* could be 
non-wellfounded in the same way. (Yes I am aware of Brotherston
and Simpson, but that is something very specific and restricted.) 
It's like a proof has to be a wellfounded structure to carry
conviction (from the premises to the conclusion). 

Hank