Re: Quibbling about definitions of "proof"

[hallam@w3.org]

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