FOM: ReplyToBarwise/Pratt/Remmel

[Harvey Friedman]

Barwise writes

>This begins to get at what to me is a fascinating question in the FOM:
	>How does mathematics connect to the everyday world
	>of direct experience?

>(Application to Harvey's question about the number 3: Human languages allow
>us to talk both about 3 people but also about the third person in a row.
>There is no obvious reason to suppose that either the cardinal or the
>ordinal notion is more basic than the other.  They are both very directly
>grounded in our experience of the world.  They are related in various ways.
>But neither needs to be lower than the other in the "more-basic-than"
>ordering.)

This is a great foundational issue, which is related to other fundamental
issues such as: why or is or how is mathematics useful? I.e., Foundations
of Applied Mathematics. I suspect that when you read my discussion of
notions of number and curves, you thought that I was hung up on rigid ideas
that all concepts must be linearly ordered in terms of how fundamental they
are. That's not what I meant at all. Firstly, of course, any such ordering
is at best a partial ordering. And sometimes it is useful and interesting
to place one concept as more fundamental than another, and sometimes it is
not. In any case, there are some related interesting linear orderings that
should be considered:

For instance, in a comprehensive reworking of the Foundations of
Mathematics, and also Foundational Studies in general, there is still the
choice of order of presentation of ideas, so as to make the treatment as
comprehensible and informative as possible. Although hypertext in principle
should make linearity less of an issue, people still have to go through,
and listen to lectures on material in a linear fashion; and hypertext just
isn't quite the cure-all we all looked forward to.

This is a real issue for me since I have long thought that I would have a
crack at a comprehensive reworking not only of the Foundations of
Mathematics, but classical Mathematics itself -  with an eye to new
presentations of material that would greatly facilitate the educational
process. And also how the various subjects fit together under a unified
exposition - mathematics, statistics, mechanics, computer science,
linguistics, law, etcetera.

Some linear choice of presentation of ideas is involved in any exposition
of any subject. It's best to make this as sensible and friendly as
possible. And as compatible with reality and human understanding as
possible.

Also there is conceptual development of children and others. There is no
doubt that in the emerging connections that children make with the world,
there are linear aspects of the order in which the concepts get
assimilated. This should not be ignored.


Barwise writes

>Martin Davis once used "Hilbert's Thesis" to name the claim that the
>informal concept of proof is adequately modeled by the first-order model of
>proof (though he did not put it quite this way).  This thesis is analogous
>in status to Church's Thesis.  It is not a mathematical conjecture, subject
>to proof, but it is surely a foundational question, one subject to rational
>inquiry.  I don't recall whether Davis subscribed to Hilbert's thesis or
>not.  My own belief is that the thesis is false.  Mathematical reasoning is
>often just not first-order.

I have had the utmost difficulty in understanding this kind of point for at
least thirty years, despite often trying to. Of course mathematics is
entirely first order, and of course mathematics is entirely not first
order. This seems to me to be a false dichotomy - unless I am missing
something fundamental here. If I am missing something fundamental here,
then I couldn't do any better than learn what I am missing from Jon Barwise.

1. Mathematics is entirely first order.
	When mathematicians reason, there is a purely logical part which is
built on top of fundamental assumptions about fundamental mathematical
concepts and constructions. There was a time when there were literally
dozens of seemingly fundamental mathematical concepts and constructions,
and there was no "rules of the game" for when the injection of yet another
concept of construction is or is not legitimate. E.g., naturals, integers,
rationals, reals, complexes, quaternions, fundtions, series, sequences, sum
of series, group, ring, field, Euclidean space, projective space,
infinitesmials, sets, functions, matrices, infinity, line, plane, surface,
tangent, etcetera. There is no doubt that this situation was rightly
considered rather unsatisfactory.
	So the present way of setting this up, which goes to the other tidy
extreme, is to just have sets and membership (and equality). Despite the
undeniable fact that this has its unsatisfactory aspects, it is quite
satisfactory, simple, and neat, and quite adequate for a great many
purposes. Furthermore, nothing comparable has been proposed and developed
that does the same things so well.
	On this account, there really still appears to be a legitimate
dichotomy between the purely logical part of mathematical reasoning, and
the set theoretic axioms. I would be the first to admit, however, that
there are real conceptual issues that can be raised here, but I feel
confident in the outcome. That the best way to look at this will still be
with this dichotomy in tact.
	Now for a concession: the ordinary setup of first order predicate
calculus with one binary relation symbol epsilon (and equality) is totally
inadequate to actually carry out mathematics. First of all, without the
apparatus for introducing abbreviations, such a system is entirely useless
for the actual formalization of mathematics. But the difficulties go
deeper. There is an elaborate system of conventions and notation that
mathematicians use, in order to facilitate the understanding of what is
written, and to support the writing of what one has in mind.


	Randy Dougherty and I have been collaborating in a systematic study
