[FOM] constructivism and physics

[Harvey Friedman]

On 2/8/06 9:34 PM, "Neil Tennant" <neilt at mercutio.cohums.ohio-state.edu>
wrote:

> The discussion on constructivism and physics appears to be based on the
> common assumption that the constructivist's task would be to serve up as
> (constructive) theorems all those theorems that physicists might have
> occasion to apply when making predictions about, and giving explanations
> of, empirical phenomena.
> 
> There is a quite different view, however, that allows the constructivist
> to claim adequacy of constructive mathematics for all possible
> applications in scientific reasoning, and which even explains why it is
> that (in light of this) it is so useful to have classical theorems
> available "off the shelf" for applications in science.
> 
> Please see
> 
> http://people.cohums.ohio-state.edu/tennant9/
> 
> and after clicking on the sidebar link "Articles", download (what is
> currently) article #1, `Logic, Mathematics and the Natural Sciences' , in
> Dale Jacquette, ed., Handbook of the Philosophy of Science. Volume 5:
> Philosophy of Logic, Elsevier BV, 2006, pp. 1149-1166.
> 

I have taken a very brief look at this paper. It raises a number of
interesting issues for f.o.m.

1. Tennant quotes Bridges on page 9 to the effect that "constructive
mathematics is none other than mathematics carried out with intuitionistic
logic."

2. This assertion of Bridges is at best very controversial. Let us take an
example. Normally Z_2 (not a great name) stands for the usual two sorted
first order theory of natural numbers and sets of natural numbers with full
comprehension in its language.

Z_2 has a well known and fairly well studied intuitionistic version, which
is the same except that intuitionistic logic is used.

It is well known that any Pi02 sentence provable in Z_2 is provable in
intuitionistic Z_2. See, e.g.,

H. Friedman, Classically and Intuitionistically Provably Recursive
Functions, Higher Set Theory, Springer Lecture Notes, Vol. 669, (1978), pp.
21-27. 

It is also well known that intuitionistic Z_2 also behaves like a very nice
intuitionistic system, in that, e.g., it shares many important metatheorems
with that old standby HA = intuitionistic first order arithmetic.

However, most constructivists yesterday, today, and tomorrow, will not
accept intuitionistic Z_2 as constructive. For that, they need to accept a
rather mysterious notion of "species" that Brouwer proposed.

I am not clear just how acceptable Brouwer found intuitionistic Z_2. But I
think the overwhelming majority of his successors would not find it
constructively acceptable. In particular, we know that Errett Bishop would
NOT find intuitionistic Z_2 acceptable constructively. (Stolzenberg could
comment on that).

3. So in light of 2, the onus is on Tennant.

4. Other interesting issues are raised as Tennant discusses possible blowups
in lengths of proof.

5. I didn't yet absorb all of the nuances in the ongoing argument between
Tennant and Burgess. But I think that I have some comments that may shed
light on just whatever they are arguing about.

6. The usual formal systems studied in f.o.m. are often quite relevant to
mathematical practice in terms of what can or cannot be proved in these
systems, how hard they are to prove consistent (relative consistency),
interpretability, as well as conservative extensions, etcetera.

7. However, the usual formal systems studied in f.o.m. are far too crude to
form the basis for a sensitive study of the lengths of proofs in actual
mathematical practice.

8. In particular, Tennant and Burgess seem to be looking at the usual kind
of formal systems studied in f.o.m. in terms of

proofs versus cut free proofs

with the principal issue being whether, when passing from proofs to cut free
proofs, one might start with a proof that is of reasonable length, and end
up with a proof of unreasonable length - and perhaps all cut free proofs may
be of unreasonable length.

9. Indeed, various formal results about the formal systems normally studied
in f.o.m. say that there are reasonable examples of iterated exponential
blowup  - which certainly takes us from the reasonable to the far worse than
totally unreasonable (for mathematical practice).

10. However, this setup - with cuts versus not with cuts - in the standard
f.o.m. systems does not seem to be sufficiently relevant to mathematical
practice - at least prima facie.

11. Let me be more specific. I do not know of a single interesting theorem
of mathematics that is proved without extensive use of abbreviation power.

12. So if you start with a theory T with the usual very spartan primitives
common in f.o.m., and you wish to prove theorem A, which lives in the
language of T, you have a problem right away. We can expect all existing
mathematical proofs of A to be riddled with abbreviations that go well
beyond the language of T. Furthermore most commonly, even to *state* A, we
require in practice that we immediately expand the language of T. This
compounds the problem of seriously talking about cut free proofs in T.

13. How to resurrect what Tennant is trying to do in light of 10-12? Of
course, we can start by pointing out that we can eliminate the use of these
abbreviations. One cost is immediate: nobody can understand the proofs, and
they certainly will get substantially longer, and unintelligible to humans.

14. I'm not sure that the cut/cut free dichotomy can be reasonably
reintroduced in a way truly relevant to mathematical practice. Perhaps
theoretically it can, but perhaps then only in a rather unsatisfactory way
for the discussion of mathematical practice.

15. Of course, the situation with regard to 1-3 is easier (for me) to
grapple with. 

Harvey Friedman