Re: Cantor Diagonal Proof

On 05/04/2025 12:36, Julio Di Egidio wrote:

On 04/04/2025 23:49, Lawrence D'Oliveiro wrote:

You should try and prove it formally, you'll see that it's you here
messing up definitions, even what a deductive system is, i.e. what
it means to prove things formally.

Meanwhile, since I have nothing to do:
My Gist, Cantor's diagonal argument (in Rocq):
<https://gist.github.com/jp-diegidio/eb05f6265c38b35c85853514ed46ab47>
<< We go for the simplest construction, which
    is not in terms of sets, just (type-theoretic)
    functions plus the most basic functional
    extensionality, i.e. eta-conversion. >>
In fact, learning some formal mathematics with some tool
that supports it I think makes one's informal mathematics
way sharper, especially for those who are self-thought
(whatever that means).
That said, I find my formalisation neither particularly
pretty nor particularly clear: corrections and suggestions
are welcome, especially in the direction of minimising
assumptions.
Julio