[FOM] 614: Adventures in Formalization 1

[Jay Sulzberger]

On Mon, 14 Sep 2015, Harvey Friedman <hmflogic at gmail.com> wrote:

> 1. General Remarks about Theorem Proving.
> 2. Theorem Statements.
> 3. Universal Gold Standards.
> 3a. Free Variable Formulations.
> 3b. Abbreviation Power.
> 4. Verifying Translations.
> 5. Verifying Proof Files.

Harvey, your program here is close to the Homotopy Type Theory
Program.  Here is a popular article on the conversion of
Vladimir Voevodsky to the Beautiful Proofs Program:

http://blogs.scientificamerican.com/guest-blog/voevodskye28099s-mathematical-revolution/

Though I have not the article before me now, Voevodsky has
written that, in doing mathematics, we will soon be able to avoid
(certain kinds of) drudgery due to more powerful "computerized
mathematics helpers" coming online.

oo--JS.


>
> 1. GENERAL REMARKS ABOUT THEOREM PROVING.
>
> The development of absolutely rigorous mathematical proofs, or Theorem
> Proving, or Proof Assistants, and so forth, is a highly active and
> highly impressive field at the interface between logic and computer
> science. Yet there are a number of missed opportunities and challenges
> that are already apparent. In this series within my numbered postings,
> I hope to seize on some of these missed opportunities, which, in some
> cases, come out of criticism of the way things are (being) done (now).
>
> Before I begin, I want to highly recommend
>
> http://www.cs.ru.nl/~freek/comparison/comparison.pdf
> http://www.cs.ru.nl/~freek/100/
>
> This gives you an idea and feel for just how impressive and highly
> developed this field is. Probably most mathematicians have some deep
> down to earth belief that serious mathematics is not really capable of
> being formalized with a fixed set of axioms and rules. Many of these
> people do not really properly internalize ZFC or even ZC or PA. And
> many that do internalize, nevertheless feel that serious mathematics
> is just too involved for there to be any construction of absolutely
> rigorous proofs.
>
> The two references above show just how wrong the typical skeptical
> mathematician has been.
>
> There is another group of doubters who have a more nuanced position.
> They acknowledge that this is being done, and probably that it can be
> done for even deeper mathematical theorems. However, they doubt the
> interest and/or importance of doing this.
>
> These more nuanced doubters are also wrong but in a more subtle way.
> First of all, the mere fact that traditional mathematicians have
> doubted that it can be done at all for serious mathematics is itself a
> reason to accomplish this as a kind of proof of concept for
> foundations of mathematics. Can absolute rigor actually have an actual
> physical existence? Secondly, and this spills over into the category
> of missed opportunities, this provides a tremendous body of data as to
> the actual structure of actual mathematical proofs - ok, or at least
> those actual mathematical proofs that come out of the process. I would
> be shocked if significant and highly surprising features of actual
> mathematical proofs didn't emerge this Century from this work.
> Thirdly, the actual construction of absolutely rigorous proofs
> requires, on a practical level, or will require as it becomes more
> powerful, an extremely interesting array of new decision procedures
> applying to all sorts of interesting everyday mathematical
> environments. Fourthly, there is a major need for the verification of
> hardware and software systems, and these require that mathematical
> statements be proved with absolute rigor. So Proof Assistants will
> become a vital tool as formal verification of hardware/software starts
> really taking off this Century.
>
> So now I am now temporarily finished with being so positive.
>
> Now for the negative. The Theorem Proving infrastructure is, as far as
> I can tell, not close to ABSOLUTE INFALLIBILITY. Or at least not
> nearly as close to it as we can make it. And making it much closer is
> a missed opportunity that is going to be very interesting,
> philosophically, foundationally, practically, and theoretically, and
> even emotionally.
>
> Below I want to take up the ingredients or some of the ingredients
> needed to move to ABSOLUTE INFALLIBILITY. Now people think that this
> is not achievable, and they have a good case for that. So we can speak
> of moving closer to ABSOLUTE INFALLIBILITY. Far closer than we are
> now.
>
> 2. THEOREM STATEMENTS.
>
> Take a look at the statements of theorems in
> http://www.cs.ru.nl/~freek/100/ They are all unconscionably ugly to
> read and digest for a typical person outside the Theorem Proving
> community. In the Theorem Proving community, they are probably looked
> at as breathtaking works of art.
>
> Now this is something that is a missed opportunity and CAN DEFINITELY
> BE LARGELY FIXED. Is it worth fixing? ABSOLUTELY, but probably no one
> in the Theorem Proving community thinks it is worth their time to fix
> it, and should have a low priority. Conventional wisdom is often very
> wrong.
>
> Part of the reason it should be of a very high priority is that it
> spills over into another NASTY issue.
>
> IN WHAT SENSE are we constructing absolutely rigorous proofs of
> mathematical theorems WHEN there is an issue constantly surfacing
> about whether or not the ACTUAL STATEMENT of the theorems to be proved
> is a CORRECT STATEMENT of the theorems to be proved??? The phrase "bug
> in the statement of the theorem" actually has been known to be heard
> (smile).
>
> It doesn't help matters if nobody (outside the Theorem Prover
> community) can, or can even want to, read the actual statements.
>
> REST ASSURED, this can be largely fixed. I started up an effort along
> these lines, furthered by others, and I think now things have gone
> somewhat further, but I don't know the latest:
>
> (with S. Kieffer, J. Avigad), A language for mathematical knowledge
> management, in: Computer Reconstruction of the Body of Mathematics,
> ed. A. Grabowski, A. Naumowicz, Studies in Logic, Grammar and
> Rhetoric, p. 51-66, 2009.
>
> In this series of postings on Formalization, I will be actually
> constructing some mathematical proofs by hand in a nonexistent dream
> system, where everything is EXTREMELY PLEASANT to read, and so I will
> be presenting FRIENDLY  LANGUAGES.
>
> 3. UNIVERSAL GOLD STANDARDS.
>
> So what axioms/rules do we want our proofs to live in? We must make a
> distinction here of the utmost importance.
>
> a. The axioms/rules used interactively between the human and the Proof
> Assistant.
> b. The ultimate Gold Standard axioms/rules for the ultimate INFALLIBILITY STAMP.
>
> Everybody is free to choose their a) according to taste, judgement,
> and prejudice. But there must be a meeting of minds as to some b).
>
> THIS IS NOT DRACONIAN. Rebel groups can be easily accommodated. Yes,
> we need the rebels to conform to our b). I.e., to export for checking
> that we have a file for b). IN EXCHANGE, we can graciously offer
> resources to go the other way around, so that the rebels can pretend
> to be in charge.
>
> So the issue is really b).
>
> I envision a large system and various important weaker subsystems.
> Since to much math can be done in systems much weaker than ZFC, this
> should be reflected in the choice of Gold Standards. There should be a
> few major Gold Standards ranging from Finite Set Theory to full blown
> ZFC.
>
> To simplify the discussion, I will only be talking about a Gold
> Standard which is a ZFC variant.
>
> What should the criteria be for choosing the Gold Standard for
> mathematical proofs?
>
> i. It has to serve as a Gold Standard in the following sense. Provers
> are required to submit files for Central Authority certification, and
> what is being certified is that the file constitutes an absolutely
> correct proof in the Gold Standard system - generally together with
> other helpful data. The other helpful data is supplied in order to
> make the program that verifies that it is indeed a proof in the Gold
> Standard easier and simpler to write, and easier and simpler to
> execute, and easier and simpler to verify that this writing and
> execute is infallible, and so forth.
>
> ii. It has to be set up so as to maximize its intrinsic infallibility.
> The usual way of presenting ZFC has a number of issues. One is that it
> is almost never done. The predicate calculus part is notoriously
> difficult to get just right, with the free/bound variable clashes and
> the like. Maybe the chances that experts screw up the axiomatization
> of ZFC in the usual form, is something like 2^-100, which is far too
> high an error rate.
>
> iii. There has to, or should be some philosophy done as to why and
> what it means to say that ZFC and/or fragments are infallible.
>
> Each of i,ii,iii are subjects onto themselves, with plenty of missed
> opportunities.
>
> 3a. FREE VARIABLE FORMULATIONS.
>
> With regard to i. Much more reliable in my mind than the usual ZFC
> axioms as presented, is the FREE VARIABLE formulation of ZFC. There is
> epsilon, equality, and function symbols associated with
> extensionality, pairing, union, power set, infinity, foundation,
> choice. With Replacement, there is first a handful of general purpose
> Skolem functions.
>
> There seems to be a missing subject of GENERAL PURPOSE SKOLEM
> FUNCTIONS. They are small in number, have very simple axioms
> indicating what they do, and they provably generate Skolem functions
> for all first order formulas (even those that mention the Skolem
> functions themselves), via composition only. And THEN Replacement is
> still a scheme, involving all terms.
>
> I prefer not to use NBG and adhere to ZFC for this purpose - in fact
> free variable ZFC for this purpose. I don't think enough is to be
> gained by going to variables over classes, to be worth its
> repercussions for what I am trying to do here.
>
> I want to EMPHASIZE that this basement is INVISIBLE to any human
> involved in Theorem Proving.
>
> Now let's focus on FVZFC = free variable ZFC, Free variable logic is
> obviously much more basic than full logic. Of course, the key
> ingredient is TERM SUBSTITUTION.
>
> TERM SUBSTITUTION is the DNA of mathematical thought. Everything
> arises from it (along with =).
>
> 3b. ABBREVIATION POWER.
>
> Now requiring all Certified Installations to conform to FVZFC is not
> going to work. The problem is that we desperately need to use
> ABBREVIATION POWER in order to avoid blowups. So we really need to use
> FVAPZFC = free variable abbreviation power ZFC. We are allowed to
> define, or nondeterministically specify, new function symbols by free
> variable statements.
>
> CAUTION. I am not saying that we want humans to be interacting with
> their computer in a free variable way. I am simply talking about what
> is to be going on in the basement of the Central Authority
> Headquarters.
>
> 4. VERIFYING TRANSLATIONS.
>
> At this point, we need the first of MANY translation modules. Here is
> a list of ones, some of which are crucially needed, but others are a
> very good idea to have anyway. And maybe will turn out to be crucial.
>
> i. Going from FVAPZFC to FVZFC.
> 2. Going from FVZFC to ZFC.
> 3. Going from ZFC to FVAPZFC.
>
> We should have a general format for and theory of SYSTEM TRANSLATION.
> We need to address the issue of INFALLIBILITY here, and the
> INFALLIBILITY of code used to implement these translations. We need to
> push this little corner of things, comparatively unproblematic, down
> to as close as we can to ABSOLUTE INFALLIBILITY. More generally,
> elemental, in your face, finite string manipulation theory. We
> probably need to address also the hardware implementation of this,
> including what we do about cosmic rays?
>
> SAMPLE ISSUE: how do we implement term substitution (the DNA), and
> what kind of INFALLIBILITY can we achieve in doing so?
>
> 5. VERIFYING PROOF FILES.
>
> We now come to the interaction between the Certified Installation
> Theorem Provers and the Central Authority.
>
> The Provers are to submit
>
> a. The statement of the Theorem.
> b. A file with a proof of the Theorem in FVAPZFC.
> c. Another larger file with an annotated proof of the Theorem in FVAPZFC.
>
> All of these three MUST adhere to the universally accepted GOOD FORM.
>
> The purpose of c) with its annotations, in universally accepted form,
> is to facilitate and improve the INFALLIBILITY of the Central
> Authorities' checking process.
>
> In general, these annotations consist of pointers so that the Central
> Authority checker does not have to do any or much search. Obviously,
> we cannot require annotations that cause significant blowup.
>
> We have now, another little subject. Let's say we want to check that a
> file meets certain criteria like being a proof in FVAPZFC. That is a
> certain kind of specification. What is a best or really good way of
> annotating it so as to greatly simplify the implementation of any
> checker checking that it meets the criteria in question? There seem to
> be two ways to go. One is to put a lot of important and useful
> pointers all over the place. Another is to make copies of certain
> things and put them in strategic positions. We want simpler kinds of
> checkers in order to make it easier to argue that they are INFALLIBLY
> EXECUTED. Remember, this is not just a matter of software, but
> includes hardware infallibility issues as well.
>
> E.g., it is far simpler to check that a file has an even number of
> characters, as, e.g., having no two substrings of length 100 that are
> the same - even though we know a lot about good efficient reliable
> ways of checking for either one.
>
> ************************************************************
> My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
> https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
> This is the 614th in a series of self contained numbered
> postings to FOM covering a wide range of topics in f.o.m. The list of
> previous numbered postings #1-599 can be found at the FOM posting
> http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html
>
> 600: Removing Deep Pathology 1  8/15/15  10:37PM
> 601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
> 602: Removing Deep Pathology 2  8/23/15  6:35PM
> 603: Removing Deep Pathology 3  8/25/15  10:24AM
> 604: Finite Emulation Theory 2  8/26/15  2:54PM
> 605: Integer and Real Functions  8/27/15  1:50PM
> 606: Simple Theory of Types  8/29/15  6:30PM
> 607: Hindman's Theorem  8/30/15  3:58PM
> 608: Integer and Real Functions 2  9/1/15  6:40AM
> 609. Finite Continuation Theory 17  9/315  1:17PM
> 610: Function Continuation Theory 1  9/4/15  3:40PM
> 611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
> 612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
> 613: Optimal Function Theory 1  9/13/15  11:30AM
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>