FOM: Mathematics, the world of experience, and the concept of proof

[Vaughan R. Pratt]

>LFrom: Jon Barwise <barwise at phil.indiana.edu>
>(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.

Quite so, although it is a shame that the third person in a row
corresponds to 2 in the ordinal model of a row.  :)

>So too, 2/3 is a certain ratio, or fraction, say the fraction of my three
>fingers I have just put down.  It is usually modeled in ZFC by a certain
>equivalence class of ordered pairs of integers.  These may be good or poor
>models but they certainly are not identities.

Absolutely.  An example I was just harping on comes from my
sets-as-ordinals story (which I promise to shut up about after this :).
The set {6} is modeled by the ordinal 1 in some contexts, and in others
by the function from \omega (or whatever ordinal type your {6} has) to
2 that is 0 except at 6.  Likewise the number 6 might belong to the
monoid of natural numbers, the group of integers, the field of
rationals, reals, or complex numbers, etc., and is represented by
different sets in these different contexts, in the ZFC world or most
any other foundations, despite the fact that 6+6=12 in all these
contexts.

Not only need one's model of something not be the something itself, if
you have to change the model in order to suit the properties being
modeled then it *cannot* be the thing itself.

So I agree 100% with you up to this point.  Now...

>What are proofs, anyway?  ...
>Proofs are surely part of the world of (mathematical) experience,
>mathematicians proving things to convince themselves and others of the
>truth of various mathematical propositions.
 ^^^^^				^^^^^^^^^^

This is something I promise *not* to shut up about because it is
uppermost in my mind these days, indeed the most important thing for
me.  I'm sorry if I'm continuing to be the odd man out in these things
but I strongly disagree with this viewpoint.  (Here I'm going to take
your "surely" at its face value, as opposed to something you really
mean to subsequently retract, since your message didn't in fact do so.)

I appreciate that true propositions are generally, I guess almost
universally, regarded as the end and robust constructions merely the
means.  But I don't think this is at all right.  I am for equal rights
in this matter and believe that true propositions and robust (widely
applicable) constructions should be treated as equal partners with
neither having priority over the other as the ultimate end.

I think the reason propositions currently dominate is that mathematics
and logic have evolved together to make them the end.  The results are
that papers are theorem-oriented, mathematical careers are judged by
the number of quality of one's theorems, and logic, in making truth the
master and construction its servant, reinforces the dominance of truth
by making it the only criterion by which soundness is judged, and by
equipping it with a beautiful and finely honed calculus.  Robustness as
wide applicability is a mere side show which logic has evolved no
formal basis for and which tends to be viewed no more charitably than
the warm feeling one gets when contemplating a slick proof of the
(however important or irrelevant) theorem to be proved.

Jon, in modeling mathematics in terms of truth and proposition, I claim
you are committing the very use-mention confusion you were complaining
about, albeit at a very fundamental level (but this *is* fom, right?).
The reason you believe mathematics communicates truth, expressed in
propositions, is because you model mathematics that way.  This is an
accident of the history of metamathematics, mathematics could equally
well and (I claim) equally successfully have been modeled in terms of
the communication of constructions.

Let me point out that propositional logic and first order logic deal
with mathematics in about the same sense that automata theory deals
with computation and particle physics with the universe.  You don't get
much bang for your buck, just what passes as the bottom layer or two in
a vastly richer fabric.

By the same token, a logic of constructions, at a comparably
fundamental level, need not promise to do very much.  As a calculus,
what it needs first of all for approximate parity with first order
logic is to have a similarly sized language and provably complete
system of reasoning, about concepts that are as central and widely used
for constructions, *throughout mathematics*, as are the concepts that
first order logic has nominated as being universally used in
mathematics viewed propositionally.

The rest of your message expressed uneasiness with the status quo.  But
at no point did you question your "surely", which I therefore took to
be an invariant of whatever transformation of mathematics you hope will
fix what you say is broken.

What is broken in my view is the basic premise that mathematics
traffics in propositions, with constructions as a mere currency.  I
claim that mathematics traffics equally in propositions and
constructions.

Unfortunately this is a somewhat lame claim, since what is missing to
back this up is a correspondingly rich theory of constructions that
foundationalists feel comfortable putting in their textbooks side by
side with the gleaming propositional status quo.  Nevertheless I
strongly believe in it, and very much want to see this playing field
leveled a bit better.

I care about this much more than whether a set is an ordinal or a duck.

Vaughan