From owner-qed Sun Aug 14 10:57:01 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA04053 for qed-out; Sun, 14 Aug 1994 10:53:51 -0500 Received: from cli.com (cli.com [192.31.85.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA04047 for ; Sun, 14 Aug 1994 10:53:44 -0500 Received: from rita (rita.cli.com) by cli.com (4.1/SMI-4.1) id AA16208; Sun, 14 Aug 94 10:53:11 CDT From: boyer@CLI.COM (Robert S. Boyer) Received: by rita (4.1) id AA25876; Sun, 14 Aug 94 10:53:10 CDT Date: Sun, 14 Aug 94 10:53:10 CDT Message-Id: <9408141553.AA25876@rita> To: qed@mcs.anl.gov Subject: More replies to JMC Sender: owner-qed@mcs.anl.gov Precedence: bulk Here are replies to several of McCarthy's remarks: > 3. Actually, for AI reasons, I don't give much weight to constructive > correctness. You are not alone. A *lot* of people give little or no weight to constructive correctness, and for a number of reasons. It is nevertheless true that a quite substantial portion of the people currently working on mechanical proof-checking *are* concerned about constructive matters. This is perhaps a quite inevitable state of affairs -- perhaps many of those who are motivated to get things as correct as possible are bound to pay attention to the critics of current mathematical orthodoxy and its classical, set theoretic practice. > 1. If the result came originally from a "constructively correct" > theory, then going through set theory shouldn't harm it. I don't know what you mean by "harm"? How does one "harm" a wff? More seriously, the point I was making is that a constructivist doesn't put much store in a proposition about which all that is known is that it is a theorem of set theory. Admittedly, to you this may be of no concern. > 2. If the result was derived in set theory and people are motivated to > take the trouble, they can label the result with what was used in > deriving it. Perhaps there is a good scheme for such labeling, but I don't know it. The question comes down to defining "what was used in deriving it". If this is nothing but a full Hilbert-Goedel style FOL proof, it's not clear to me that a constructivist is going to be able, in general, to tell whether there is any constructive content to a given set theory theorem. (I should correct a previous message and identify the "only one disjunct on the righthand side" syntactic restriction of classical logic to intuitionistic logic I mentioned as being an intuitionistic sequential calculus of Gentzen, which is presented in Kleene's "Introduction to Metamathematics". A most knowledgeable friend, in correcting me, adds that the essential difference is in the right negation rule, which can only be applied when the right hand side is empty.) > 4. Is there another proposal for an intermediate language? It seems to me that the alternative to set theory as the single intermediate language is not another single, universal, intermediate language but a number of languages, all tied together with metamathematical connections. Metamathematical results could be mechanically proof-checked with checkers for some of the weaker sorts of logics that proof theorists have long used. I think that Hilbert and Bernays recommended something like Skolem's primitive recursive arithmetic as the basis upon which to do metamathematics, but Feferman's FS0 seems much more usable, e.g., it has "cons" and quantifiers. Perhaps something even weaker will suffice, thus accommodating those who suspect that the full set of primitive recursive functions is a fantasy. Perhaps we won't need a logic with functions of more than polynomial complexity in order to prove that, say, any proof of a certain class of theorems in the Coq logic can always be transformed to a proof of a related theorem in the Mizar logic. One can make some progress merely by writing and executing functions that actually do such proof transformations, but I suspect that it will be eventually be practically necessary to prove the correctness of such functions, rather than to run them, simply because the transformed proof objects will be too large. I suspect that such correctness proofs, a kind of baby metamathematics, can be carried out in weak logics that are widely supported. It would be divine if there could be agreement on a single, very strong, universal language, but I doubt that such agreement is to be found. It seems sensible for us to see what we can agree upon, if anything, and then treat what we cannot agree upon not as doctrinal issues that separate us but merely as interesting logical variations that support results which can sometimes be transformed from one variation to another. I imagine that ring theorists don't disparage group theorists, but rather take advantage of their theorems as much as possible. But currently, the users of the many mechanical proof checking systems manage to depend upon the results of the use of other systems about as little as one might imagine. Bob