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