[FOM] Formal Proofs

[Jay Sulzberger]

On Sat, 25 Oct 2014, Harvey Friedman <hmflogic at gmail.com> wrote:

>
> < ... />
>
> POSITIVES: (for me, there are enough spinoffs of the formal proof
> movement to pique my interest).
>
> 1. CHALLENGE above. Micro proof theory - study of new deeper
> fundamental features of actual mathematical proofs. Actually, this may
> not even have been properly initiated at all.

I think the heart of New Crazy Types^W^W^WHomotopy Type Theory is
exactly the systematic examination of proofs and objects at this
"micro" level.

ad the exercise:  Yes the exercise is a good sample to work on.

> 2. Motivation for the development of and implementation of a truly
> massive and massively interesting set of decision procedures. AND,
> even when one encounters algorithmic undecidability, there are ALWAYS
> associated decision procedures when one goes to large (or even not so
> large) input spaces. Easily enough for 10^6 Ph.D. theses and careers.

Such development is already today the systematic study, at the
level of what was once called "metamathematics", of the varieties
of microscopic proof rules and the study of their interactions.

> 3. Historically, there has been the informal and wrong idea that
> formalization is utterly impossible for state of the art theorems, as
> "mathematical proving is not subject to complete logical analysis".
> Well, maybe that is the case at the creative conceptual level -
> particularly finding proofs and formulating theormes - but we are
> talking here at the level of finished polished rigor. Is it possible
> to actually have files residing on computers that constitute finished
> polished completely rigorous proofs of deep state of the art? The
> answer is yes, but only through the formal proof revolution are we
> able to have this. I regard this as a principal foundational issue
> that has been nearly put to rest. This is a real victory for f.o.m.

Surely no serious student of logic after the publication of the
completeness theorem for the lower order predicate calculus ever
thought that formalization was impossible, in any serious sense.
If one thought this, then the completeness theorem must seem to
lack force.

>
> BUT now I hear rumblings that 3 has not been put to rest from these
> higher homotopy types people. So we come to what I call the UMBRELLA
> issue.
>
> The normal course of events is simply to adhere to the time tested
> Standard Umbrella of ZFC. Put category theory, usual type theories,
> etc., under this Umbrella. After ZFC, immediately create special
> infrastructure, which look like simply careful definitions and basic
> theorems.

Doubtless for most suggested New Crazy Types Foundations one
could do as Paul Levy suggests and make an object within ZFC, or
something close to ZFC ("close" as understood by workers in set
theory) which serves as a HoTT World Object.  But once one has
done this, and assuming that given a New Crazy Types Foundation
proof P of a theorem T, the sentence in ZFC

"Trans^NCT_ZFC(P) has the relation 'is an NCT proof of' Trans^NCT_ZFC(T)."

is provable in ZFC with perhaps some limitation on how much
longer the proof of this sentence in ZFC is than P in NCT, one
still has not done much, as seen from NCT. (Here Trans^NCT_ZFC is
the translation from the NCT World to the ZFC World.)  Why not?
Well, after all, to use a word that V. Voevodsky has recently
used here, we may be happy with ZFC as an etalon of mere rigor,
but the notions of proof and object and theorem in NCT are quite
different from the now received versions as taught and thought
about among students of ZFC.  One has to apply a monstrously
forgetful functor down to the one question

   Is this a correct proof?

from the more important questions such as

   What does this proof really prove?
   How might this proof be varied to get something else?
   How has the organization of our textbooks/databases affected
    what we have done, what can we see?
   Is this proof P really the same proof as the old proof P0?

to think that writing down Trans^NCT_ZFC(P), and proving that it
is sound and complete (and does not cause the transcription to
increase in length too much) for NCT gets one very far.

When I took my first formal course in mathematical logic in the
1960s from Jack Schwartz (he presented his version of forcing, I
assumed he must be a professional logician) I was already a member
of the ZFC tribe.  We had behind us the heroic age of Cantor,
Dedekind, Peano, Hilbert, Goedel, Church, Turing and other Great
Old Ones.  We had won through to an extraordinary origin myth
which, we felt, we had secured by very beautiful theorems:

   There is Syntax, the Set of Sentences with their proper apparatus.
   There is Semantic Values, the Set of Structs with their proper operations.
   And from the Galois connection between Syntax and Semantic Values
    there is Rigor.

And the practice of Mathematical Logic was based on the strict
formal opposition of Syntax and Models.  Of course anyone can see
at once a sentence is a very different thing from a model, or
indeed from an element of a model.  But the victories of the
heroes were so great that we forgot, except when telling the old
stories, that once, this great insight, that Syntax and Models
are only connected by the thin hard elegant rules of
"interpretation of clauses" which give us the Galois connection
between sets of sentences and sets of models was not glaringly
obvious.  If one reads work in Mathematical Logic before Our
Triumph, one sees that the glaring truths we now hold as the
foundation of our work were once either denied, or worse, the
very questions were framed in such a way that our present answers
are not answers to the questions asked.  Many New Crazy Type folk
consciously, because they are well educated, deny that the ZFC
tribe's answers are right, and they make an even stronger attack:
they claim that many of our moves are just not to the point.

I repeat here a formula that I have already at least once posted:
Among New Crazy Type folk, among those who admit that there are
"models" at all, it is required of a model that every element be
a lambda term.  Further all proofs are lambda terms in NCT.  The
difference in the mathematics of ZFC and NCT, even if we have in
hand a good Trans^NCT_ZFC does not disappear.

