[Agda] Re: Logical meaning of nontermination

[Vag Vagoff]

Samuel Gélineau wrote:
> I think the question is. ((⊥→⊥)→⊥) is a typo for ((P→⊥)→⊥), isn't it?
>
>   
Yes, exactly. That was a typo.
> Well, first of all, you need to be careful about what you mean by
> non-termination. Do you mean that the program has been checked not to
> terminate? On all inputs? Some inputs? Or has termination-checking
> simply failed to show that the program terminates on all inputs?
Thanks for pointing to it, it's very important for novices.
> Vag wants (I think) to interpret (NonT Q) as (Q →⊥).
>
>   
Yes, you are right.

> 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.
>
>   
Thanks! Now I think I understood it.