Re: Cantorian pseudomathematics

david petry wrote:
|Keith Ramsay wrote:
|> david petry wrote:
|> I don't see how one can practically speaking prevent oneself,
|> as one is doing constructive mathematics, from dealing
|> sometimes with statements of the form X->Y where it turns
|> out afterward that (sometimes) X is not constructively valid,
|> but is nonconstructively provable.
|>
|> We had a discussion of statements of the form X->Y where X
|> is false, and one of my points there was that we need to be
|> able to proceed in a way that doesn't require us to declare
|> things to be nonsensical retroactively. If I can't tell, just
|> by looking at X, whether it's "okay" to use it as a premise,
|> even just hypothetically, then there's something wrong with
|> your notion of "okay".
|
|But we can tell, just by looking at X, whether it is a constructively
|meaningful statement. Sometimes it is not so clear when the statement
|is made in informal natural language, though.

I think that when you "just look at" a statement and decide
whether it is "constructively meaningful" you do it in a
naive way. Going with your gut on these things is a bad idea.
You need to spend more time dealing with criteria that are
explicit enough that someone can tell whether a statement
qualifies or not without being you.

|When you write "we had a discussion...", are you talking about fifteen
|years ago?

No, I didn't mean "you and I"; I meant a recent discussion
of implication where someone had another one of these naive
gut reactions to the effect that if X is false, X->Y should
be regarded as "meaningless" rather than true.

| I vaguely recall such a discussion, but the problem was
|with the interpretation of X->Y. Usually we say that X->Y is
equivalent
|to "I have a way to convert a proof of X into a proof of Y", in which
|case X must be a constructively meaningful statement (i.e. it must
make
|predictions about the results of computational experiments). But it
|might also be interpreted as not(X) OR Y, in which case, not(X) must
be
|constructively meaningful.

For X->Y to be meaningful X has to be meaningful, but this
just begs the question of what it takes for X to be
"meaningful". My point here is that one has to distinguish
between X being meaningless and X being unacceptable for
some other reason, like its being false.

Errett Bishop's constructive analysis textbook in at least
one edition contains a mistake regarding AC. He made a
mistake which led him to think it was true. So if there
is some way that one can just magically intuit its
unacceptability from a constructive point of view by just
looking at it, for the first time, it is at least a method
that had escaped his attention.

No, AC is something that is eventually realized to be not
constructively acceptable *AFTER* some consequences have
been deduced from it. If your claim about it was correct,
one would have to decide retroactively to invalidate the
deductions of the form AC->X that had been made, once it
was discovered to imply the law of excluded middle and the
rest.

|>
|> |> And also it's not clear that every
|> |> constructive theorem in the sense he and I were considering
|> |> is constructive in the sense you and I are considering.
|> |
|> |I would say not.
|>
|> So, I was pointing out the contrast between your idea and
|> the one I more often consider.
|>
|> In the context of explaining why it's not clear to me that
|> a "lot" of "Cantorian mathematics" will never have a
|> constructive counterpart, in your sense, the point is (1) it
|> always has a constructive counterpart in a broad sense, and
|
|Proving theorems like AC->X is not doing constructive mathematics,
even
|in a "broad" sense.

So now you're ready to explain what core, essential aspect
of the concept of "constructivity" it violates? No. Of
course not. You derive too much enjoyment from glibly
tossing off such claims for stopping to examine the
principles in question to be attractive to you.

Constructivity is typically explained in terms of the
meaning assigned to existential quantifiers. In particular,
each existence claim should be accompanied by a
"construction", where it is often left rather vague as
to what should be counted as a "construction".

One case, however, is more crucial than most people who've
heard of constructivism realize, and that's the case of
integers (and consequently other finite combinatorial
constructions). A constructive proof that an integer exists
must (by the nature of the concept of "constructive") give
a way of computing it (in decimal form, say). A second case
that is less crucial but generally fits people's intuitions
about what "constructive" should mean is that a construction
of a set should give us a way to express it as {x:P(x)} for
some explicit property P.

So for an axiom system we have two natural criteria for
constructivity, known as the numeric existence property
and the set existence property. It has the numeric existence
property if there is a procedure for converting a proof of
a statement of the form (En)Q(n) where n ranges over the
integers into a proof of Q(n) for a specific n given in
decimal form. It has the set existence property if there is
a procedure for converting a proof of a statement of the
form (ES)Q(S) where S ranges over sets (of some kind) into
a proof of a statement of the form Q({x:R(x)}) for some
predicate R.

There are two fundamental axioms famous for creating
problems with the numeric and set existence principles.
Most mathematically trained people are aware of proofs
using the axiom of choice of the existence of things like
a Vitali set (with one representative from each member
of R/Q) where one doesn't expect to be able to give an
explicit example. This is associated with ZFC's failure
of the set existence principle. Now a lot of people don't
realize this can be patched over by going to ZF+V=L,
where V=L implies AC. But set theorists usually seem to
prefer axioms that contradict V=L so it doesn't make much
difference. The second and more serious issue is with the
way the law of excluded middle destroys the numeric
existence principle.

Not every constructivist is "happy" with every formal system
satisfying the numeric and set existence properties. I don't
know of any additional requirement, however, for which there
is a consensus that it is a necessity for a system to be a
"constructive" system, and its proofs "constructive" proofs.
Among people who want proofs to be constructive, I suppose
there's often interest in their being predicative as well.
It strikes me as somewhat arbitrary and severe to say that
this is some kind of absolute requirement.