of the notation of mathematics sufficient to support the user friendly
presentation of mathematics. The first phase of the project is to handle
the presentation of mathematical information. This is a realistically
doable project, which has really gotten off the ground. The stated goal,
which is not too far off, is to take some basic elementary texts and write
the mathematical substance of what is asserted in such a way that it is
totally formal (in the sense of a completely precise syntax and semantics),
yet totally user friendly and readable (the mathematical information - not
the proofs). The whole idea is to create an elaborate form of first order
predicate calculus replete with all kinds of additional constructs and
syntactic features that support readability and writability.
	One may take the position that what we have is no longer first
order. I think that the extent to which it is not first order is misleading
and uninteresting. There is a perfectly reasonable Tarkian semantics -
although much more complicated - and a Godel type completeness theorem.

See:   Formalization of Mathematics, somewhere in
www.math.ohio-state.edu/~friedman/
available in postscript.

2. Mathematics is entirely not first order.
	After all, one must use concepts like set, which are not part of
first order predicate calculus. And obviously the valid sentences is not
recursively enumerable.

In summary, I think that the first order/not first order dichotomy is a
false and misleading dichotomy. The real dichotomy to me is: is there a
precise syntax and a precise finite set of axioms and rules of inference
that are used to model mathematical reasoning? Certainly ZFC meets these
criteria. Take so called second order logic. I have never understood what
is exactly meant. There is a semantics, which is closely allied to set
theory. And there are axioms and rules of inference. But the axioms and
rules of inference constitute just a first order system with, say, two
sorts. So what? Set theory is also a first order system - with one sort.
When one gets down to brass tacks, one always wishes to give those finitary
axioms and rules of inference.

Maybe the point some people wish to make is that "second order logic is
open ended and mathematicians continually create more principles that
cannot be codified in any fixed set of axioms and rules of inference; after
all, the usual semantics is far from being recursively enumerable, and has
no complete set of axioms and rules."

But this is simply not true (first part). Mathematicians do not create
anything of the sort - the usual ZFC framework is still overkill for the
working mathematician. (Of course, as you know, I'm beginning to understand
what kind of valuable information can be obtained only by going beyond this
framework, but that is completely irrelevant to this discussion).

Or maybe people mean this: one naturally wishes to reason with, say, "there
are at least five objects such that P holds," or "there are infinitely many
objects such that P holds," and insist that this is logic, but not first
order logic. But this is also subject to exact axioms and rules of
inference, and also it is conceptually close enough to making moves like:
"{x: P(x)} has cardinality 5" or "{x" P(x)} is infinite" that one might as
well think of this as embedded in the usual set theoretic framework with
its first order theories such as ZFC.

Enought of this meandering. Jon - it's your turn to tell us more about what
you have in mind, rather than for me to go all over the map guessing and
fighting what may well be straw men. I wouldn't be surprised if I get
interested in what you have to say, and wind up agreeing with you
completely!!!

Barwise writes

>It sometimes get in a mood where I find it a bit shocking that we have as
>little to say about mathematical proofs as we do.  This is not to belittle
>the work in proof theory, which has flourished as a part of mathematics in
>recent years.  Rather, what I can find shocking in this mood is that we
>have not done more with the task of trying to understand the relation of
>the informal concept of proof to various formal models of proof, and with
>it the task of trying to improve the our formal accounts to better model
>the informal concept used in mathematics.  Perhaps the reason we have not
>done more is that it is not clear to what extent the task is a logical one,
>rather than philosophical, cognitive, sociological, or heaven knows what
>else.  But still I hope to see a day when there is what I would consider a
>rich "theory of proofs".  The theory may not be part of mathematics, or
>even of the FOM, but it should greatly enrich the FOM and our discussions
>of mathematical activity.

You don't have a monopoly on this shock. I have been saying this for years.
I'm more shocked than you are, I think. That we should examine carefully
actual mathematical proofs (and other kinds of proofs as well). But I got
stuck somewhat on the isssue of mathematical notation and the presentation
of mathematical claims. This has been the driving force behind my work with
Randy Dougherty on the formalization of mathematics. I gave a talk at SRI
and UCSD this year about it. People doing automated proof checkers and the
like, for verification of hardware and software, have their own ways of
doing some of these things. But what Randy and I do is stronger with regard
to how mathematicians actually think about and write claims.

Even a very superficial aspect of proofs has not really been all that
thoroughly worked on -- their size. By the way, cut free proofs, or normal
proofs, aren't what mathematicians do. Everything pretty much is not cut
free or normal. Lower bounds for cut elimination or normalization have been
known, at least by me, since the late sixties - but nobody knows who should
get credit for this work. The lower and upper bounds approximately match -
they are iterated exponential.

