[Agda] termination proofs
Serge D. Mechveliani
mechvel at botik.ru
Tue Sep 25 18:33:26 CEST 2012
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
More information about the Agda
mailing list