Then there's the issue of "computational meaning".

Some famous judge said of pornography that he couldn't
define it precisely but could recognize it when he saw it.
If one wants to be able to say something more satisfying
than that about mathematics that is "obscenely" lacking in
computational meaning, then one has further work to do.

You seem not to believe me when I say it, but there's a
simple, straightforward way of applying the "mathematical
theories must make predictions" rule that tells us to dump
the same two axioms, and nothing else. Take "computational
predictions" to mean only the most obvious kind of thing,
namely, statements of the form (n)P(n) where n ranges over
the integers and P is a primitive recursive predicate.
Then say that an axiom system should be no more complicated
than necessary to entail all conclusions of that form that
it does.

By the work of Goedel on AC, we can show that removing it
has no effect on which arithmetic statements we can prove,
let alone the kind of computational prediction I'm
considering here. Likewise there are some basic results on
the law of excluded middle that show it also doesn't give
us any more "predictions" than we had to begin with. I don't
know whether it counts as a coincidence or not, but these
are the same two axioms as were nonconstructive in the
obvious way.

The rest of the axioms in ZFC do give new predictions. The
axiom of replacement is often written in a form implying
the law of excluded middle, but it can be written not to.
Without AC or LEM this leaves us with a system called IZF
that satisfies the numeric and set existence properties.
I guess it's not very well liked for practical use, but in
a theoretical way it nicely matches ZFC. One can prove the
existence of the same recursive functions in each for
instance.

IZF can prove the consistency of IZF with the axiom of
replacement removed, which IZF with the axiom of replacement
removed can't do (by Goedel's second incompleteness theorem).
Since a consistency statement is equivalent to one of the
form (n)P(n) this counts as some kind of additional
prediction.

IZF with the axiom of replacment removed can prove the
consistency of IZF with the power set axiom and the axiom
of replacement both removed.

IZF with both the power set axiom and the axiom of replacement
removed can prove the consistency of IZF with the axiom of
infinity removed. If the axiom of infinity is replaced with
its negation, we get a system essentially the same as elementary
arithmetic. There's a model of it consisting only of the sets
that can be built up in finitely many steps from the empty set.

The only way to get the full "computational content" is to
keep all the axioms in IZF. Presumably there's some way
to simplify the system by replacing axioms, but none of
the axioms can be just tossed out.

|> (2) I don't see where, within mathematics seen from a
|> constructive point of view, it is supposed to be that it
|> departs from having computational meaning. We could consider
|> cases where someone was investigation a question of the form
|> X->Y and eventually found that X is false, that there were
|> no examples of the kind of thing they were investigating, and
|> things like this, but as long as it's decided after the fact,
|> and there isn't a criterion we can use in advance to see that
|> the question lacked content, I don't think it counts.
|
|Actually, I can't really follow that paragraph. But the question of
|whether a statement has computational meaning is independent of
whether
|it has been proven.

I'm talking in that paragraph about your apparent wish to
draw a line between "computationally meaningful" and "not
computationally meaningful". I can relatively easily see
how you could decide that certain bits of nonconstructive
mathematics should be left on the "not computationally
meaningful" side of the line. But then you appear to want
to draw your line so that it passes somewhere *inside* of
what I describe as constructive mathematics.

The criteria I described above give us a principled way to
designate certain kinds of mathematics as nonconstructive.

Is there a principled way to designate some of the
mathematics that counts as constructive by those criteria,
and say that, nevertheless, it lacks computational meaning?
As far as I can tell, you just go on your own gut reaction,
without any principle that someone not sharing your
intuitions could apply in a consistent way. It's hard to see
how one could in a principled way dispose of all the
"Cantorian" mathematics you have such a problem with
(Cantor's theorem as usually understood, for pity's sake)
without being rather draconian. It's hard to see how one
could in a principled way accept the applied math you are
friendly toward without accepting just about everything.

|> |> Some results like Cantor's theorem are perfectly natural for
|> |> a constructive mathematician like Bishop.
|> |
|> |You might say that, but the constructive version of Cantor's
theorem is
|> |not the same theorem as the classical version.
|>
|> I don't know in what relevant sense you consider them not
|> the same.
|
|I know we've discussed this a few times before. The result that is
not
|disputed by either constructivists or classical mathematicians is that
|if we are given a well defined list of well defined real numbers (so
|that every digit of every number can be computed), then the diagonal
|method gives us a new number not on that list. The classical
|mathematicians claim, essentially, that the argument is still valid
|when the list and the numbers on the list may not be well defined.

You're equivocating between computable, which is a property
of certain objects, and "definedness" which is really a
property of the description of the object that needs to be
satisfied before one can ask whether the object described
by the description has some property or not.

You describe constructivists as if they automatically
assume that reals are computable. They don't. The argument
makes no use of any such assumption.

we can, moreover, understand what the classical mathematicians
have in mind when they talk about real numbers. They are
thinking of things that we can represent with sets of
rationals. Given two sets of rationals L and R, with L
downward closed and R upward closed, where

(*) For some epsilon>0, for every l in L and r in R, we
have r-l>epsilon.

leads to a contradiction, we have a "classical real". These
are not "undefined", although its nonconstructive to say
that these are the same as the honest-to-goodness reals.

We can use the same (Cantorian) reasoning to take a
sequence of classical reals and produce a new classical
real different from the terms of the sequence.

Keith Ramsay

.

Loading