Re: Cantorian pseudomathematics

Keith Ramsay wrote:
> An expert in constructivism once said to me that there
> seemed to be areas in classical mathematics that had no real
> corresponding area in constructive mathematics, but I don't
> think he meant it in the sense of individual results, since
> he'd recently been explaining that for each theorem X of
> classical mathematics, there was a corresponding theorem
> AC->X of constructive mathematics, where AC is the axiom of
> choice. When the axiom of choice isn't used, one could
> consider LEM->X instead, where LEM is the law of excluded
> middle. (The axiom of chioce implies the law of excluded
> middle.) They correspond in the sense that when someone
> working constructively sees announced the classical result
> X, they can consider the proof as a proof of AC->X, and if
> someone working classically sees announced a constructive
> proof of AC->X, they can consider it a classical proof of X.

> But an area in mathematics is more than just a unmotivated
> pile of theorems. 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.
>
> Some results like Cantor's theorem are perfectly natural for
> a constructive mathematician like Bishop. The general theory
> of cardinality as pursued by classical mathematicians seems
> a bit curious from a constructive point of view. The original
> definition of cardinality is equivalent to asking for various
> sets X and Y whether there is an injection from X to Y. When
> one proves constructively that there is one, in many cases
> that means one has constructed a continuous, computable
> injection from X to Y. So it seems to me that constructively,
> this question has something in common with topology. But the
> classical results are about something else (coarser). The
> manner in which LEM entails the existence of an injection,
> which does not necessarily exist otherwise, is some more
> convoluted relationship. It's possible (how would we rule it
> out?) that there is some more natural relationship that entails
> with LEM the existence of an injection from X to Y, but which
> would make better sense to study constructively.
>
> There are some interesting tools for attempting to pry some
> constructive content out of theorems. I can only assume that
> there are others that we just don't know about. Goedel's
> Dialectica interpretation (from his paper in volume 12 of the
> journal Dialectica) translates a theorem, in arithmetic for
> example, into a form
>
> (Ew) (Ax) P(w,x)
>
> where w is a "witness" that can be extracted from the proof
> of the theorem, P(w,x) is decidable, and x is a variable
> ranging over a type. So this is something like what we were
> discussing a few days ago, with the difference that the type
> is not necessarily the type of the natural numbers.
>
> For arithmetic, the types needed are the finite types where
> 0 corresponds to the natural numbers, 1 to the computable
> functions from natural numbers to natural numbers, and in
> general n+1 corresponds to the type of computable functions
> from objects of type n to the natural numbers.
>
> I know there are extensions to certain stronger systems than
> arithmetic, but I haven't studied them much.
>
> There is a famous Curry-Howard "proofs as programs"
> correspondence for various systems. I believe the system Coq
> for automated (constructive) proof verification has a known
> such correspondence, allowing one in principle to execute
> proofs as programs.
>
> There have been those who have worried that mathematics has
> paid too little attention to constructive content, become too
> speculative, and things like that, but even those criticisms
> are quite different from supposing that it's gotten to the
> point of completely lacking content in large areas.
>
> Keith Ramsay

Thank you for that very generous post, which is yet another one of
yours that I have saved for my reference.

MoeBlee

.

Relevant Pages

  • Re: does sqrt(2) exist in CM?
    ... |> | or EXPLICIT definability, ... constructive mathematics and other kinds is what we mean ... I believe Troelstra's understanding of constructivism is ... According to Konig's lemma, it has an infinite ...
    (sci.math)
  • Re: Choice sequences, intuition, etc
    ... Now the doctor may nuance this view in certain ... mathematics, not at all. ... between constructivism and other philosophies to a matter ... in terms of personal taste are tacitly wishing that the ...
    (sci.logic)
  • Re: Cantorian pseudomathematics
    ... |> An expert in constructivism once said to me that there ... |> seemed to be areas in classical mathematics that had no real ... |> injection from X to Y. So it seems to me that constructively, ... question of the existence of injections from one space to ...
    (sci.math)
  • Re: A Modest Proposal
    ... On Jan 17, 4:48 am, Bill Taylor ... |> remember whether the mathematics they are reading is constructive ... classical ones is also typical for constructivism. ... "We in the majority, because we have the weight of tradition on our ...
    (sci.logic)
  • Re: Cantorian pseudomathematics
    ... I am also claiming that we can build a new formalism for mathematics ... For constructivism, lists are a much more natural structure than sets, ... and the axiom of choice for lists is trivially true. ... existence in what I am doing. ...
    (sci.math)