Re: Quibbling about definitions of "proof"

[fc@all.net (Dr. Frederick B. Cohen)]

> 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