[Agda] termination proofs

[Serge D. Mechveliani]

On Tue, Sep 25, 2012 at 05:12:01PM +0100, Peter Hancock wrote:
>
>> The countability grounds is not relevant here, because I asked about an
>> _algorithmic_ map in  Nat -> Nat.
>
> For me, a function just *is* an algorithmic map which we can recognise as total.
> The normal Cantor diagonalisation argument shows that Nat->Nat is uncountable.
>
> I admit, this will seem strange at first, because there are only countably
> many Turing machines, and the total ones will be a subset of these.  But
> the notion of a cardinal is a bit strange constructively.  There are
> arbitrarily many subsets of a singleton, constructively.  I suggest that
> this argument is worth a bit more of your attention.
>
> (I also admit I am sweeping some subtle points under the carpet.)

I meant classical mathematics and classical logic. According to them,
the set of total Tuering machines is countable.
I try now to imagine many subsets of a singleton. And it comes out that 
there are as many as  2^1  of them, that is  2.

I like Agda, despite that understand nothing in a non-classical logic.
So far I, studied only that proofs are build as members of a dependent
type, and that negation for T is represented as  T -> \bottom
(if I do not confuse anything).

Regards,

------
Sergei