FOM: human well-being; constructivism; anti-foundation

[Andrej.Bauer@cs.cmu.edu]

(1) A question:

Matthew Frank <mfrank at math.uchicago.edu> writes:
> Hilbert responded to Brouwer (according to Reid's biography, p. 184)
> with a slight variation of this: "with your methods most of the
> results of modern mathematics would have to be abandoned, and to me
> the important thing is not to get fewer results but to get more
> results."

I've heard several times (e.g. Beeson's Foundations of Constructive
Mathematics) that both Hilbert and Brouwer _erroneously_ expected that
"most results of modern mathematics would have to be abandoned" in an
intuitionistic setting. Does anyone know of _specific_ remarks or
comments by Hilbert and/or Brouwer that would indicate more precisely
which theorems or parts of mathematics they expected to evaporate
under intuitionism?


(2) A comment:

Matthew Frank <mfrank at math.uchicago.edu> writes:
> Simpson had said: "Bridges/Richman do not comment on *why* one might
> choose one system [of constructive math] over another, except to say
> that Bish[op-style math] may be better, because it assumes less."

If we think about constructive mathematics from a computational point
of view (what other view is there?), then we can explain perfectly
well why there are many constructive settings: logic and constructive
reasoning principles, e.g., Markov's Principle, Number Choice, Fan,
are dictated by the choice of the underlying computational model. It
is _not_ the case that all reasonable computational models are
equivalent to the Turing machine model, at least not in the sense of
realizability theory.

Two examples: (a) in a programming language with a "timeout" construct
every real function is uniformly continuous on closed intervals (b) in
a programming language with a "quote/unqoute" construct Church's
Thesis holds.

Bishop-style math is the common core of classical math and
constructive math"s". That's why it's important.

Which system of constructive math should one choose? That's like
asking which geometry is the best. [Bait: and sticking to classical
logic because it is "true" is like claiming that Euclidean geometry is
the true geometry of our space.]

If one has applications in mind, then one will choose that
constructive setting which corresponds to the computational model
(programming language) one is using. Without an application in mind
the obvious thing for a logician/mathematician to do is to study _all_
constructive settings and their relationships.


Andrej Bauer

Pure and Applied Logic
School of Computer Science
Carnegie Mellon University