[Agda] termination proofs

[Peter Hancock]

On 25/09/2012 17:33, Serge D. Mechveliani wrote:
> On Tue, Sep 25, 2012 at 05:12:01PM +0100, Peter Hancock wrote:

>> (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 appreciate you were thinking classically.  That's fine.
After 2 millenia, we are finally beginning to understand classical logic.
Or some of it.

As for the subsets of a singleton, think of it like this:  there are
as many subsets of a singleton as there are propositions that can be stated
about the inhabitant of that singleton.  Now think of Curry-Howard.
To put it set-theoretically, the power-set of a singleton is not
a *set*, but a proper class.  (So I said, "arbitrarily many" (I think!).)

To repeat, I am sweeping some subtle things under the carpet.  I have not
said anything about when subsets are equal, or defended the Curry Howard
principle. In the last few years, these things have got a lot more subtle.
I am thinking of Voevodsky's ideas about "h-propositions", and equality between
"h-sets", and that sort of thing.

Nevertheless, leaving the powerset of a singleton aside, I still stand
by my countability argument.  (Probably rashly...)

Peter