>
> But, just as some category theorists in the good (bad) old days,
> pushed for overthrowing the Standard Umbrella, basically replacing it
> by a new Umbrella, or overthrowing the whole idea of an Umbrella, we
> have some people pushing for something like this again.

New Crazy Type Theory is, in major part, the research program of
doing the old Categorical Umbrella right.

>
> What happened with the old movement to overthrow the Standard
> Umbrella, is that enough f.o.m. people, philosophers, mathematicians,
> and others, considered the overthrowing of the Standard Umbrella, and
> generally didn't like the idea of No Umbrella much, and started to dig
> in to what it would really entail, foundationally and philosophically,
> to replace the Standard Umbrella. They found that the same issues
> arise with the New Umbrella, only these issues had already been
> properly addressed in the Standard Umbrella, and any way of handling
> them in the New Umbrella either caused new problems, or were imitative
> of the Standard Umbrella. So the movement to replace the Standard
> Umbrella pretty much died (not completely of course). Even MacClane
> starts off his book Categories for the Working Mathematician with "a
> category is a set of objects, together with a set of arrows,
> etcetera". And if you try the category of all categories, etc., you
> wind up with difficulties more or less like trying the set of all
> sets, etc.

These are questions of ZFC.  They have versions in NCT work, but
the two versions are not the same.  Just because Mac Lane uses
such language does not impress those of us who feel the force of
the New Crazy Types Program.  Those few sentences do not convince
us that really, after all, it is all just good old fashioned ZFC
at bottom.  It is not.  The questions are different.  To repeat:
If you apply a forgetful enough functor then many things that are
different will seem to be the same, particularly if one has
forgotten that a functor has been applied.

>
> Now with the radical wing of the higher homotopy type people (by the
> way, I do know some part timers who are NOT radicals), there is the
> idea that we need to overthrow the Standard Umbrella and replace it
> with either No Umbrella, or a New Umbrella. The claim seems to be that
> there are better reasons for overthrowing the Standard Umbrella than
> there were before, with the radical category theorists.
>
> Well, just as in the case of the radical category theorists, these new
> radicals are going to have to carefully, and painstakingly, make their
> case for the overthrow of the Standard Umbrella to a wide range of
> foundationalists, philosophers, mathematicians, even computer
> scientists. They are going to have to do two things:
>
> A. Give a completely transparent account of a generally understandable
> situation where the Standard Umbrella allegedly really breaks down. It
> is easy to point to some math that few people have studied and simply
> say "the Standard Umbrella is inadequate" and just leave it at that.
> That is completely unconvincing. See the recent FOM postings of Freek
> and Levy on this point. Radicals - please comment on Freek and Levy on
> this point.I

No.  We are asking different questions.

>
> I think that the radicals want to make a claim that "something really
> radical in connection with equality must be done which simply cannot
> be handled under the Standard Umbrella". But there are many convenient
> ways of handling situations like this. It's called extra information.
> A toy example is f:A into B. Well, the usual way of treating functions
> is that f:A into B is equaled to f:A into C if the range is contained
> in B and in C. HOWEVER, as you know, you can talk of functions as
> pairs (graph(f),B), where you pack the codomain into the function. So
> you can introduce special variables for "packed functions" F, and use
> the notation dom(F) and codom(F). Everything remains beautifully
> simple, and this is all within the Standard Umbrella, admittedly based
> on ZFC WITH SUGAR. Now this is a trivial example of what is second
> nature to any good f.o.m. person. Before overthrowing the Standard
> Umbrella, we are going to have to know that highly skilled f.o.m.
> people have digested the challenge, presented in generally
> understandable terms, and become convinced that such devices -
> particularly information packaging with accompanying sugar - don't
> work perfectly fine. Radicals who are not steeped in f.o.m. simply
> cannot be prima facie trusted.

This is a good point, which I am, after suppressing some
important dimensions, in agreement with.  But I hope to answer
your claim here in another post.  I will disagree once we have
looked at the suppressed, that is, forgotten, dimensions.

>
> Here I am acknowledging claims that "yes, it can be done under the
> Standard Umbrella, but it is completely impractical". However, it is
> fully practical in any situation foundationalists, philosophers,
> almost all mathematicians, are familiar with at this point.

Getting a good Trans^NCT_ZFC is very important.  Indeed we will
get whole categories of such.  Work has been done and is being
done on this.

ad Blakers-Massey:

1. Indeed one can do a translation.

2. Because NCT is so different from ZFC, any translation, without
much further work of explication beyond checking soundness and
completeness, will be required before one dare say, "Yes, this
object here in ZFC really is a good version of NCT
Blakers-Massey.".

3. Even after above, a real logical problem remains: If we have
two different logics, then is what senses can an object in one be
said to be the same as an object in the other?

>
> B. After A - which of course may (will) never happen - the radicals
> have to construct a New Umbrella. Here philosophical coherence,
> simplicity, general usability, and general transparency are absolute
> requirements. The Standard Umbrella spectacularly meets these
> requirements. Some even slightly opaque kind of intensional equality
> is not going to work for this. Well, if that becomes the essential
> point, then there are serious variants of the Standard Umbrella where
> extensionality is dropped. However, my instinct is that I don't like
> it, and information packing is highly preferable, with accompanied
> sugar.
>
> Harvey Friedman

ad B: I think some of the New Crazy Types folks' propaganda is
inaccurate.  Because I am a partisan in favor of New Crazy Types
I wish our propaganda to be good, and so I want to avoid
inaccurate claims.

oo--JS.