Re: (Not quite) Cantor's diagonal proof

From: Ross A. Finlayson (raf_at_tiki-lounge.com)
Date: 10/28/04 

Date: Wed, 27 Oct 2004 21:20:16 -0700

Josh Purinton wrote:

> In article <3c6b9c1e.0410261813.2fb2fa5b@posting.google.com>,
> Ross A. Finlayson <raf@tiki-lounge.com> wrote:
> > Norm, infinite sets are equivalent.
>
> Not in ZFC.
>
> Sadly, Norm's prediction that "the skeptics won't put in the minimal
> effort needed to identify where they claim the formal proof is wrong"
> has been accurate so far.
>
> It seems likely that computer-verified proofs will eventually be quite
> common. When that day comes, the "skeptics" -- in order to avoid being
> ignored -- will have to produce (or at least critique) formal proofs
> that have been verified by a widely-accepted proof checking program
> using standard axioms and definitions.
>
> As Norm wrote in _ Metamath: A Language for Computer Mathematics _
> <http://us.metamath.org/#book>:
>
> Mathematicians sometimes have to put up with the annoyance of cranks
> who lack a fundamental understanding of mathematics but insist that
> their "proofs" of, say, Fermat's Last Theorem be taken seriously. I
> think part of the problem is that these people are misled by informal
> mathematical language, treating it as if they were reading ordinary
> expository English and failing to appreciate the implicit underlying
> rigor. [...] With easily accessible computer-based abstract
> mathematics, a mathematician could say to a crank, "don't bother me
> until you've demonstrated your claim on the computer!"
> --
> Josh Purinton

I disagree with you.

Review each of Megill's ruclem1 through ruclem39, the list of lemmas or
assertions towards his theorem.

Consider ruclem33, that g is non-empty. For EF, g is finite.

Consider ruclem32, that all values of g are less than all values of f:
not so.

There seems to be errors of a sort in this machine-readable data of
"ruclem"'s piling onto "ruc", presumably short for "reals are
uncountable", a concise English language definition that is succinct,
clear, to-the-point, unambiguous, and otherwise somewhat more simple for a
human being to verify than a computer.

Keep in mind the data processing credo: garbage-in, garbage-out, it
applies to human inference as well.

I'm not against computer verification of proofs, on the contrary, I think
that it is pretty clear that Norm was having some difficulty encoding
Cantor's first proof or the antidiagonal proof as applied to reals into a
computer-tractable form, indicating to some extent their fallacy, although
to be fair he just said that they were inelegant.

Now for "ruc", the only lemma of interest is "ruclem39", that claims no
surjection from N onto R, the rest if an assumption of no bijection where
N is a subset of R is trivial. Lemma "ruclem39" refers to 38, refers to
37, ..., refers to 33, refers to 32.

So, careful analysis of the correct, unambiguous, plain language
description is just as good as reverse engineering the digital symbolic
manipulations that can be implemented on a five dollar chip that fits in a
button, or even out of pebbles laid in a row and moved according to rules,
the grey matter bag encased within the human skull with tens of thousands
of interconnected neurons, connected to the senses and motor functions,
wins again.

The computer does many things well, it's a space heater, paperweight,
_and_ it crunches numbers. I do concur that computer verification of
proofs can be an important tool, and there is even work towards automated
generation of proofs, and search for proofs, and even inductive logic
perhaps surpassing individual human capability, and those computers were
designed using software on other computers. Millions of years of human
evolution and forty years of the computer age have produced some excellent
computers.

About ZFC, the Zermelo-Fraenkel set theory with as well the Axiom of
Choice (also known as the well-ordering principle, Zorn's lemma,
etcetera), if anything is a set and everything is a set and thus
everything is a set, and as well, the set of all sets, yet the set of all
sets is deemed irregular and non-existent, is not ZFC empty?

When I say that EF is illustrated to be a bijection between naturals and
the unit interval of the reals with adequate consideration of Cantor's
first proof and the antidiagonal argument, do you consider why Megill
wants to find yet another result along those lines, or why codification of
those into his program is unfeasible?

Do you think Skolem was a crank, Josh? What's your interest?

Can you draw a single continuous line if you lift, move, and then drop the
pencil at some point on the line? (Yes.) What if you can only stipple?

So anyways, I am happy to address Norm's cogent and verbose input to his
syntax and type checker, if you would, as I'm not using his program yet,
please address my point about his informal description of his argument,
that is expected to be readily interpreted as the formal argument.

Warm regards,

Ross Finlayson

Quantcast