Now here is something I have been interested in and did some work on: give
very natural, interesting, and varied examples where there are short proofs
in predicate caluclus, yet all cut free proofs are absurdly long. In
general, show that, throughout the entire logical landscape, that when one
moves to higher, less elementary systems, one dramatically shortens proofs.
Now Godel did this in theory in a famous paper. But do this in the most
natural of examples, preferably with regard to theorems that are celebrated
within classical mathematics.

Also there is the following point, which is best thought of in connection
with this joint work of Dougherty on mathematical notation. Namely, there
are only a few formulas that ever occur in mathematics (or mathematical
claims). This is true because as soon as things get a bit complicated to
state, mathematicians introduce abbreviations to make them simple again. So
there are only a handful of logical forms. They should be enumerated and
classified, and statistics should be run on them with regard to their
frequency of occurrence. Question with psychological, and sociological
overtones: when do formulas get too complicated, so that mathematicians
simplify them by introducing new abbreviations? We all know that this is a
crucially interesting matter, since otherwise mathematicians could not
actually be done. Maybe there is a complexity theorem here somewhere - and
maybe this is related to the fact that, also, humans generally can only
efficietnly process relatively short sentences and phrases.


Recall the e-mail from Pratt:

From: "Vaughan R. Pratt" <pratt at cs.stanford.edu>
To: fom at math.psu.edu
Subject: Re: FOM: Golden Age/FOM plans
Date: Thu, 23 Oct 1997 17:01:18 -0700

I don't pretend to really understand Pratt's point of view, which is
obviously a sophisticated form of the commonplace point of view that
mathematical objects do not (or should not) have an existence independently
of how they fit into larger mathematical strucutures. As I have said
before, I find this point of view extremely interesting, but I have never
been able to analyze it sufficiently productively so as to develop an
alternative foundation for mathematics, which is comparably smooth and
systematic, to the usual Foundations for Mathematics. I have managed to say
at least a little something about some aspects of this viewpoint, within
the context of the usual Foundations; e.g., in an article "On the
naturalness of definable operations," Houston J. Math., vol. 5, No. 3,
1979, pp. 325-330. By the way, this paper can be viewed as a paper in basic
model theory of the kind that is not readily classifiable and doesn't fit
into the usual viewpoint of current practitioners of model theory.

Despite my ignorance, I do have something to say that may be relevant. I
have been proving results that show an inexorable and unbreakable link
between certain finitary/discrete mathematical problems (which are being
more and more accepted as natural by working mathematicians) and these
large cardinals that Vaughn wants  to banish. Namely (to oversimplify a
little bit), these mathematical problems are demonstrably equivalent to the
consistency of ZFC + "there exists these large cardinals." Vaughan, you may
wish to banish these large cardinals, but what do you make of that
equivalence? If you accept these mathematical problems into your discourse
- and they are very normal looking - you are stuck with the large
cardinals, in a precise and powerful sense of the word "stuck."


Remmel writes

>I forgot now who first brought up the idea of generally
>acceptable proof methods, but there is still considerable
>controversy about what is an acceptable proof as is witnessed by
>the controversy about computer aided proofs that has occured recently in
>the Notices.  There are some mathematicians who are very uncomfortable
>with proofs that rely on verification of computations or case
>analysis which are done by the computer.  However such proofs
>are clearly going to become much more common as the sybolic
>computation packages such as Maple, Mathematica, etc
>are becoming a research tool used by an increasing number of
>mathematicians in a variety of fields.  Then there is
>the idea of proof which can be verified by checking a small
>number of random bits which has emerged from the work on
>interactive proof checkers in computer science.  Do we
>want to accept proofs which have a greater 1 - 1\10^20 chance
>of being true?.  Is that some how different than the proof
>for the classification of finite groups which because of its
>length and complication is extremely difficult to understand
>and check?

I have done some initial work on the problem of giving an adequate
formalization of these augmented concepts of proof, and asking traditional
questions from the Foundations of Mathematics. E.g., what is the proper
analogue of Godel's 2nd incompleteness theorem, etcetera? It's a bit
tricky, since one must get into matters such as the probability that one of
these formal systems based on coin flips is or is not consistent (in
various senses). There is plenty of opportunity for an interesting
combination of comnplexity theory, proof theory, Godel's phenomena,
foundations, etcetera here, related to these new kinds of proofs that are
emerging.

How sure are we that, e.g., Wiles proof is correct? Ron Graham has thought
about this, and gave me an opinion that it would be many - but not too many
- years before the probability really gets high, since it involves so much
earlier material, some of which is not yet published. It might be
interesting to get a feel for the probabilities involved - particularly
after a proof has been gone over in state of the art Seminars in leading
centers that do the relevant kind of work. Perhaps somebody can gather and
analyze some data.

There is also the delicious matter of trying to formalize arguments that
purport to convince us that computer programs are correct. Or that roundoff
procedures don't skew data, etcetera. I think there should be interesting
deep rigorous underpinnings of these things. I remember Manuel Blum telling
me he worked on these issues.