[FOM] Solution (?) to Mathematical Certainty Problem
Steve Newberry
stevnewb at ix.netcom.com
Sat Jun 21 16:16:42 EDT 2003
Harvey,
I think you have made a really good suggestion here. I would like to
nominate the
instruction set for the DEC PDP-11 as being ideally qualified for the task
of machine
language [actually, assembly-language] programming of the core proof
checker. There
are probably more people alive with PDP-11 assembly language experience
than all the
others combined, and the PDP-11 instruction set was a uniquely
well-designed machine,
both for programming and for readability. The fact that the 11 is no
longer in
production can be regarded as an advantage, for the language is now frozen;
and there
already are a number of more modern processors which have PDP-11
emulators, so execution
does not require actually getting the original DEC processor boards.
Cordially,
Steve
At 01:04 AM 6/21/2003 -0400, you wrote:
>This is a followup to my posting 2:32AM 6/20/03.
>
>Here is a proposal for attaining mathematical certainty with computer
>assistance.
>
>1. THE BEGINNING - THE MASTER FORMAL SYSTEM T.
>
>I start like everyone else in specifying the formal system in which proofs
>are required to exist.
>
>Normally, T will be taken to be some practical version of ZFC, with
>flexible abbreviation power, and also like what I discussed in 7:03PM 6/20/03.
>
>We will assume that this master formal system is specified human to human,
>of course in a very careful and meticulous way.
>
>As we shall see from my proposal, it is entirely appropriate to assume
>that this system T is a Hilbert style proof system, which is much easier
>to deal with from the human level in terms of specifying what proofs are.
>Of course, Hilbert style systems are a nightmare in terms of humans
>actually reading or casting proofs directly in them. But as we shall see
>in my proposal, humans are not going to be reading or casting proofs in T.
>
>So the first step is for T to be cast in simple and clear enough terms, so
>that humans are all convinced that if there happens to be a proof in T of
>a sentence A, then this confers the desired certainty on (the intended
>interpretation of) A.
>
>Of course, it is vital that the language of T be sufficiently powerful
>that a mathematician can identify sentences in the language of T that
>correspond exactly to the Theorems being verified. This is not a problem
>if we start with a really good version of ZFC. This does require a
>discussion of work I have been involved with, but have not discussed the
>details of, on the FOM. Work concerning appropriate forms of ZFC for the
>development of mathematics, on the language, not the proof, side.
>
>One aspect of my posting 11:49PM 6/17/03 "Theory of Actual Proofs" is
>vitally important here. Statements to be verified generally have a line of
>definitions that need to be made in advance of the statement. And these
>definitions must be in proper linkage with all of the previous definitions
>made. So as we use the system T, we create a definitional chain, as well
>as a statement chain. For some purposes, there is no point in
>distinguishing between definitions and theorems, as they are all to be
>verified statements (the definitions, in proper form, need no verification).
>
>The part of T other than proofs, is required to be extremely humanly
>friendly, since it is going to be part of the official record, to be read
>by mathematicians. This requires serious care, and needs to be discussed
>further, as I said above.
>
>However, this issue is reasonably under control. I.e., this part without
>proofs. We do not require any kind of perfection in this respect. I know
>of reasonable proposals, which do require a little flexibility on the part
>of users, but are an improvement over anything that I have seen.
>
>2. EXTREMELY ANNOTATED PROOFS IN T.
>
>The overall design of this proposed system is as follows.
>
>i. Humans interact with various existing systems like Mizar and Isabelle
>and others, New ones will be developed once our system is put into place.
>I don't care what they look like, but the purpose of these auxiliary
>systems is to use whatever tools, to
>
>create files purporting to be formal proofs in T appended with what I call
>an "extreme annotation".
>
>Because of this "extreme annotation", I don't care what kind of buggy
>garbage may sometimes be produced by such human/machine interactive
>systems. I don't care if they happen to be buggy, but of course that may,
>in a practical sense, waste a lot of time of their users trying to comply
>with our perfect standards.
>
>ii. These purported formal proofs in T must start with a statement of what
>is being proved, preceded by an appropriate definitional lead in. This is
>in full accordance with the dynamic nature of the setup of T. Of course,
>the definitional lead in may be empty. (See the last paragraph of section
>1 above).
>
>iii. The purported proof in T, appended with the so called extreme
>annotation, is sent to the core proof checker for examination.
>
>iv. In practice, it should not be difficult for systems like Mizar and
>Isabelle to conform to these requirements, and also to create an export
>program that supplies the required extreme annotation. Again, for our
>purposes, no verification of this is relevant for us. And if Mizar and
>Isabelle won't do it, then we can wear different hats and go into that
>human/machine interactive business ourselves.
>
>v. If the core proof checker says "yes, this is a correct proof in T",
>then the statement that has been proved, including the definitional lead
>in to it, is posted to the world with a time stamp. The definitional
>leadin used, as well as the statement verified, becomes part of the
>official record of the system. The proof stuff, including the extreme
>annotations, are put away in a separate secure place, of course. This
>official record is meant to be read worldwide by mathematicians, as it is
>particularly friendly.
>
>vi) All subsequently accepted purported proofs in T with extreme
>annotation, must conform and also have available to it, what has been done
>in the official record from these public postings.
>
>We now come to the novel(?) idea here.
>
>The idea is that so much information in the form of pointers, etcetera,
>into the proof in T is given after the end of the proof in T, that this
>alleviates the need for parsers, string searchers, and the like in the
>core proof checker. (We have not yet come to the core proof checker).
>
>Also, this is to be, together with T, a universally agreed upon standard,
>adhered to throughout the world.
>
>We also claim that
>
>i) the specification of the formal system T (much simpler than a computer
>system or computer language!!) is humanly digestible;
>
>ii) the specification of the extreme annotation is humanly digestible.
>
>iii) the proof that every file with an extreme annotation is a proof in T
>over the existing posted record of the system, is humanly digestible.
>
>iv) extreme annotations are not too long for practical use.
>
>I will take a stab at how this is could be designed, in the next posting.
>That should (might) convince you of i) - iii).
>
>Items i) - iii) are to indicate our feeling that we don't need to use
>formal verification methods in connection with i) - iii). However, we are
>entirely open to the idea that some sort of formal verification would be
>desirable in connection with 1) - iii).
>
>3. THE CORE PROOF CHECKER.
>
>Extreme annotation will be so explicit that the core proof checker has
>only to do completely trivial grunt work of the most elemental kind.
>
>We think that one should be able to easily program the core proof checker
>in an appropriate MACHINE LANGUAGE, and have a mathematician write a
>completely readable correctness proof of the machine language program that
>is completely convincing to any mathematician. Special purpose hardware
>would circumvent a number of verification issues.
>
>It may be valuable to do this in an agonizing machine language like Turing
>machines. In fact, that may be a real good test. To show that we are at a
>suitably low level but understandable level, we could see if the TM code
>could easily be written and understandably proved to be correct.
>
>The extent to which any formal verification methods would help here is
>quite unclear, as we are at the primitive lookup level.
>
>Harvey Friedman
>
>
>
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom
More information about the FOM
mailing list