Quibbling about definitions of "proof"
Look, you all, I'm *really sorry* I even brought up the subject of proofs of correctness! As I feared, any mention of certain loaded words immediately brings the quibblers out of their lairs to dissect the "real meaning" of one or more terms. I had thought that my carefully worded mention of the Boyer-Moore prover and that this means little for actual implementations would deter quibbling over the cosmic significance of "proof." (An interesting topic, by the way, as Ray's knowledgeable article makes clear. But metamathematics is an arcane subject and short articles are rarely persuasive...we debated the same stuff a couple of years ago on the Extropians list.) With 700 subscribers, quibbling is the usual state of affairs. No matter what is said, someone will quibble over terms or meanings. No wonder it is the major venal sin at West Point. The Boyer-Moorer theorem prover is an accepted ("Huh? Define what you mean by "accepted"! Not all of us accept that term.") term of art. If you disagree, or wish to raise the possibility that the computer glitched during the proof, there are entire newsgroups devoted to such arcania. On a more mundane note, my Internet Service Provider of the past 6 weeks just sent out an urgent notice tonight announcing that they are no longer "sensemedia.net" and have become "got.net" (as in "got net?" as in "got milk?). This means my 3 years as "tcmay@netcom.com" is followed by 6 weeks as "tcmay@sensemedia.net" and an as-yet-undetermined time as "tcmay@got.net" (at least until the "Got milk?" ad people get wind of this pun and tell them to change to something else. --Tim May Special note: My ISP has changed its domain name from "sensemedia.net" to "got.net" (as in "got milk?"), so I have to again ask you all to bear with me and use my new e-mail address, "tcmay@got.net". ---------:---------:---------:---------:---------:---------:---------:---- Timothy C. May | Crypto Anarchy: encryption, digital money, tcmay@got.net (Got net?) | anonymous networks, digital pseudonyms, zero 408-728-0152 | knowledge, reputations, information markets, Corralitos, CA | black markets, collapse of governments. Higher Power: 2^756839 | Public Key: PGP and MailSafe available. "National borders are just speed bumps on the information superhighway."
All this quibbling about the "validity" of proof checkers is philosophically inept. It is a basic property of logic that it proceeds from axioms to conclusions. No proposition can be understood except by reference to some other proposition. It is not possible to objectively observe anything, all observation is made through a mechanism which is imperfectly analysed and thus the observation is subjective to the extent that the interpretation is unknown. We may obtain an objective statement from a subjective observation by reference to the source of subjectivity. If however the subjective assumptions are shared by all participants within the system of being any statement which follows from only those assumptions may be regarded as objective. Objectivity is thus not an atomic fact but a relation, a fact cannot have the property of objectivity except with respect to a system of being. [Thus I may assert 1+1=2 as an objective fact since the assumptions upon which it is based are commonly shared. If however someone wished to question this statement (e.g. phenomological bracketing) then in the context of that discussion I would accept it as being subjective).] The question of prooving the proof checker is thus an extension of a more fundamental problem, providing proof of proof. Since a proof is a fact and facts are subjective except with resepct to a system of being the demand for proof of consistency of proof is an extension of the requirements for proof as normally understood. The requirement for "prooving" a program is thus significantly less onerous than asserted. It is not necessary to provide a trancendental proof, merely to establish consistency with respect to a commonly accepted set of axioms. Phill Hallam-Baker
All this quibbling about the "validity" of proof checkers is philosophically inept. It is a basic property of logic that it proceeds from axioms to conclusions. No proposition can be understood except by reference to some other proposition.
Except that it all starts with language and developes through set theory.
It is not possible to objectively observe anything, all observation is made through a mechanism which is imperfectly analysed and thus the observation is subjective to the extent that the interpretation is unknown.
And yet it is all based on observations at the initial set theoretic level.
We may obtain an objective statement from a subjective observation by reference to the source of subjectivity. If however the subjective assumptions are shared by all participants within the system of being any statement which follows from only those assumptions may be regarded as objective. Objectivity is thus not an atomic fact but a relation, a fact cannot have the property of objectivity except with respect to a system of being.
And indded, we are people which gives us some common context.
[Thus I may assert 1+1=2 as an objective fact since the assumptions upon which it is based are commonly shared. If however someone wished to question this statement (e.g. phenomological bracketing) then in the context of that discussion I would accept it as being subjective).]
I was taught 1+1=1 in boolean algebra.
The question of prooving the proof checker is thus an extension of a more fundamental problem, providing proof of proof. Since a proof is a fact and facts are subjective except with resepct to a system of being the demand for proof of consistency of proof is an extension of the requirements for proof as normally understood.
But in computers, we are living in a mathematically defined system (except for physical issues which have been suppressed to a very large extent by the design of statistically low error-rate systems) which follows very precisely the logic of its design. Thus proofs work since we are working in this well formed domain.
The requirement for "prooving" a program is thus significantly less onerous than asserted. It is not necessary to provide a trancendental proof, merely to establish consistency with respect to a commonly accepted set of axioms.
More specifically, within the logic dictated by the hardware designed to assure that the system remains within the mathematical structure defined by its design. -- -> See: Info-Sec Heaven at URL http://all.net Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236
All this quibbling about the "validity" of proof checkers is philosophically inept. It is a basic property of logic that it proceeds from axioms to conclusions. No proposition can be understood except by reference to some other proposition.
Except that it all starts with language and developes through set theory.
That is not necessarily the case. It all starts with communication of which language is a form, logic is a more perfect form of communication because its validity is most widely shared. It is perfectly consistent to deny the supremacy opf logic. Wittgenstein was wrong to assert that it is impossible to step outside the logical framework. The mind may be characterised by logical inferences but that does not mean that it is bounded by logical inferences. The observer might take a hallucinatory drug for example and thereby participate in an extra-logical ontology.
And yet it is all based on observations at the initial set theoretic level.
Only if you accept that the logical positivists were right and that there is no thought that cannot be characterised in that manner. The problem with this approach is that it prevents consideration of the real issue which philosophy should consider, the questions of being, time and spirit. We might conisder that the logical positivists found and aswer to the wrong question while the continetal school found an unsatisfactory anwer to the right one.
And indded, we are people which gives us some common context.
Exactly we can communicate because we participate within the same system of being and that provides sufficient common reference points for us to convince ourselves that we are communicating the same ideas. We cannot prove that we are in fact achieiving this goal for we cannot objectively determine that we both observe the same things.
The question of prooving the proof checker is thus an extension of a more fundamental problem, providing proof of proof. Since a proof is a fact and facts are subjective except with resepct to a system of being the demand for proof of consistency of proof is an extension of the requirements for proof as normally understood.
But in computers, we are living in a mathematically defined system (except for physical issues which have been suppressed to a very large extent by the design of statistically low error-rate systems) which follows very precisely the logic of its design. Thus proofs work since we are working in this well formed domain.
But that mathematically defined system is still subject to the constraint that we cannot analyse the thing in itself. Instead we must step outside the system to analyse it. We do not in fact define LISP in LISP what we actually do is to define LISP in a language that looks like LISP and demonstrate that the two are compatible. It is important to distinguish a demonstration of meta-consistency from a proof within the logic of that logic. We might assert correctly that a program have been proven correct using a proof checker. We do not need to explain that the proof is of correctness with respect to a set of axioms for that is the nature of proof and is thus no more necessary when considering proofs of computer programs than of any other type of proofs. The meta-form of this proof is "A Therefore B where B is independent of A". We cannot however assert that we have used the program checker to prove itself. That would have a meta-form "A Therefore A". This form does not contain any information. The only meta form of A concerning A that carries information is "A Therefore (not A)". This implies that A is false. Thus although it is not possible to prove A true it is possible to prove it false. Phill Hallam-Baker
On Mon, 7 Aug 1995 hallam@w3.org wrote:
The requirement for "prooving" a program is thus significantly less onerous than asserted. It is not necessary to provide a trancendental proof, merely to establish consistency with respect to a commonly accepted set of axioms.
Phill Hallam-Baker
Is THAT all? But I didn't know we could establish consistency of these commonly accepted axioms with THEMSELVES! (By commonly accepted, I mean ZF. I'll even the choice & continuum hypotheses out.) Nathan
Phill Hallam-Baker summarized it best. I advise anyone interested in this issue to read up on pancritical rationalism (a favorite extropian topic of debate). "The Retreat to Commitement" by Bartley (?, sorry, can't recall at the moment, the book is not with me) is a good writeup of the subject. At the lowest level, even the basic axioms can be cricitized. -Ray
participants (5)
-
fc＠all.net -
hallam＠w3.org -
Nathan Zook -
Ray Cromwell -
tcmay＠got.net