|
|
Re: what's all the excitement about intuitionistic logic?
Posted:
May 8, 2005 3:15 AM
|
|
alex goldman wrote:
[...]
|If I understand you correctly, every theorem in Intuitionistic Logic
is a
|theorem Classical Logic (because the former has a weaker set of
axioms).
Yes.
|Then how can it be that "[In Intuitionistic Logic] every function on
[0, 1]
|is uniformly continuous." ? (quoting Jim Spriggs from elsewhere in
this
|thread)
He didn't refer to intuitionistic logic. He referred to
intuitionistic mathematics. In Brouwer's intuitionism,
additional assumptions are made, some of which contradict
classical mathematics, and even classical logic.
For a real number x, let P(x) be the statement that either
x<0, x>0, or x=0. A real can be represented constructively
as a sequence of rationals x_n where |x_n-x_m|<=1/n+1/m
for every n,m>=1. To say x>0 is to say for some n, x_n>1/n.
To say x<0 is to say that for some n, x_n<-1/n. To say
x=0 is to say that for every n, -1/n<=x_n<=1/n.
Thus it's constructively valid to reason that if x<0 and x>0
are both false, then x=0, since x=0 is equivalent to denying
that x<0 or x>0 arise. Moreover, ~P(x), where "~" stands for
negation, is a contradiction in terms. Classically the
conclusion is that P(x), but constructively the conclusion
is ~~P(x). Writing (x) for "for all x", we get (x)~~P(x).
In Bishop's constructive mathematics, nothing's assumed that
contradicts classical mathematics, so (x)P(x) is not denied.
He names something equivalent to it the "limited principle
of omniscience" (LPO). It's also nonconstructive.
>From LPO a lot of the nonconstructive results of classical
analysis can be proven. For example, we can prove that there
exists a discontinuous function, such as f(x)=-1 if x<0,
f(x)=0 if x=0, and f(x)=1 if x>1, defined on the whole real
line.
Brouwer, on the other hand, has additional assumptions that
imply this continuity principle mentioned above. Hence in
Brouwerian intuitionism, we have ~(x)P(x). Thus in
intuitionism, unlike Bishop's constructivism, one has examples
where ~(x)P(x) and (x)~~P(x) are both theorems.
|Also, if you saying there is a purely mechanical procedure for
converting
|Classical Mathematics into Constructive Mathematics (by keeping track
of
|those not's), is there a program for converting Mizar libraries into
Coq
|ones?
As far as I know there isn't, and there are several reasons.
The double-negation embedding deals with the fact that one
uses classical logic and the other uses intuitionist logic.
But their axiom systems may be of differing strengths in
other respects. There's a correspondence between classical
and intuitionist systems, but they may be in different
positions in it. We could consider a classical system
Coq+LEM like the one in Coq but including the law of excluded
middle as an axiom, and the translation from Coq+LEM -> Coq
would work. We could also consider a constructive system
CMizar akin to Mizar but leaving out the law of excluded
middle or its equivalent, with a translation from Mizar into
CMizar.
For instance, it appears Mizar incorporates a Grothendieck
universe axiom, saying that if X is a set, then there's a
universe U that has X as a member, and for every member Y
contains every subset of Y, the power set of Y, and such that
every subset of U of cardinality less than U is a member of U.
That's a pretty strong assumption set theoretically, and I
don't know whether Coq has such a thing in it. However, I'm
pretty sure that this assumption is constructively acceptable.
Constructive systems tend to be more cautiously typed. Some
of them require you to be predicative.
Probably the main reason there's no such conversion is that
the resulting libraries wouldn't be very good for what one
wants if one is using Coq.
|If so, why study Constructive Mathematics at all?
Wouldn't it make more sense to ask, why study classical
mathematics at all?
If a classical mathematician has a conjecture X, it's possible
in principle for him to reformulate it as a constructive
conjecture Y that's equivalent, in the sense that a constructive
mathematician proving Y will provide the classical mathematician
with what is required for a classical proof of X, and vice-versa.
There are a couple of natural ways of doing this. The double
negation translation is one way. The results tend to be somewhat
ugly with all the double negations required. Another way is to
phrase Y as being X conditional on the additional assumptions he
is making. So for example one can ask whether, constructively,
the axiom of choice and law of excluded middle imply X.
The reverse does not work quite as naturally. I can pose a
constructive mathematical question where to express it as a
classical problem requires some dodge like asking instead whether
it's a theorem in some constructive formal system, or whether
it holds in the internal language of every topos, or whether
it holds in a Kripke or Beth model. All of these have somewhat
the effect of putting the question into a little isolated
chamber, a controlled sandbox. I don't see how a seamless
integration of the two is possible on such a basis.
Constructive mathematics permits one to ask, in some form,
all the questions asked in classical mathematics, plus some
additional ones that are difficult to formulate classically.
| If it's useful, one
|can get it as a side effect when more Classical Math is formalized.
|(e.g. http://www.cs.ru.nl/~freek/qed/qed.html )
A lot of mathematicians seem to have the impression that it's
reasonable to leave constructive mathematics as a kind of footnote
to the subject, because they think somehow the accumulation of
classical results is bound to wind up answering the constructive
questions in the end anyway.
I don't see that this works out. A few years ago I had a question
about a more effective version of the Jordan-Holder theorem in
group theory. If one were working it out constructively it would
be a fairly natural question to ask. But classically it's not.
Why should this kind of knowledge emerge as a "side effect" of
anything-- until the day that the side effect is somebody taking
the trouble to work it out constructively?
Keith Ramsay
|
|
