[FOM] Solution (?) to Mathematical Certainty Problem

[Steve Newberry]

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